Set-theoretic models of algebraic theories: II

(Part 4 of a series.)

We will henceforth treat theories primarily as collections of rules, rather than signatures equipped with axioms. This viewpoint allows us to treat extensions of algebraic theories as merely comprising additional rules; it also affords a uniform treatment of all the rules.

A set-theoretic model of an algebraic theory is a set \(X\) and an interpretation function \([\![- ]\!]\) which sends every judgment \(x_1,\cdots,x_n\vdash t\) to a function \([\![x_1,\cdots,x_n\vdash t ]\!]:X^n\to X\).

In particular, for each rule

it must be the case that, if a function \([\![\Delta\vdash s ]\!]\) exists, then we can produce a function \([\![\Gamma\vdash t ]\!]\) in some fashion generic to the choice of \(\Delta,\Gamma,s,t\). And for each rule

it must be the case that \([\![\Gamma\vdash s ]\!]=[\![\Gamma\vdash t ]\!]\).

Structural rules

Recall that \(x_1,\cdots,x_n\vdash t\) means that, so long as \(x_1,\cdots,x_n\) stand for terms, \(t\) is a term. Then \([\![x_1,\cdots,x_n\vdash t ]\!]\) is a function which takes an \(n\)-tuple of terms \((x_1,\cdots,x_n)\) and returns a term \(t\) which may contain them. In particular, the hypothesis rule

is modeled by the function \((x_1,\cdots,x_n)\mapsto x_i\) which projects out the \(i\)th element of the tuple. (We call this projection function \(\pi^n_i\).)

The substitution rule:

tells us that, from \(n\) functions \(f_1,\cdots,f_n:X^m\to X\) (given by \([\![\Gamma\vdash s_i ]\!]\)) , and a function \(g:X^n\to X\) (given by \([\![x_1,\cdots,x_n\vdash t ]\!]\)), we can get a function \(X^m\to X\). We model this by the function \(\hat x\mapsto g(f_1(\hat x),\cdots,f_n(\hat x))\) which takes an \(m\)-tuple, forms an \(n\)-tuple by applying each \(f_i\) to that tuple, and passes all the results to \(g\).

A side note to cognoscenti: this actually enforces alpha-equivalence (the irrelevance of variable names) in the model. For example, by substitution,

shows that \([\![y\vdash [y/x]t ]\!]\) must be modeled by \(y\mapsto [\![x\vdash t ]\!](y)\), which is simply \([\![x\vdash t ]\!]\). The same argument applies with any number of variables in the context.

Signature rules

How do we model the signature rules? Consider \(\circ\). In particular, we have the instance

which gives rise to a function \([\![a,b\vdash a\circ b ]\!]\). Once we have chosen this function—which we will abbreviate \([\![\circ ]\!]\)—we have in fact fixed the choice of \([\![\Gamma\vdash t\circ s ]\!]\) for each \([\![\Gamma\vdash t ]\!]\) and \([\![\Gamma\vdash s ]\!]\), and vice versa.

The converse is obvious. If we have chosen how to obtain \([\![\Gamma\vdash t\circ s ]\!]\) for each \([\![\Gamma\vdash t ]\!]\) and \([\![\Gamma\vdash s ]\!]\), then we simply plug in \([\![a,b\vdash a ]\!]\) and \([\![a,b\vdash b ]\!]\), which must be the projections \(\pi^2_1\) and \(\pi^2_2\), and obtain \([\![a,b\vdash a\circ b ]\!]=[\![\circ ]\!]\).

Given \([\![\Gamma\vdash t ]\!]\) and \([\![\Gamma\vdash s ]\!]\), where \(\Gamma\) has length \(n\), \([\![\Gamma\vdash t\circ s ]\!]:X^n\to X\) must be the function \(\hat x\mapsto [\![\circ ]\!]([\![\Gamma\vdash t ]\!](\hat x),[\![\Gamma\vdash s ]\!](\hat x))\). To see this, by substitution,

where \([\![\Gamma\vdash [t,s/a,b](a\circ b) ]\!]= [\![\Gamma\vdash t\circ s ]\!]\) because \(\Gamma\vdash [t,s/a,b](a\circ b)=t\circ s\). But \([\![\Gamma\vdash [t,s/a,b](a\circ b) ]\!]\) must be \(\hat x\mapsto[\![a,b\vdash a\circ b ]\!]([\![\Gamma\vdash t ]\!](\hat x),[\![\Gamma\vdash s ]\!](\hat x))\), which is what we asserted above.

