Mfcttrf

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?

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

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_mathrmop)_mathrmop in I$ of sets $A_mathrmop$ indexed by a set $I$. We think of the elements of $I$ as the operation symbols, and $A_mathrmop$ as the arity of the operation symbol $mathrmop$. (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 $mathrmop in A$, a map $mathrmop_C : |C|^A_mathrmop| 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_mathrmop in I X^A_mathrmop$. 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_mathrmop$ 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 $mathrmop in I$, there is a point constructor $overlineop : X^A_mathrmop 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),., overlineell_i(x_1, ldots, x_n) =_X overliner_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.