Birkhoff's completeness theorem put into practice

Question

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.

Answer 1

Let me try to restate the question.

I consider an identity to be a pair, written $(s,t)$ or $s\approx t$. I also consider a set of identities to be a set of pairs.

Birkhoff's Theorem compares three things, namely
(1) $\Sigma\models s\approx t$,
(2) The pair $(s,t)$ belongs to the fully invariant congruence $\Theta^{T(X)}(\Sigma)$ on the term algebra $T(X)$, and
(3) $\Sigma\vdash s\approx t$.

I think the question is asking whether it is possible to extract from the proof of Birkhoff's Theorem and from a specific instance of $\Sigma\models s\approx t$ a proof witnessing that $\Sigma \vdash s\approx t$.

The proof of Birkhoff's theorem does explain why (1) $\Leftrightarrow$ (2). Also, if we are told HOW the pair $(s,t)$ is generated as a member of $\Theta^{T(X)}(\Sigma)$, that can be translated into a $\Sigma$-proof of $s\approx t$. What is missing is: given the knowledge that $(s,t)\in\Theta^{T(X)}(\Sigma)$, do we know how the pair $(s,t)$ got into $\Theta^{T(X)}(\Sigma)$? The proof of Birkhoff's Theorem does not require this missing ingredient, it only requires that if $(s,t)$ is in $\Theta^{T(X)}(\Sigma)$, then it was generated in some way. So the answer to the question in the form it was asked (can we extract a $\Sigma$-proof of $s\approx t$ from the proof of Birkhoff's Theorem?) has to be No.

You could try asking a slightly different question: Suppose, given finite $\Sigma$, that we are told that $\Sigma \models s\approx t$. By B's Theorem we know there must exist a $\Sigma$-proof of $s\approx t$. Question: can we estimate an upper bound on the complexity of such a proof?

An affirmative answer would imply that any finitely axiomatizable variety has a decidable equational theory. But we know this to be false, since in the 1940's Tarski found a finitely axiomatizable variety of relation algebras with an undecidable equational theory. Many other examples are known now.

Answer 2

The proof of Birkhoff's theorem, much like the proof of the completeness theorem for predicate logic, will not give a very interesting algorithm for computing a proof for a statement known to be valid: it will essentially consist of a naive proof search which, for a valid statement, will terminate. But as Keith Kearnes wrote, there cannot be a computable bound for the size of a proof in the size of the statement.

However, note that Birkhoff's theorem uses only the truth of the statement under consideration. It does not use any information contained in any of the known proofs of the statement. In proof theory there are techniques for using this information, in particular Gentzen's cut-elimination theorem. It provides a proof transformation which, in some sense, allows to remove notions for a proof which do not appear in the theorem it shows. Famous applications of the cut-elimination theorem to mathematical proofs are Girard's transformation of the Fürstenberg-Weiss proof of van der Waerden's theorem into the original proof [1, annex 4.A] and Luckhardt analysis of Roth's theorem about approximations of irrational numbers [2]. A strongly related line of work is proof mining [3] which focuses on the extraction of functionals and bounds from proofs.

Instead of applying Birkhoff's theorem, it may be more fruitful to apply such proof-theoretic techniques since they also allow to leverage the proof of the statement under consideration.

[1] J.Y. Girard: Proof Theory and Logical Complexity. In Studies in Proof Theory, Bibliopolis, Napoli, 1987.

[2] Horst Luckhardt. Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken. Journal of Symbolic Logic, 54(1):234–263, 1989.

[3] Ulrich Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer, 2008.