---
tag: KRM89R0T28
kind: statement
role: theorem
name: McKenzie's undecidability of the finite basis problem
msc: [08B05, 03D35, 03B25]
uses: [AB22FWBQ0M, YGYZAQ12MZ, 758EYCN27B, Z7TN2B35B0]
about: [AB22FWBQ0M, YGYZAQ12MZ]
sources:
  - url: https://doi.org/10.1142/S0218196796000040
---

## Statement

There is no algorithm that decides, for an arbitrary finite algebra $A$ of finite signature given by its operation tables, whether $A$ is [[finitely based|YGYZAQ12MZ]].
More precisely, there is an effective construction that assigns a finite algebra $A(T)$ of finite signature to each [[Turing machine|758EYCN27B]] $T$.
It has this property: $T$ halts, started on the empty tape, if and only if $A(T)$ is finitely based.

## Remarks

The second sentence implies the first, because the [[halting problem|Z7TN2B35B0]] is undecidable.
So this theorem gives a negative answer to [[Tarski's finite basis problem|AB22FWBQ0M]].
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.

## Explanations

### L1 human

Some finite algebras have all their laws captured by a finite list, and others do not.
The theorem says that no computer program can sort finite algebras into these two kinds.
It is proved by hiding a computer program inside a finite algebra so that the algebra has a finite list of laws exactly when the program stops.

### L2 human

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.