Thus, modeling the \(\circ\) rule amounts to choosing a function \([\![\circ ]\!]:X\times X\to X\). Similarly, modeling \({}^{-1}\) requires a function \([\![{}^{-1} ]\!]:X\to X\), and \(\mathord{\sf{\text{e}}}\) an element \([\![\mathord{\sf{\text{e}}}]\!]\in X\).

This last one requires some explanation. As before, \([\![\cdot\vdash\mathord{\sf{\text{e}}}]\!]:X^0\to X\) is a function \(()\mapsto [\![\mathord{\sf{\text{e}}}]\!]()\) which takes an empty tuple of terms. But since there is only one empty tuple, \([\![\mathord{\sf{\text{e}}}]\!]\) always takes on the same value, so a choice of \([\![\mathord{\sf{\text{e}}}]\!]\) is simply a choice of an element of \(X\), and we say \([\![\mathord{\sf{\text{e}}}]\!]\in X\). (We call the set containing only the empty tuple \(1\), because it has one element; this notation draws an analogy with numerical exponentiation, where \(x^0=1\).)

Finally, the weakening rule

is derived from substitution, and so \([\![x_1,\cdots,x_n,x_{n+1}\vdash t ]\!]\) is

Axioms

Because an interpretation \([\![- ]\!]\) must send equal judgments to equal functions, we must verify that the constructions above satisfy the axioms required of all algebraic theories.

Reflexivity, symmetry, and transitivity are satisfied simply because ordinary mathematical equality enjoys these properties. For example, if \(\Gamma\vdash t=s\), then the model has equal functions \([\![\Gamma\vdash t ]\!]=[\![\Gamma\vdash s ]\!]\); the symmetry axiom implies \(\Gamma\vdash s=t\), and so demands simply that \([\![\Gamma\vdash s ]\!]=[\![\Gamma\vdash t ]\!]\) also.

Congruence is satisfied because equality of mathematical functions is extensional (i.e., two functions are equal when they send equal arguments to equal results). Consider the example that \(\Gamma\vdash t=t'\) should imply \(\Gamma\vdash t\circ\mathord{\sf{\text{e}}}=t'\circ\mathord{\sf{\text{e}}}\). We have seen that \([\![\Gamma\vdash t\circ\mathord{\sf{\text{e}}}]\!]=\hat x\mapsto [\![\circ ]\!]([\![\Gamma\vdash t ]\!](\hat x),[\![\mathord{\sf{\text{e}}}]\!])\) and similarly for \(t'\), but if \([\![\Gamma\vdash t ]\!]=[\![\Gamma\vdash t' ]\!]\), then these functions must be equal as well.

To see the general case, recall the congruence rule. Let \(f_i=[\![\Gamma\vdash s_i ]\!]\), \(g_i=[\![\Gamma\vdash u_i ]\!]\), and \(h=[\![x_1,\cdots,x_n\vdash t ]\!]\).

The two functions in the conclusion are, by the interpretation of substitution, \(\hat x\mapsto h(f_1(\hat x),\cdots,f_n(\hat x))\) and \(\hat x\mapsto h(g_1(\hat x),\cdots,g_n(\hat x))\). The hypotheses imply that \(f_i=g_i\) for each \(i\), so these functions are equal as well.

To summarize, a set-theoretic model of a theory is a set \(X\) and interpretation function \([\![- ]\!]\) from judgments to functions \(X^n\to X\), where the hypothesis and subsitution rules are interpreted in a particular fashion, and which obeys the remaining rules in a particular way.

In fact, this definition is sufficiently rigid that models are determined by a choice of interpretation for each function symbol, such that the axioms hold true (i.e., \([\![\circ ]\!](x,[\![\circ ]\!](y,z))= [\![\circ ]\!]([\![\circ ]\!](x,y),z)\)). This justifies our earlier statement that groups are in bijection with models of the algebraic theory of groups—a mathematical group is precisely a set equipped with such a choice of \([\![\circ ]\!],[\![{}^{-1} ]\!],[\![\mathord{\sf{\text{e}}}]\!]\) satisfying the axioms.

Posted February 17th, 2013 in Academic. Tagged: .

Leave a response: