# Constructive proof of existence of free algebras for infinitary equational theories

Is it constructively true that all (not necessarily finitary) equational theories $$T = (\Sigma, E)$$ have an initial model?

The usual proof for finitary equational theories I know constructs first from the signature $$\Sigma$$ the set $$P$$ of syntax trees/preterms. This set is by construction the initial model of the theory $$(\Sigma, \emptyset)$$, i.e. will usually not satisfy equations $$E$$. One then considers the congruence $$R \subseteq P \times P$$ generated by (all interpretations of) the equations in $$E$$, and proves that $$Q = P / R$$ is a model of $$T$$ and then that it is the initial one.

If $$\Sigma$$ contains an operation symbol $$f$$ of non-finitary arity $$A$$ then I struggle with defining the operations on the quotient $$Q$$. The interpretation of $$f$$ for $$Q$$ should be a function $$f_Q : Q^A \rightarrow Q$$, and should be defined in terms of the function $$f_P : P^A \rightarrow P$$ on syntax trees. If $$A$$ was finite, then any given map $$x : A \rightarrow Q$$ could be lifted along $$P \twoheadrightarrow Q$$ to a map $$x' : A \rightarrow P$$, and then $$f_Q(x)$$ could be defined as the residue class of $$f_P(x')$$ in $$Q$$. But if $$A$$ is not a choice object/set, then the proof is stuck here.

Is there a way to get around this issue without assuming choice, or is it maybe known that the existence of certain initial algebras implies some version of the axiom of choice?

EDIT: The reference pointed out by Valery Isaev contains the answer to my questions. There are models of ZF (without C) in which there is no initial algebra for a certain equational theory, in particular it cannot be proved to exist using just constructive logic. On the other hand, initial algebras exist for all theories in all Grothendieck toposes provided that AC holds in the metatheory, so all choice principles that fail to hold in some Grothendieck topos don't follow from the existence of initial algebras.

