Algebraic theories
(Part 2 of a series.)
This post is quite long, since it introduces the judgmental machinery of type theory. Future posts will be shorter and less familiar to any type theorists in the audience.
We start by exploring the notion of an algebraic theory, a collection of terms and equations between these terms. To define an algebraic theory, we start by writing down a signature of constants and their arities.
For example, a group is a structure which has

a distinguished identity term \(\mathord{\sf{\text{e}}}\),

a multiplication operation \(\circ\) which sends any two terms \(x,y\) to a single term \(x\circ y\), and

an inverse operation \({}^{1}\) which sends any term \(x\) to a term \(x^{1}\).
(These operations must satisfy certain equations, which we’ll get to later.)
We say its signature has three constants: \(\mathord{\sf{\text{e}}}\) has arity zero, as it requires no arguments; \({}^{1}\) has arity one, as it takes one argument; and \(\circ\) has arity two. We obtain a term by applying a constant of arity \(a\) to exactly \(a\) terms. Because they send terms to terms, constants are usually called function symbols.
Let us write the judgment \(\Gamma\vdash t\) whenever

\(\Gamma\) is a (possibly empty) set of variables, and

\(t\) is a valid term in the theory, given the above rules and that each variable in \(\Gamma\) is also assumed to be a term in the theory.
Thus, \(\cdot\vdash\mathord{\sf{\text{e}}}\) means that, under no assumptions, \(\mathord{\sf{\text{e}}}\) is a term. \(x\vdash x^{1}\) means that, assuming \(x\) is a variable standing in for some term, then \(x^{1}\) is a term.
Of course, it is safe to make extraneous assumptions—it is the case that \(\mathord{\sf{\text{e}}}\) is also a term when \(x\), \(y\), and \(z\) stand in for terms (i.e., \(x,y,z\vdash\mathord{\sf{\text{e}}}\)). But it isn’t the case that \(\cdot\vdash x^{1}\), since the variable \(x\) is not intrinsically a term. (Do not confuse the constant term \(\mathord{\sf{\text{e}}}\) with variables like \(x,y,z\).)
We can summarize the signature of a group with the following rules. Read these rules as stating that whenever all the judgments above the line are true, so is the judgment below the line. As before, \(\Gamma\) stands for any set of variables, and \(t,s\) stand for any term.
For example, the second rule says that, if \(t\) is a term under the assumptions in \(\Gamma\), then \(t^{1}\) is also a term under the assumptions in \(\Gamma\).
To show \(\cdot\vdash\mathord{\sf{\text{e}}}^{1}\circ\mathord{\sf{\text{e}}}\) (under no assumptions, \(\mathord{\sf{\text{e}}}^{1}\circ\mathord{\sf{\text{e}}}\) is a term), we would first conclude \(\cdot\vdash \mathord{\sf{\text{e}}}\) from the first rule, which by the second rule implies \(\cdot\vdash\mathord{\sf{\text{e}}}^{1}\). If we apply the third rule to this and to \(\cdot\vdash\mathord{\sf{\text{e}}}\) (from the first rule), we obtain \(\cdot\vdash \mathord{\sf{\text{e}}}^{1}\circ\mathord{\sf{\text{e}}}\). We typically chain these derivations together in a treelike structure, like so:
Structural rules
If we add one more rule to the system, we will be able to derive (from the rules) that \(\Gamma\vdash t\) whenever \(t\) is a term under the assumption that the variables in \(\Gamma\) represent terms. For example, using only the three rules above, we can’t conclude that \(x\vdash x\), even though \(x\) is a term under the assumption that \(x\) is a term. The required rule is:
Called the hypothesis rule, this lets us conclude \(x\vdash x\), or, for example, \(x\vdash x^{1}\) (from \(x\vdash x\) and the second rule).
For any \(t\) such that \(x\vdash t\), it is also the case that \(\cdot\vdash t'\) where \(t'\) replaces all occurrences of the variable \(x\) in \(t\) with the term \(\mathord{\sf{\text{e}}}\). For example, \(x\vdash x^{1}\), and so \(\cdot\vdash\mathord{\sf{\text{e}}}^{1}\). In general, we can turn a derivation of \(x\vdash t\) into a derivation of \(\cdot\vdash t'\) by replacing each instance of the hypothesis rule with the \(\mathord{\sf{\text{e}}}\) rule, and modifying the term appropriately:
We can do better—for any \(x\vdash t\), then \(\Gamma\vdash t'\) where \(t'\) replaces each occurrence of \(x\) in \(t\) by a term \(s\) for which \(\Gamma\vdash s\). Here, we produce the derivation of \(\Gamma\vdash t'\) by replacing each instance of the hypothesis rule with a derivation of \(\Gamma\vdash s\). For example, given \(x\vdash x^{1}\circ x\) and \(a,b\vdash a\circ b\):
We say that \(t'\) is obtained via the (singlevariable) substitution of \(s\) for \(x\) in \(t\), and use \([s/x]t\) to denote this term. We can prove that the following rule holds for all algebraic theories, by performing the derivationrewriting described above.
Substitution generalizes to the simultaneous substitution of multiple variables. If \(x_1,\cdots,x_n\vdash t\), and \(\Gamma\vdash s_1\), …, \(\Gamma\vdash s_n\), then we can derive \(\Gamma\vdash [s_1,\cdots,s_n/x_1,\cdots,x_n]t\), where this term means that each \(x_i\) in \(t\) is replaced by \(s_i\). Again, in all algebraic theories, the following rule is provable:
As a side note, the hypothesis rule ensures certain variables must be in \(\Gamma\) for a particular term, but no rule requires any variables to not be in \(\Gamma\). So, as we said before, it is safe to add extraneous assumptions.
Here, \(y\) is a variable not already in \(\Gamma\), as we require the variables to be distinct. This is called the weakening rule, and is also true of all algebraic theories—in fact, it follows directly from the substitution rule above. Indeed, if \(\Gamma=x_1,\cdots,x_n\), then we can apply the hypothesis rule \(n\) times to get \(\Gamma,y\vdash x_i\). Combining these and \(\Gamma\vdash t\), the substitution rule gives us
where \([x_1,\cdots,x_n/x_1,\cdots,x_n]t=t\) because this substitution replaces each variable with itself; thus we conclude \(\Gamma,y\vdash t\).
Axioms
We finally have enough machinery to finish defining algebraic theories. After fixing a signature, we list axioms equating some of the terms. By default, we include reflexivity, symmetry, and transitivity, which guarantee that syntactically identical terms are equal.
It is worth noting that substitutions are not part of terms themselves, but rather send terms to terms. Thus, for example, we need not throw in any additional equality rules to ensure \(x\vdash [x/y]y=x\), since \([x/y]y\) denotes the term \(x\).
We also include an axiom which states that equality is a congruence, that is, that two terms are equal when their corresponding subterms are pairwise equal.
This allows us to conclude, for example, that if \(\Gamma\vdash t=t'\), then \(\Gamma\vdash t\circ\mathord{\sf{\text{e}}}= t'\circ\mathord{\sf{\text{e}}}\). If \(\Gamma=x_1,\cdots,x_n\), then
One axiom of groups says \(\Gamma\vdash t\circ\mathord{\sf{\text{e}}}= t\) when \(\Gamma\vdash t\): assuming \(t\) is a term under \(\Gamma\), then \(t\circ\mathord{\sf{\text{e}}}\) is equal to \(t\) under \(\Gamma\). (We maintain the \(\Gamma\) because, in general, \(t\) is not a term except under \(\Gamma\).)
The group axioms state that \(\mathord{\sf{\text{e}}}\) is an identity on both sides,
that \({}^{1}\) produces inverses,
and that \(\circ\) is associative:
Summary
I realize I’ve introduced a huge amount of notation and terminology during this post, but it’s hard to get started without the framework of judgments we’ve developed. Let’s summarize:
An algebraic theory is a signature (a set of constants with arities) and a set of axioms equating some of the terms generated by the signature. We use the judgmental notation \(\Gamma\vdash t\), meaning that \(t\) is a term, assuming that each variable in the set \(\Gamma\) represents a term.
Each algebraic theory includes rules corresponding to its signature. All algebraic theories additionally satisfy the hypothesis rule (below, left), and have a definable notion of substitution satisfying the substitution rule (below, center). The substitution rule implies the weakening rule (below, right).
We also have a judgment \(\Gamma\vdash t=s\), meaning that \(\Gamma\vdash t\), \(\Gamma\vdash s\), and that \(t\) and \(s\) are equal terms. Each theory comes with its own axioms. In all theories, equality is additionally reflexive, symmetric, transitive, and a congruence.
Thanks to Nico Feltman for some helpful feedback on this post, and commenter gasche for noting my omission of the congruence rule.
I am not so fond of the syntax for the hypothesis rule. To me it looks like an unfinished proof tree. Is this syntax wide spread?
January 24th, 2013 at 10:20 amOften $x\in\Gamma$ is omitted from the rule, but more explanation would have been required that way. One could of course axiomatize the $\in$ relation in order to close off the proof trees entirely (a variable is in the context if it is the last thing in the context, or if it is in the head of the context) but that’s perhaps a bit too pedantic here, and makes simple proof trees much larger.
January 26th, 2013 at 2:40 pmI’m missing some congruence rules in your equality: how would you
February 10th, 2013 at 5:54 amprove that (t . u . u⁻¹ = t)?
gasche: You’re quite right, and I’ve updated the post with one additional rule.
February 17th, 2013 at 8:24 pm