These are my notes taken while approaching categorical logic from the angle of algebraic theories. My notes are based on Notes on Categorical Logic by Andrew Pitts, Steve Awodey’s (unfortunately unfinished, but very helpful) lecture notes on categorical logic, and the ncatlab article on internal logic.
An algebraic signature is specified by a set of sorts, a set of operator symbols, and a set of variables for each sort. A context is a (possibly empty) list of distinct variables with their types. We will denote the empty context by . A term-in-context is a term over the signature in question together with a context such that all free variables of the term appear in the context. An equation-in-context consists of two terms of the same with a context that is appropriate for both of them. Finally, an algebraic theory is given by an algebraic signature and a set of equations-in-context. The theorems of the theory are the derivable equations using reflexivity, transitivity, symmetry, substitution, and weakening (where weakening refers to the fact that we can add more variables to a context and substitution means that if and is known, we can conclude ). We write if is a theorem.
A example of an algebraic theory is the theory of monoids, which has a single sort and a two operator symbols: the binary (written infix) and the nullary . Its equations are simply and .
Given a algebraic signature and a category with finite products, a -structure in maps each sort of to an object of and each operator to an arrow (without any further requirements). To any context we can then associate an object . We can use all of this to define the denotation of a term-in-context of sort to be an arrow :
* if with , then is the projection with .
* if , then is .
If is an algebraic theory on and is a -structure, we say that satisfies an equation-in-context , written , if . If satisfies all equations of a theory, it is called a -algebra in . The -algebras in a category again form a category , where morphisms are given by a family of -arrows , one for each sort of , such that for every function symbol the diagram
commutes. All this generalizes the usual algebraic notions; e.g. a monoid in the category of sets is just a monoid, and the commutativity of the diagram just states that in a monoid.
We can now prove the soundness property, namely, that every -algebra satisfies all theorems of . To do this, it is enough to ensure that the rules of inference are compatible with our models. Reflexivity, symmetry, and transitivity just restate properties of equality for arrows. This still leaves weakening and substitution open (which brings us to the substitution lemma). For terms-in-context , let us write for the term . Then by induction on , one can prove that . Weakening is then just a special case of substitution.
Completeness can be proved by constructing a model that satisfies just the theorems provable in the theory. For this, let us define the syntactic category of where the objects are simply contexts and an arrow is a list of terms-in-context . More precisely, these are equivalence classes of these, since we identify two arrows , if is provable in . Composition of arrows , is defined by substitution in each component, . Note that each variable in a context belongs to a certain sort, which I have suppressed here, and two contexts are only equal if they also agree on sorts.
This category has all finite products and they are given by concatenation of contexts. We can now define a -structure in by setting for all sorts and for . Then , since, by definition,
Now amazingly, any -algebra in can be seen as an image of under a specific finite-product preserving functor (FP-functor) , and vice-versa, each FP-functor induces a -algebra. First note that any such functor maps to a -algebra in (this part is obvious; we write for this -algebra). Also, if is a natural transformation between two such functors, notice that it restricts to a -algebra homomorphism between and , since for all we have, by naturality and preservation of products, that . Thus evaluation at is a functor . When restricted to the full subcategory of FP-functors, this yields an equivalence: Given any model , we can construct an FP-functor by setting for all sorts (finite product preservation then fully determines the other objects) and . This is a functor, since is a model and two arrows in are equal iff they are equal in all models.
The category is then called the classifying category and the universal model, and by the preceding discussion it is defined by the universal property that -algebras in are in one-to-one correspondence with FP-functors . Sometimes is also referred to as logically generic for the calculus we sketched in the beginning, which here simply means that it satisfies exactly these equations that are provable. As a side note, the Yoneda embedding , gives rise to another logically generic model , since is an FP-functor that is also faithful.
Instead of starting off with a theory and building a category, we can also go the other way around. What the construction of essentially did, was replacing the representation of a theory via axioms by some category with a universal property that ensures that the category contains all consequences of the axioms, and just these. So given a category with finite products, the associated signature contains a sort for each object of the category and a operator symbol for each arrow . Now let be the model sending every sort and every operator symbol to itself (the terms over this signature make up the internal language of , and essentially allow you to treat similar to ). Now consider the theory with all equations satisfied by as axioms. Intuitively, it is clear that this construction is right-adjoined to the process of constructing the syntactic category (in a sense, we are simply forgetting that our theory is also a category), and that .