Model-Theoretic Connections

Semantic Embeddings and Undecidability

To prove a theory undecidable, embed a known undecidable theory into it algebraically. The technique needs no recursion theory at all — the encoding does the work.

Engineering · Mathematics5 min readKV-MATH-0256

Learning objectives

Define a semantic embedding and state what it transfers.
Explain why the technique needs no familiarity with algorithms.
Identify the standard source theories used for encoding.
Contrast with the positive decidability results for discriminator varieties.
State the Burris–McKenzie classification of decidable modular varieties.
List the decidability problems the source records as open.

01The technique

A semantic embedding interprets the models of one theory inside the models of another, uniformly and definably, so that decidability transfers backwards and undecidability forwards.

ProcedureProving a theory undecidable by semantic embedding

in: undecidable source theory and an interpretation → out: undecidability of Th(K)

input: target class K whose first-order theory is to be shown undecidable
choose a source theory T known to be undecidable
(graphs, semigroups, or the word problem for groups)
construct, for each model M of T, an algebra A_M ∈ K
construct first-order formulas interpreting M inside A_M:
a formula defining the universe of M as a definable subset of A_M
formulas defining the relations and operations of M
verify uniformity: the same formulas work for every M
then any sentence of T translates to a sentence about K
a decision procedure for Th(K) would decide T — contradiction
conclude: Th(K) is undecidable

Correctness: the translation is computable, so decidability of the target would give decidability of the source. Caveat: the interpretation must be uniform across models — a per-model construction proves nothing.

Key resultNo recursion theory required

The source stresses that this technique is essentially algebraic and requires no familiarity whatsoever with the theory of algorithms. The undecidability of the source theory is imported as a black box; all the work is in constructing the interpretation, which is a purely algebraic exercise.

02Standard source theories

What gets encoded
Source	Undecidable since	Typically used for
Word problem for semigroups	Markov and Post, 1947	semigroup and monoid varieties
Word problem for groups	Novikov, 1955	group varieties
Theory of graphs	classical	general algebraic structures
Equational theory of relation algebras	Tarski, 1953	algebras of logic
Unary algebras	Mal'cev	very weak signatures
Finitely based semigroup varieties	Murskiĭ, 1968	equational undecidability

Graphs are the most flexible source because a graph is a minimal structure — one binary relation — so interpreting a graph inside an algebra requires only that the algebra have enough definable structure to encode adjacency.

03Results the source reports

1954–1978
Group varieties
Szmielew, Ershov and Zamjatin: a variety of groups is decidable if and only if it is abelian.
1976
Ring varieties
Zamjatin: a variety of rings has a decidable theory iff it is generated by a zero-ring and finitely many finite fields.
1979
Discriminator varieties — positive
Burris and Werner: every finitely generated discriminator variety of finite type has a decidable theory.
1981
The modular classification
Burris and McKenzie: if a locally finite congruence-modular variety has a decidable theory then it is of the form (discriminator) ⊗ (modular Abelian).
1982
Strengthened group result
McKenzie: any class of groups containing P_S(G) for a non-abelian G has an undecidable theory.

The pattern the source identifies is a long-standing conviction among researchers that positive decidability and good structure theory go hand in hand. Every decidable case turns out to have a structural description, and the modular classification makes that precise for a large class.

04The Burris–McKenzie classification

The strongest result the source reports ties decidability to the structural decomposition of Chapter IV.

Key resultThe classification

If a locally finite congruence-modular variety has a decidable first-order theory, then it is of the form (discriminator) ⊗ (modular Abelian). Moreover there is an algorithm which, given a finite set K of finite algebras of finite type, decides whether V(K) is of this form; and if so, constructs a finite ring R with 1 such that V(K) is decidable iff the variety of unitary left R-modules is.

Structure implies the form
Decidability forces the variety into the two-part decomposition — a discriminator piece and a module-like piece.
The form is recognisable
An algorithm decides membership in the class, so the structural question is itself decidable.
Decidability reduces to modules
The remaining question is whether the module variety over a constructed finite ring is decidable — a question about ring theory rather than universal algebra.
What is not settled
Which finite rings give decidable module varieties. The reduction is complete; the reduced problem is not.

05The open problems recorded

Decidability problems in the source's closing survey
Problem	Statement
3	Which locally finite varieties of finite type have a decidable theory?
4	For which varieties of finite type is the theory of the finite algebras in the variety decidable?
5	Do the finite algebras in any finitely generated arithmetical variety of finite type have a decidable theory?
6	Do the finite algebras in any finitely generated congruence-distributive but not congruence-permutable variety of finite type have an undecidable theory?
7	Is there an algorithm deciding which equations in at most 4 variables hold in modular lattices?
9	Can the Linial–Post theorem be derived from base undecidability for Boolean algebras, or conversely?
10	Is there an algorithm to determine whether V(A) has a finitely based equational theory, for A finite of finite type?

Problem 7 is notable for its precision: Freese proved in 1979 that no algorithm decides which equations in at most 5 variables hold in modular lattices, and the 3-variable case is decidable from Dedekind's description of the free modular lattice on 3 generators. The 4-variable case sits exactly in the gap.

06The general lesson

Undecidability

Encode something hard

Semantic embedding. Algebraic work, no recursion theory. Applies whenever the target has enough definable structure.

Decidability

Find enough structure

Requires a genuine structure theorem — Boolean product representation, quantifier elimination, or reduction to a known decidable theory. Much harder to obtain.

NoteWhy undecidability is the common outcome

Most varieties have enough definable structure to encode graphs, so most are undecidable. Decidability is the exception and always comes with a structure theorem attached. This asymmetry is why the positive results — discriminator varieties, abelian group varieties — are so prized, and why they cluster in exactly the well-behaved classes Chapter IV identified.

Frequently asked

Does semantic embedding prove undecidability of the equational theory too?

Not automatically. Embedding a first-order theory gives first-order undecidability. Equational undecidability is a stronger statement requiring the encoding to work at the level of identities, which is harder and is the content of results such as Murskiĭ's for semigroups and Tarski's for relation algebras.

Is a decidable variety necessarily well behaved structurally?

The Burris–McKenzie result makes this precise for locally finite congruence-modular varieties: decidability forces the two-part decomposition. Outside that setting the conviction that decidability and structure coincide is a working hypothesis rather than a theorem, and the source presents it as such.

Which of these problems have been resolved since 1981?

Several, and the collection does not state the outcomes on this page because the source records them as open and reporting otherwise here would misrepresent the text. The Research Frontier stream reviews the seventeen problems as a set and reports current status, marked explicitly as postdating the 1981 edition.

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.