How much choice is needed to prove the completeness of equational logic?

Question

All the proofs of the completeness of (Birkhoff's) equational logic I have read seem to pick representatives for equivalence classes of terms and hence require the axiom of choice. Is AC (or a weak version) necessary to prove that theorem?

Answer 1

I do not know what proofs precisely you have in mind, but at least for operations with finite arities no choice is needed, nor excluded middle for that matter. Let us review the proof to make sure this is the case.

Consider a signature $\Sigma = (\mathsf{op}_i : n_i)_{i \in I}$, indexed by an arbitrary set $I$, where each operation $\mathrm{op}_i$ has arity $n_i \in \mathbb{N}$. Let $T$ be the set of all terms built inductively as:

• variable symbols $x_0, x_1, x_2, \ldots$
• if $t_1, \ldots, t_{n_i} \in T$ then $\mathrm{op}_i(t_1, \ldots, t_{n_i}) \in T$.

Let $E$ be a set of equalities of the form $t = u$, where $t, u \in T$. We consider the equational theory (the deductive closure) of $E$. Write $t \cong u$ for provable equality, i.e., for any $t, u \in T$, $$t \cong u \iff E \vdash t = u.$$ Clearly, $\cong$ is an equivalence relation.

If we can show that the quotient set $A \mathrel{{:}{=}} T/\cong$ is a $\Sigma$-algebra that satisfies the equations $E$, we will be able to prove Birkhoff's theorem because equality in $A$ coincides with provable equality with respect to $E$.

So let us be careful about showing that $A$ is a $\Sigma$-algebra. For any $i \in I$, we must interpret $\mathrm{op}_i$ as some map $f_i : A^{n_i} \to A$, which we do as follows (this is the place where choice seemingly appears):

Given equivalence classes $\xi_1, \ldots, \xi_{n_i} \in A$, there exist terms $t_1 \in \xi_1, \ldots, t_{n_i} \in \xi_{n-1}$. Define $f_i(\xi_1, \ldots, \xi_{n_i}) = [\mathrm{op}_i(t_1, \ldots, t_{n_i})]_{\cong}$.

It is easy to check that the above definition of $f_i$ is well-formed. Crucially, we did not use any choice! We used $n_i$ applications of $\exists$-elimination. If we allowed operations with non-finite arities, then we would be in a pickle – but finitely many choices can be done without appeal to the axiom of choice, one only needs induction on $\mathbb{N}$.

$\newcommand{\sem}[1]{[\![#1]\!]}$ Second, let us verify that $A$ satisfies any equation $t = u$ in $E$. Suppose $x_1, \ldots, x_k$ are the variables appearing in the terms $t$ and $u$. Let $\nu : \{x_1, \ldots, x_k\} \to A$ be an assignment of values to the variables. There are terms $s_1, \ldots, s_k \in A$ such that $\nu(x_i) = [s_i]_{\cong}$ for $i \in \{1, \ldots, k\}$. (Again, this step does not require any choice, it is an $k$-fold application of the logical rule of $\exists$-elimination.) Let $\sigma = [s_1/x_1, \ldots, s_k/x_k]$ be the substutution which replaces $x_i$ with $s_i$, and write $\sigma(t)$ for the application of $\sigma$ to a term $t$.

Let $\sem{t}_\nu, \sem{u}_\nu \in A$ be the interpretations of $t$ and $u$ in $A$ with respect to the valuation $\nu$. Observe that $$\sem{t}_\nu = [\sigma(t)]_{\cong}, \qquad\qquad \sem{u}_\nu = [\sigma(u)]_{\cong}.$$ Moreover, because $t = u$ is in $E$, $E$ proves the instance $\sigma(t) = \sigma(u)$, from which we get $$\sem{t}_\nu = [\sigma(t)]_{\cong} = [\sigma(u)]_{\cong} = \sem{u}_\nu,$$ as required.

So, no choice and no excluded middle for finite arities. For infinite arites one can either use choice, or cross over to the Dark Side and use homotopy type theory, where the Lindenbaum-Tarski algebra can be constructed without choice using a higher inductive-inductive type.