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.

  • $\begingroup$ There should be varieties with nonrecursive (but r.e.) equational theories. Short of doing computations in a finitely generated relatively free algebra, I am not sure how to answer your question when it can be answered at all. Gerhard "Equational Proof Is Just Equations" Paseman, 2020.02.25. $\endgroup$ Feb 26, 2020 at 0:41
  • $\begingroup$ It is an old theoren of Jacobson that if R if a ring satisfying the equation $x^n=x$ is commutative. The prof uses subdirect products and structure of division rings. There are very few examples of $n$ where an equational proof of commutativity is known. Birkhoff’s proof uses choice I believe and doesn’t really tell you how to get equations. $\endgroup$ Feb 26, 2020 at 0:44
  • $\begingroup$ @BenjaminSteinberg Actually, I have an equational proof for infinitely many $n$. :-) $\endgroup$ Feb 26, 2020 at 7:29
  • $\begingroup$ @GerhardPaseman: I do not think there is a known variety of rings with undecidable equational theory. Ring varieties behave much better than group or semigroup varieties. $\endgroup$
    – user6976
    Feb 26, 2020 at 8:32
  • 1
    $\begingroup$ I was wrong. Alexei Kanel-Belov does not know a purely syntactic proof. Says that he would be interested to see such a proof for infinitely many $n$, What can be easily proved syntactocally. is that the Jacobson radical of such rings is trivial. $\endgroup$
    – user6976
    Feb 26, 2020 at 12:13

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

  • $\begingroup$ Thank you! So my guess was correct. $\endgroup$ Feb 26, 2020 at 7:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.