Birkhoff's completeness theorem (see here, Theorem 14.19) states that an equation which is true in all models of an algebraic theory can be proven in equational logic.

**Question.** Does the proof of Birkhoff's completeness theorem actually *produce* for each specific equation a proof in equational logic? If yes, can you please demonstrate this with an instructive example?

Actually, I suspect that the answer is "No", but I am not entirely sure.

Let us look at the following well-known statement: If $R$ is a ring in which every element $r \in R$ satisfies $r^2=r$ (i.e. $R$ is boolean), then $R$ is commutative. There is the following overkill proof: $R$ is reduced, hence a subdirect product of domains $R_i$. Since the maps $R \to R_i$ are surjective, each domain $R_i$ satisfies the same equation and then must be isomorphic to $\mathbb{F}_2$. In particular, $R_i$ is commutative. Since $R \to \prod_{i \in I} R_i$ is injective, it follows that $R$ is commutative. So by Birkhoff's theorem, there *must be some* equational proof of this. My question is not how an equational proof looks like - this is just a basic algebra exercise. I would like to see how (if possible) it can be extracted from the overkill proof.

I think the proof of Birkhoff's theorem in this special case works as follows: Consider the free ring on two generators $\mathbb{Z}\langle X,Y\rangle$ and take the quotient with respect to the relations $r^2=r$ for all elements $r$. This is the free boolean ring $R$ on two generators. By the overkill proof, $XY=YX$ holds in $R$. This means that $XY=YX$ can be derived from the relations $r^2=r$ in $\mathbb{Z}\langle X,Y\rangle$. But we don't *get* a derivation, right? How to produce, for example, the following equation?

$$\begin{align*}
XY - YX &= \bigl((X+Y)^2 - (X+Y)\bigr) - \bigl(X^2-X\bigr) - \bigl(Y^2-Y\bigr) \\
&\phantom{=}+ \bigl((YX)^2 - (YX)\bigr) - \bigl((-YX)^2 - (-YX)\bigr),
\end{align*}$$
As far as I can tell, we are not even guaranteed a priori to have a proof which works without the axiom of choice, since this is used in the structure theorem for reduced rings in the overkill proof? (At first this might be confusing since the axiom of choice is surely not allowed in an equational proof, but actually the axiom of choice is used to show the *existence* of an equational proof.)

I am interested in more complicated applications of Birkhoff's theorem. This here is just an example to get started. You can also choose other examples if they are more instructive.

6more comments