Algebraic Theory

We mainly follow Awodey for the definition, models and interpretations. The idea is to develop a categorical approach to logic.

A theory in the traditional approach is given by a particular presentation. Namely by allowed operations and axioms. This presentation is like a presentation of a vector space on one particular basis, which should be able to be dispensed of while might be helpful practically. Therefore from a theory one constructs a category, called syntactic category, that contains the same information as the theory but is syntax invariant. This category should be in some sence universal since all dispensable informations (those about presentations) are removed. The informations of the theory should be encoded in the structure of the category. In this sense the syntactic category of an algebraic theory is a classifying category of its.

We don’t need to distinguish much between a particular presentation fo an algebraic theory and its syntactic category. The models of the theory are then given by structure-preserving functors from the syntactic category to categories that admit a model. In fact, when the functor admits all finite products, functoriality alone ensures that all valid (satisfying the axioms in a particular presentation) equations of the theory are preserved.

Translating between different models (homomorphisms between models) are then given by natural transformations of the functors that produce a model.

The classifying category of a theory can be constructed from the logical syntax of the theory. This is the completeness of the theory with respect to general categorical semantics. Completeness with respect to a special class of models depends on the structure of the codomain categories of the models.

Definition

Fix a family of sets $\{\Sigma_k\}_{k\in \mathbb{N}}$ called signature. The elements of $\Sigma_k$ are $k$-ary operations. The elements of $\Sigma_0$ are the constants or nullary operations. Given a signature $\Sigma$, the terms of the signature $\Sigma$ are expression constructed inductively by the rules

  1. variables $x,y,z$ are terms,
  2. if $t_1,\ldots,t_k$ are terms and $f\in \Sigma_k$, then $f(t_1,\ldots,t_k)$ is a term.
Definition(Algebraic theory) . An algebraic theory $\mathbb{T}=(\Sigma_\mathbb{T},A_\mathbb{T})$ is given by a signature $\Sigma_\mathbb{T}$ and a set $A_\mathbb{T}$ of axioms which are equations between pairs of terms.

Examples

  1. The theory of groups. We have a $2$-ary operation $\cdot\in \Sigma_2$, a constant $e\in \Sigma_0$, and a $1$-ary operation $(\cdot)^{-1}\in \Sigma_1$. The axioms are equations $x\cdot(y\cdot z) = (x\cdot y) \cdot z$, $x\cdot e = x$, $e\cdot x=x$, $x\cdot x^{-1} = e$ and $x^{-1} \cdot x=e$.

Of course one can say formulate the theory of groups in a different manner and describe it as a set $G$ with a binary operation $\cdot$ satisfying the two axioms for the existence of $e$ and an inverse and the associativity of $\cdot$. However this requires quantifiers and hence the axioms are no longer equations.

  1. The theory of commutative rings with unit. $0,1\in \Sigma_0$, $- \in \Sigma_1$, $+,\cdot \in \Sigma_2$. The equations are easy to find.

Maybe a non-example will be more illuminating:

There is no reformulation of the general theory of posets into an equivalent equational one, while given a meet or join one can make the equational theory of $\wedge$-or-$\vee$-semilattices, by defining, for example, a partial ordering $x\leq y \Leftrightarrow x\wedge y = x$.

Models and interpretations

Definition(interpretation) . A interpretation $I$ of an algebraic theory $\mathbb{T}$ in a category $\mathbb{C}$ with finite products consists of an object $I\in\mathcal{C}$ and a morphism $f^I : \underbrace{I\times I\times\ldots \times I}_{k\text{ times}}\rightarrow I$ for each operation $f\in \Sigma_k$.

The interpretation can be extended to all terms. These are context dependent. Given a general term $t$, it is always interpreted together with a context of variables $x_1,\ldots,x_n$ containing the variables appearing in $t$. We write $$ x_1,\ldots,x_n | t $$ to indicate that the term $t$ is interpreted in the context $x_1,\ldots,x_n$. The interpretation of $t$ is then a morphism $t^I:I^n\rightarrow I$ determined by the specifications

  1. The $i$-th projection $\pi_i: I^n\rightarrow I$ is the interpretation of the variable $x_i$.
  2. A term of the form $f(t_1,\ldots,t_k)$ is interpreted as the composite $$ I^n\xrightarrow{(t_1^I,\ldots,t_k^I)} I^k \xrightarrow{f^I}I $$ where $t^I_i: I^n\rightarrow I$ is the interpretation of the subterm $t_i$ and $f^I$ is the interpretation of the basic operation $f$.

