Constructive proof of existence of free algebras for infinitary equational theories

Question

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.

Answer 1

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).

Answer 2

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.