---
tag: 35G4HQG2FN
kind: statement
role: theorem
name: Baker's finite basis theorem
msc: [08B05, 08B10]
uses: [YGYZAQ12MZ, 9GZ7F6ETC6, AJNZJD8442]
about: [YGYZAQ12MZ, 9GZ7F6ETC6]
sources:
  - url: https://en.wikipedia.org/wiki/Congruence_lattice_problem
---

## Statement

Let $A$ be a finite algebra of a finite signature with only function symbols.
Assume that the [[variety|AJNZJD8442]] generated by $A$ is [[congruence-distributive|9GZ7F6ETC6]].
Then $A$ is [[finitely based|YGYZAQ12MZ]].

## Remarks

Kirby Baker proved the theorem in 1977.
One ingredient is Jónsson's lemma, which shows that the subdirectly irreducible algebras in the variety generated by $A$ are quotients of subalgebras of $A$, so they are finite and few.
The other ingredient is the Jónsson terms of a congruence-distributive variety, which Baker used to find finitely many identities that axiomatise the variety.

Example: every finite lattice is finitely based, since lattices form a congruence-distributive variety.
The same holds for every finite Boolean algebra and every finite Heyting algebra, since these have lattice reducts and so generate congruence-distributive varieties.

The finite signature is needed.
Let $A$ be the two-element lattice $\set{0, 1}$ with infinitely many extra unary operations $f_1, f_2, \ldots$, all equal to the identity map.
It has a lattice reduct, so it generates a congruence-distributive variety, and it satisfies $f_i(x) \approx x$ for every $i$.
A finite set $\Sigma$ of identities of $A$ mentions only the $f_i$ with $i$ in some finite set $S$.
Change $A$ by letting $f_j$ be the constant map with value $0$ for every $j \notin S$.
The new algebra still satisfies $\Sigma$, but it fails $f_j(x) \approx x$ at $x = 1$, so $\Sigma$ is not an equational basis of $A$.

## Explanations

### L1 human

The theorem gives a large family of finite algebras whose laws follow from finitely many of them.
It applies whenever the congruences of the algebras in the variety behave like a distributive lattice, as they do for lattices and Boolean algebras.
So every finite lattice can be described by finitely many laws.

### L2 human

Baker's theorem is one of the main positive answers to Tarski's finite basis problem.
It extends McKenzie's earlier result that finite lattices are finitely based.
It was later generalised by McKenzie to congruence-modular varieties with a finite residual bound, and by Willard to congruence meet-semidistributive varieties with a finite residual bound.
These results are steps towards Park's conjecture, which predicts that a finite algebra of finite signature that generates a variety with a finite residual bound is finitely based.