• The problem is that whether two words are equal under $E$ is undecidable. (I don't have an exact reference, but it should be a variant of the Post correspondence problem, or the undecidability of the word problem for groups.) So this may depend on the treatment of equality in your definition of initial model. – Matt F. Jul 10 '19 at 14:54
• @MattF.: actually, the bigger problem is how to avoid choice, decidability of equality does not seem to be relevant. – Andrej Bauer Jul 10 '19 at 15:54

It was proved by Andreas Blass in Words, free algebras, and coequalizers that free infinitary algebras are not constructible neither in topoi nor in ZF. It is easy to see that the existence of free algebras for all theories is equivalent to the existence of initial algebras of all theories.

Even though initial algebras do not exist in "the basic constructive mathematics", there are stronger theories in which they do exist and which still can be called constructive. For example, initial algebras can be constructed in homotopy type theory with recursive higher inductive types (see Lumsdaine, Shulman, Semantics of higher inductive types).

• Ah thanks for reminding me that this paper exists, it's very relevant! Regarding your remark on HoTT's higher inductive types, see my comment to Andrej Bauers reply. – Martin Bidlingmaier Jul 10 '19 at 19:30
• Just a short addition: A weaker version of higher inductive types suffice, namely the quotient inductive types by Altenkirch and Kaposi. – Ingo Blechschmidt Jul 10 '19 at 20:40

As was already pointed out by Valery Isaev, even in the presence of excluded middle initial algebras for equational theories need not exist. I would like to explain a bit what is needed from a constructive point of view.

Suppose $$T = (\Sigma, E)$$ is an equational theory where $$\Sigma$$ is a family $$\Sigma = (A_\mathrm{op})_{\mathrm{op} \in I}$$ of sets $$A_\mathrm{op}$$ indexed by a set $$I$$. We think of the elements of $$I$$ as the operation symbols, and $$A_\mathrm{op}$$ as the arity of the operation symbol $$\mathrm{op}$$. (Normally arities are natural numbers, but since we allow infinitary operations it is better for arities to be general sets.)

A $$T$$-algebra $$C$$ is given by a carrier set $$|C|$$ and, for each $$\mathrm{op} \in A$$, a map $$\mathrm{op}_C : |C|^{A_\mathrm{op}}| \to |C|$$, such that the equations $$E$$ are satisfied.

A natural way of constructing the initial $$T$$-algebra is as follows:

1. Construct the set of well-founded trees $$W_T$$ whose branching types are $$\Sigma$$, i.e., the initial algebra for the polynomial functor $$X \mapsto \Sigma_{\mathrm{op} \in I} X^{A_\mathrm{op}}$$. This is also known as a $$W$$-type.

2. Quotient $$W_T$$ by the (interpretations of) equations $$E$$ to obtain a candidate for the initial algebra.

We cannot get either step for free, but in general the first step is the easier one, as it is well understood what it takes to have $$W$$-types in a constructive setting.

For the second step to go through, one needs to resolve the question posed by the OP, namely, how do we lift operations from the quotient $$W_T/E$$ to $$W_T$$? It looks like we need choice. Indeed, it suffices for all the arities $$A_\mathrm{op}$$ to satisfy choice (to be choice sets, also called projective objects), but is that necessary? I do not know of any way of avoiding choice if one attempts to construct the initial algebra as a quotient of an inductively defined set.

Homotopy type theory offers an alternative. We avoid stratifying the construction of the initial algebra into an inductive construction followed by a quotient. Instead, we make a purely inductive construction: the initial $$T$$-algebra is the higher-inductive type $$X$$ with the following constructors:

• for each $$\mathrm{op} \in I$$, there is a point constructor $$\overline{op} : X^{A_\mathrm{op}} \to X$$;
• for each equation $$\ell_i(x_1, \ldots, x_n) = r_i(x_1, \ldots, x_n)$$ in $$E$$ there is a path constructor $$e_i : \prod (x_1, \ldots, x_n : X)\,.\, \overline{\ell}_i(x_1, \ldots, x_n) =_X \overline{r}_i(x_1, \ldots, x_n)$$,
• set-truncation: for all $$x, y \in X$$ and all paths $$p, q : x =_X y$$ there is a path $$\tau_{p,q} : p =_{x =_X y} q$$.

For further reference, look at the HoTT book chapter on the real numbers, where a variant of such a construction is used to present the Cauchy completion of rational numbers in an inductive fashion.

• Thanks for the thorough answer. Do you know whether the existence of initial algebras is equivalent to some version of choice? – Martin Bidlingmaier Jul 10 '19 at 19:02
• Regarding HoTT's higher inductive types: As I understand their semantics is not completely resolved. HoTT has a model in every infinity topos, and HoTT's hsets correspond to 0-truncated objects. The subcategory of 0-truncated objects of an infinity topos is a 1-topos, and every 1-topos arises in this way. So the logic of HoTT's hsets is essentially just the internal logic of Grothendieck 1-toposes. But then if not every Grothendieck 1-topos has initial models (because choice might fail), HoTT shouldn't prove that they exist. So HoTT shouldn't include general HITs. Am I overlooking something? – Martin Bidlingmaier Jul 10 '19 at 19:15
• Ah, so it appears that any Grothendieck topos relative to a topos satisfying AC has initial algebras of all equational theories (Rosebrugh, Abstract families of algebras), so this argument doesn't rule out models of arbitrary HITs in (Grothendieck) infinity toposes. – Martin Bidlingmaier Jul 10 '19 at 19:43
• I have no definitive answers regarding semantics of HoTT. I find it reasonable to take HITs as a primary notion, on the grounds that they extend inductive constructions. Certainly they’re no more suspect than the axiom of choice. – Andrej Bauer Jul 11 '19 at 10:54
• @MartinBidlingmaier Right -- since all Grothendieck toposes over a topos with AC have initial algebras, but don't satisfy choice, the existence of initial algebras doesn't imply choice. What seems more likely to me is that the existence of initial algebras might be equivalent to the existence of sufficiently large regular ordinals, e.g. something like the "regular extension axiom" -- note that Blass's proof proceeds by way of constructing an uncountable regular cardinal and observing that (modulo a large cardinal hypothesis) ZF cannot construct such a thing. – Mike Shulman Jul 11 '19 at 13:10