McKenzie's undecidability of the finite basis problem

Remarks

The second sentence implies the first, because the halting problem is undecidable. So this theorem gives a negative answer to Tarski's finite basis problem. McKenzie published the proof in 1996. McKenzie built his algebra from a simpler finite algebra that encodes the computation of $T$. The proof relates the halting of $T$ to the sizes of the subdirectly irreducible algebras in the variety generated by this simpler algebra. McKenzie also used the simpler algebra to show that it is undecidable whether a finite algebra generates a variety with a finite residual bound. Willard later proved that the simpler algebra itself is finitely based if and only if $T$ halts, which gives a shorter route to the theorem.

Going deeper

For a student

The theorem closes a question that had driven much of the work on finite bases since the 1950s. It shows that results such as Baker's finite basis theorem, which give finite bases under structural hypotheses, cannot be replaced by a general decision procedure. The construction of $A(T)$ links equational logic with residual bounds of varieties, which is also the setting of Park's conjecture.