Connections with Model Theory

Baker's Finite Basis Theorem

The theorem that every finitely generated congruence-distributive variety of finite type has a finite equational basis — the deepest result in the source's final chapter.

Category Engineering / MathematicsSource V.4Pages 265-271Reading 2 minReviewed 2026-08-07

Learning objectives

State Baker's theorem and its hypotheses
Follow the proof strategy
Assess the sharpness of each hypothesis

The statement

Baker's finite basis theorem

Let A be a finite algebra of finite type. If V(A) is congruence-distributive, then V(A) has a finite equational basis.

More generally, any finitely generated congruence-distributive variety of finite type is finitely based. No assumption of definable principal congruences is needed.

Immediate coverage

The theorem applies to every finitely generated variety of lattices, distributive lattices, Boolean algebras, Heyting algebras, and every discriminator variety generated by a finite algebra. That is a very large class of the varieties of practical interest.

The proof strategy

Jónsson's lemmaSubdirect irreducibles of V(A) lie in HS(A) — finitely many, all finite

Definable principal subcongruencesWithin any principal congruence, a smaller one is definably located

Bound the variablesIdentities beyond a computable number of variables add nothing

Finite typeFinitely many identities remain; they form a basis

Definition — Definable principal subcongruences

A variety has DPSC if there is a formula that, given a non-trivial principal congruence, definably identifies a non-trivial principal congruence inside it of a controlled form.

DPSC is strictly weaker than DPC. Lattices have DPSC without having DPC, which is exactly why Baker's theorem covers lattices while the earlier theorems do not.

Baker's original proof and later simplifications

Baker's 1977 proof was long and technical. Jónsson later gave a substantially shorter argument, and Willard's 2000 finite basis theorem generalises the result to congruence-meet-semidistributive varieties with a bounded residual character. The source presents the theorem within the framework of Chapter V §3.

Sharpness of the hypotheses

Dropping each hypothesis
Hypothesis dropped	Result
Finite type	Fails — infinitely many operation symbols give infinitely many candidate identities
Finitely generated	Fails — infinitely generated varieties can be non-finitely-based
Congruence-distributive	Fails — Lyndon's example is a finite algebra generating a non-finitely-based variety
All present	Baker's theorem applies

Congruence-modular is not enough

The theorem genuinely requires distributivity. There are finite algebras generating congruence-modular varieties with no finite basis. The gap between modular and distributive appears here as sharply as anywhere in the subject.

For congruence-modular varieties, McKenzie's finite basis theorem supplies a partial substitute under an additional residual smallness hypothesis, but it is later than the source.

Consequences and context

Decidability of the equational theory. A finite basis plus finitely many finite irreducibles gives a decision procedure for identities.
Finitely many subvarieties. Already available from Jónsson's lemma, but the finite basis makes each subvariety finitely axiomatisable too.
Practical axiomatisation. Algebraic specification languages require finite axiom sets; Baker's theorem certifies their availability for a wide class.
Contrast with Tarski's problem. Baker gives a sufficient condition; McKenzie's 1996 undecidability result shows no decidable necessary and sufficient condition can exist.

Attribution

Baker's theorem (1977) is contemporaneous with the source and is presented there. Willard's generalisation (2000), McKenzie's undecidability result (1996) and McKenzie's congruence-modular finite basis theorem are later work, noted here for context and not attributed to Burris and Sankappanavar.

Frequently asked questions

Does Baker's theorem give an explicit basis?

The proof is effective in principle — it bounds the number of variables needed and the identities in that many variables can be enumerated. In practice the bounds are large and explicit bases are usually found by other means.

Is there a converse?

No. Many finitely based varieties are not congruence-distributive — abelian groups, for instance, are finitely based and congruence-modular but not distributive.

Source. S. Burris and H. P. Sankappanavar, A Course in Universal Algebra, The Millennium Edition — a corrected re-typesetting of Springer-Verlag Graduate Texts in Mathematics 78 (1981). Section V.4, book pages 265-271.

This page is an original exposition prepared for the KEVOS® knowledge library. It restates and reorganises mathematical results; it is not a reproduction of the source text.