A DOCTRINAL VIEW OF LOGIC

The general framework of this thesis is Categorical Logic, more precisely the one of Doctrines, introduced by Lawvere in 1969. Doctrines are a categorical tool that allows the analysis of both syntax and semantics of logical theories — in particular first-order theories — using the same mathematical structure. The thesis begins with a thorough analysis of Henkin’s Theorem for first-order logic (“every consistent theory has a model”), with the aim of interpreting it in the language of existential implicational doctrines. The thesis also considers how to describe free constructions in algebra in the context of elementary doctrines. At first, we study the meaning of “adding a constant to a language” for any doctrine, and “adding an axiom to a theory” for a primary doctrine. These constructions are used to find a possible interpretation of Henkin’s Theorem. Starting from a consistent doctrine, we construct a new doctrine which is rich, where a theory is rich when for every valid formula of the kind ∃xφ(x) there exists a witness constant c such that φ(c) holds. We then show that a rich doctrine admits an appropriate morphism towards the doctrine of subsets. Henkin’s Theorem for doctrines follows from these two results, and our proof in the context of existential implicational doctrines is modeled on the main lines of the original theorem. Finally, the thesis proposes a further analysis of the procedure for adding structure and axioms to a theory, this time in the context of elementary doctrines. It is well-known in universal algebra that adding structure and equational axioms generates forgetful functors between varieties, and such functors all have left adjoints. Given a morphism of elementary doctrines, we prove the existence of a left adjoint of the functor induced by precomposition in the doctrine of subobjects of a Grothendieck topos. It is then shown how the existence of free functors in universal algebra follows from a more general result that lives in the theory of doctrines.