Anton Christenson: Functorial Semantics for Fragments of First-Order Logic

Abstract

Functorial semantics provides a close connection between logic and category theory, where models of a theory can be seen as functors out of a classifying category. This perspective also shows how set-theoretic models can be generalized in a natural way to models in any other category with the appropriate structure.
 
In this thesis we introduce functorial semantics first for algebraic theories and then for intuitionistic first-order logic, and show how the categorical framework can be used to prove soundness and completeness of the corresponding deductive systems.

Different treatments of this topic make different equivalent choices both on the logical side (in terms of which deductive rules to include) and on the categorical side (in terms of which extra structure to require). We aim here to make the connection between the two sides as clear as possible, by stating the structural requirements in a way that directly mirrors the deductive rules. This approach also simplifies the process of comparing and contrasting different logical fragments, such as regular and coherent logic.