Terms, Free Algebras and Equational Logic

Fully Invariant Congruences and Equational Theories

Equational theories are fully invariant congruences on the term algebra. The lattice of varieties is that lattice upside down.

Engineering · Mathematics4 min readKV-MATH-0223

Learning objectives

Define full invariance and distinguish it from ordinary congruence.
Identify equational theories with fully invariant congruences on T(X).
State the dual isomorphism between theories and varieties.
Describe the lattice of varieties of a given type.
Define an equational basis and the finite basis property.
Recognise where the lattice of varieties is understood and where it is not.

01Full invariance

A congruence θ on an algebra A is fully invariant when it is preserved by every endomorphism of A.

⟨a, b⟩ ∈ θ ⟹ ⟨ε(a), ε(b)⟩ ∈ θ for every endomorphism ε of A

Ordinary congruences need only be compatible with the operations. Full invariance is strictly stronger and is not automatic.

On the term algebra T(X), endomorphisms are exactly substitutions: a map sending each variable to a term, extended by the universal property. So a fully invariant congruence on T(X) is a congruence closed under substitution — precisely the closure conditions of equational logic.

02Equational theories are fully invariant congruences

Direction 1

Theories are fully invariant

Id(K) is a congruence on T(X) by the first four inference rules and fully invariant by substitution. So every equational theory is a fully invariant congruence.

Direction 2

Fully invariant congruences are theories

Given such a congruence θ, the quotient T(X)/θ generates a variety whose identities are exactly θ. So every fully invariant congruence arises as a theory.

Conclusion

An exact correspondence

Equational theories of type F over a countably infinite X correspond bijectively to fully invariant congruences on T(X).

Key resultCon<sup>FI</sup>(T(X)) is the object of study

The lattice of fully invariant congruences on the term algebra is a complete lattice, and it is dually isomorphic to the lattice of varieties of that type. Studying varieties and studying this lattice are the same activity.

03The lattice of varieties

Varieties of a fixed type form a complete lattice under inclusion, dually isomorphic to the lattice of equational theories.

Operations in the lattice of varieties
Operation	On varieties	On theories
Order	V ⊆ W	Id(V) ⊇ Id(W)
Meet	V ∩ W	the theory generated by Id(V) ∪ Id(W)
Join	V ∨ W = HSP(V ∪ W)	Id(V) ∩ Id(W)
Bottom	trivial variety (one-element algebras)	all equations
Top	all algebras of the type	only trivial equations

Meets are easy on the variety side and joins are easy on the theory side, which is the usual consequence of a dual isomorphism. In practice the join of two varieties is the harder computation, and is often approached through the theory side.

04Equational bases

An equational basis for a variety is a set Σ with M(Σ) = V. A variety is finitely based when a finite basis exists.

Finitely based

A finite axiom list suffices

Groups, lattices, Boolean algebras, rings. The variety is fully specified by finitely many equations.

Inherently non-finitely based

No finite basis exists

Some finite algebras generate varieties with no finite equational basis, and moreover no finitely based variety between them and the trivial one behaves correctly.

CautionFinite algebra does not imply finite basis

It is tempting to assume a variety generated by a single finite algebra must be finitely axiomatisable. It need not be. Lyndon produced a seven-element algebra generating a non-finitely based variety, and the general question — Tarski's finite basis problem, Problem 10 in the source's list — was open in 1981 and is addressed in the Research Frontier stream.

05Known finite basis theorems

1970s
Baker's theorem
A finite algebra generating a congruence-distributive variety is finitely based. This is one of the three finite basis theorems in the source's Chapter V.
1970s
Jónsson's contributions
Congruence-distributivity yields strong control over subdirectly irreducibles via Jónsson's lemma, which is what makes Baker's theorem possible.
1980s
Congruence-modular extensions
Later work extended finite basis results into the congruence-modular setting using the commutator.
Post-source
The general problem resolved negatively
The question of whether Tarski's finite basis problem is decidable was settled after the source was written — see the Research Frontier stream, where this is flagged as beyond the 1981 text.

06How much of the lattice is understood

The lattice of varieties of a given type is enormous and mostly uncharted. What is known is concentrated in small types and in well-behaved regions.

Lattice varieties
The lattice of varieties of lattices is understood at the bottom: the trivial variety, distributive lattices, then a rich structure above.
Group varieties
Extensively studied, with a substantial literature of its own. The Burnside problems live here.
Semigroup varieties
Very large and largely unclassified. Undecidability results abound.
Types with one binary operation
Even here the lattice of varieties is of the cardinality of the continuum, so no complete classification is possible.

Because complete classification is out of reach, the working programme is to classify by properties — congruence conditions, decidability, structure theory — rather than to enumerate. That is the programme the rest of this collection follows.

Frequently asked

Is every congruence on T(X) fully invariant?

No. Ordinary congruences on the term algebra correspond to arbitrary quotients; fully invariant ones correspond to equational theories. The principal congruence generated by a single pair of terms is generally not fully invariant, since substitution instances of that pair need not be related.

Does the number of variables in X matter?

For the correspondence, X must be countably infinite so that every identity is expressible. With finitely many variables one obtains the theory restricted to that many variables, which is a coarser object and can behave differently — Freese's result on modular lattices distinguishes the 4-variable and 5-variable cases.

How do I show a variety is not finitely based?

Typically by exhibiting, for each n, an algebra satisfying all identities of the variety in at most n variables but failing some identity of the variety. That family witnesses that no finite subset of the theory can axiomatise it. Constructing such families is the hard part and is specific to each case.

Sources and further reading

S. Burris and H. P. Sankappanavar, A Course in Universal Algebra, Millennium Edition (a corrected re-typesetting of Springer GTM 78, 1981).
G. Grätzer, Universal Algebra, 2nd edition, Springer.
R. McKenzie, G. McNulty and W. Taylor, Algebras, Lattices, Varieties, Volume I.

Original KEVOS® explanatory article. Written from the topic map of the cited works; no text is reproduced from them.