The equation $u=v$, where $u$ and $v$ are terms in a context $x_1,\ldots,x_n$, is said to be satisfied by the interpretation $I$ if $u^I = v^I$ as morphisms in $\mathcal{C}$. This we also write as $I\models u=v$.

Definition(model) . A model $M$ of an algebraic theory $\mathbb{T}$ in a category $\mathbb{C}$ with finite products is an interpretation $I$ of the theory that satisfies the axioms of $\mathbb{T}$, i.e. $I\models u=v$ for all $(u=v)\in A_\mathbb{T}$ ($u$ and $v$ are terms).

The individual groups and rings as we know are models of the algebraic theory of groups and rings in the category $\mathsf{Set}$. By translating the equations between elements into equations between the operations themselves one can extend the models of group theory in any category $\mathcal{C}$ with finite products $\times$.

A group $G$ in $\mathcal{C}$ is then an object $G\in\mathcal{C}$ equipped with arrows:

Created by potrace 1.16, written by Peter Selinger 2001-2019

satisfying some obvious commutative diagrams. Homomorphism of groups would be arrows in $\mathbb{C}$ between groups that commute with the interpretations of the operations $m,i,e$. These give a category of groups $\mathsf{Group}(\mathbb{C})$ in $\mathbb{C}$. If we write $\mathbb{T}_G$ for the algebraic theory of groups, this is the category $\mathsf{Group}(\mathbb{C}) = \mathsf{Mod}(\mathbb{T}_G,\mathbb{C})$ of $\mathbb{T}_G$-models in $\mathbb{C}$.

Syntactic categories

This can be familiar if one is aquainted with proof theory.

Loosely speaking, what is really important in a theory is the structure of the morphisms between contexts, so a theory should be seen as a category. Equivalent algebraic theories are presentations of the category in a specific manner. There can be many algebraic axiomatization, or presentations of a theory as equivalent algebraic theories. Namely, different choices of basic constants, operations and axioms, hence different choices of algebraic theoires, can lead to a same theory.

The presentation-independent category $\mathcal{C}_{\mathbb{T}}$ for a general algebraic theory $\mathbb{T}$ is called the syntactic category of $\mathbb{T}$.

  1. The objects are equivalence classes of contexts under renaming of variables.
  2. A morphism from $[x_1,\ldots,x_m]$ to $[x_1,\ldots,x_n]$ is an $n$-tuple $t=(t_1,\ldots,t_n)$ of terms $x_1,\ldots,x_m|t_k$.
    • Two morphisms $t=(t_1,\ldots,t_n)$ and $s=(s_1,\ldots,s_n)$ are equal iff $\mathbb{T}\vdash t_k = s_k$.
    • So these are tuples of equivalence classes of terms in context, where two terms are equivalent when the theory proves them to be equal.
    • The composition of morphisms $s\circ t$ is the morphism obtained by substituting the variables of $s$ with terms in $t$.

There is a equivalence of categories between [the category of finite product preserving functors $\mathcal{C}_\mathbb{T} \rightarrow \mathcal{D}$, where $\mathcal{D}$ is a category with finite product], and [the category $\mathsf{Mod}(\mathbb{T},\mathcal{D})$]. This is genven by a functor

$$ \mathsf{eval}_U : \mathsf{Func}_{\mathrm{FP}}(\mathcal{C}_\mathbb{T},\mathcal{D}) \rightarrow \mathsf{Mod}(\mathbb{T},\mathcal{D}) $$

where $U$ is a $\mathbb{T}$-model in $\mathcal{C}_\mathbb{T}$ with the object being the context $U=x_1$ of length one and each operation $f$ of arity $k$ is interpreted as itself. The model $U$ is called the syntactic model in $\mathcal{C}_\mathbb{T}$.

Note that this is similar to Yoneda lemma.

Classifying category

Given an algebraic theory $\mathbb{T}$ we have a notion of classifying category:

Definition(Classifying category) . The classifying category of an algebraic theory $\mathbb{T}$ is a category with finite products $\mathcal{C}$ with a distinguished model $U$ such that
  • for any model $M$ in any category $\mathcal{D}$ with finite products there is a functor $M^\sharp:\mathcal{C}\rightarrow \mathcal{D}$ which preserves finite products and an isomorphism of models $M\cong M^\sharp(U)$
  • for any functors $F,G$ that preserve finite products and model homomorphism $h:F(U) \rightarrow G(U)$ there is a unique natural transformation $\theta:F\Rightarrow G$ with $\theta_U = h$.
The model $U$ is called the universal model.
Theorem. Every algebraic theory $\mathbb{T}$ has the syntactic category $\mathcal{C}_\mathbb{T}$ as a classifying category.