# Functorial Semantics for Algebraic Theories


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.

#### Algebraic Theories

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 $t(x)$ is a term $t$ over the signature in question together with a context $x$ such that all free variables of the term appear in the context. An equation-in-context $s = t(x)$ consists of two terms $s,t$ 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 $s = s' \;(x)$ and $t = t' \; (x, y)$ is known, we can conclude $t[s/y] = t'[s'/y] \;(x)$). We write $T \vdash s = t \; (x)$ if $s = t \; (x)$ is a theorem.

A example of an algebraic theory is the theory of monoids, which has a single sort $M$ and a two operator symbols: the binary $\cdot$ (written infix) and the nullary $e$. Its equations are simply $e \cdot m = m(m)$ and $(m_1 \cdot m_2) \cdot m_3 = m_1 \cdot (m_2 \cdot m3) (m_1, m_2, m_3)$.

#### Algebras

Given a algebraic signature $\Sigma$ and a category $\mc C$ with finite products, a $\Sigma$-structure $M$ in $\mc C$ maps each sort $A$ of $T$ to an object $MA$ of $\mc C$ and each operator $f \colon A_1, \ldots, A_n \to B$ to an arrow $Mf \colon \prod_{i=1}^n MA_i \to B$ (without any further requirements). To any context $x = x_1 : A_1, \ldots, x_n : A_n$ we can then associate an object $Mx = \prod_{i=1}^n MA_i$. We can use all of this to define the denotation of a term-in-context $t(x)$ of sort $A$ to be an arrow $[[t (x)]]_M \colon Mx \to MA$:
* if $t = x_i$ with $x_i : A$, then $[[t(x)]]_M$ is the projection $\pi \colon Mx \to MA$ with $\pi(x) = x_i$.
* if $t = f(t_1, \ldots, t_n)$, then $[[t(x)]]_M$ is $Mf \circ \prod_{i=1}^n [[t_1(x)]]_M$.

If $T$ is an algebraic theory on $\Sigma$ and $M$ is a $\Sigma$-structure, we say that $M$ satisfies an equation-in-context $s = t \; (x)$, written $M \models s = t \; (x)$, if $[[s(x)]]_M = [[t(x)]]_M$. If $M$ satisfies all equations of a theory, it is called a $T$-algebra in $\mc C$. The $T$-algebras in a category again form a category $\model(T, \mc C)$, where morphisms $h \colon M \to N$ are given by a family of $\mc C$-arrows $h_A$, one for each sort $A$ of $\Sigma$, such that for every function symbol $f \colon A_1,\ldots, A_n \to B$ 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 $h(x\cdot y) = h(x) \cdot h(y)$ in a monoid.

#### Soundness

We can now prove the soundness property, namely, that every $T$-algebra $M$ satisfies all theorems of $T$. 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 $t(x), s(y)$, let us write $t(s(y))$ for the term $t[s_1/x_1, \ldots, s_n/x_n](y)$. Then by induction on $t$, one can prove that $[[t(s(y))]]_M = [[t(x)]]_M \circ \langle [[s_1(y)]]_M, \ldots, [[s_n(y)]] \rangle$. Weakening is then just a special case of substitution.

#### Completeness

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 $\clsf(T)$ of $T$ where the objects are simply contexts and an arrow $h \colon x = (x_1,\ldots, x_n) \to (y_1, \ldots, y_m) = y$ is a list of terms-in-context $(t_1(x), \ldots, t_m(x))$. More precisely, these are equivalence classes of these, since we identify two arrows $(t_1(x), \ldots, t_n(x))$, $(s_1(x), \ldots, s_n(x))$ if $s_i = t_i (x)$ is provable in $T$. Composition of arrows $(t_1(x), \ldots, t_m(x)) \colon (x_1, \ldots, x_n) \to (x_1, \ldots, x_m)$, $(s_1(x), \ldots, s_k(x)) \colon (x_1, \ldots, x_m) \to (x_1, \ldots x_k)$ is defined by substitution in each component, $s_i[t_1, \ldots, t_m/x_1, \ldots, x_m]$. 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 $\clsf(T)$ has all finite products and they are given by concatenation of contexts. We can now define a $T$-structure $U$ in $\clsf(T)$ by setting $UA = (x \colon A)$ for all sorts $A$ and $Uf = f(x_1, \ldots, x_n)$ for $f \colon A_1, \ldots, A_n \to B$. Then $U \in \model(T, \clsf(T))$, since, by definition,

#### Functorial Semantics

Now amazingly, any $T$-algebra $M$ in $\mc C$ can be seen as an image of $U$ under a specific finite-product preserving functor (FP-functor) $\clsf(T) \to \mc C$, and vice-versa, each FP-functor $F \colon \clsf(T) \to \mc C$ induces a $T$-algebra. First note that any such functor $F$ maps $U$ to a $T$-algebra in $\mc C$ (this part is obvious; we write $FU$ for this $T$-algebra). Also, if $\eta \colon F \Rightarrow G$ is a natural transformation between two such functors, notice that it restricts to a $T$-algebra homomorphism between $FU$ and $GU$, since for all $f \colon A_1, \ldots, A_n \to B$ we have, by naturality and preservation of products, that $\eta_{UB} \circ FU f = GUf \circ \eta_{\prod UA_i}$. Thus evaluation at $U$ is a functor $\mathrm{eval}_U \colon \mc C^{\clsf(T)} \to \model(T, \mc C)$. When restricted to the full subcategory of FP-functors, this yields an equivalence: Given any model $M \in \model(T, \mc C)$, we can construct an FP-functor $F_M \colon \clsf(T) \to \mc C$ by setting $F_M((x \colon A)) = MA$ for all sorts $A$ (finite product preservation then fully determines the other objects) and $F_M(t (x)) = [[t (x)]]_M$. This is a functor, since $M$ is a model and two arrows in $\clsf(T)$ are equal iff they are equal in all models.

The category $\clsf(T)$ is then called the classifying category and $U$ the universal model, and by the preceding discussion it is defined by the universal property that $T$-algebras in $\mc C$ are in one-to-one correspondence with FP-functors $\clsf(T) \to \mc C$. Sometimes $U$ 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 $y \colon \clsf(T) \widehat{\clsf(T)}$, $A \mapsto \mathrm{Hom}(--, A)$ gives rise to another logically generic model $y(U)$, since $y$ 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 $\clsf(T)$ 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 $\mc C$ with finite products, the associated signature $\Sigma_{\mc C}$ contains a sort for each object of the category and a operator symbol $f \colon A_1, \ldots, A_n \to B$ for each arrow $f \colon \prod{i=1}^n A_i \to B$. Now let $M_{\mc C}$ be the model sending every sort and every operator symbol to itself (the terms over this signature make up the internal language of $\mc C$, and essentially allow you to treat $\mc C$ similar to $Set$). Now consider the theory $T_{\mc C}$ with all equations satisfied by $M_{\mc C}$ 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 $\clsf(T_{\mc C}) \simeq \mc C$.