Trakhtenbrot’s Theorem and the Finite Model Boundary

First-order logic has no decision procedure for validity. That is Church’s theorem, and it is usually proved by showing that a sentence can encode the computation of a Turing machine. A natural response is to restrict attention to finite structures, on the grounds that infinite domains are a mathematical idealisation and every real database, every real program state, and every real hardware configuration is finite. Trakhtenbrot’s theorem says the restriction does not help: the set of sentences true in all finite structures is undecidable too. What makes the pair interesting is that the two undecidability results have different shapes, and the difference exposes exactly what compactness buys.

Two validity notions that are not the same set

Fix a relational signature: finitely many relation symbols with fixed arities, no function symbols, and equality. A structure for the signature is a nonempty set called the domain together with an interpretation of each relation symbol as a set of tuples of the appropriate arity. A sentence is a formula with no free variables.

Val is the set of sentences true in every structure. FinVal is the set of sentences true in every finite structure. Since every finite structure is a structure, FinVal contains Val, and the inclusion is strict. A single sentence over one binary relation separates them: require the relation to be a strict linear order with a first element, no last element, and an immediate successor for every element. A finite linear order always has a last element, so the sentence has no finite model and is therefore vacuously true in all finite structures. The naturals under < satisfy it, so it is not true in all structures.

One further fact about the gap is needed later, and it is a compactness argument. If a sentence has finite models of every size, it has an infinite model: add axioms forcing at least n elements for each n, observe that every finite subset is satisfiable, and apply compactness. Contrapositively, a sentence with no infinite model has its finite models bounded in size, so checking it over finite structures reduces to finitely many sizes.

Encoding a computation in a finite domain

The reduction from acceptance to finite satisfiability is the standard one, and it is worth writing out because every detail matters.

Given a machine M and input w, build a sentence φ whose finite models correspond to accepting computations of M on w. The domain of a model is the set of time steps 0, 1, …, n, where n is the number of steps before halting. Relations encode the configuration at each time:

• A binary relation < interpreted as the usual order on the domain, with axioms making it a strict linear order with a first element and a last element, plus an axiom saying that besides these the domain has nothing but the successors of the first element. Finiteness is not axiomatised; instead the finite domains satisfying the sentence are exactly the intended ones, and the question is only whether a finite model exists.
• A unary relation for each state of M, with axioms saying exactly one state holds at each time step, and the state at the first element is the start state, and the state at the last element is the accepting state.
• A binary relation H(t, p) for “the head is at cell p at time t”, with a uniqueness axiom per time step.
• A ternary relation T(t, p, s) for “cell p holds symbol s at time t”, with a uniqueness axiom per pair (t, p).
• Initial-content axioms: for each position i within the length of the input w, a clause fixing the symbol at the i-th cell of the first time step. The symbols of w are constants of the vocabulary, so the sentence hardwires the input.
• Transition axioms: for each pair of consecutive time steps and each position, the symbol at that position at the later time is determined by the earlier symbol and whether the head was there, according to M’s transition table.

The sentence is a conjunction of first-order axioms over this vocabulary, and its length is proportional to the size of M’s transition table plus the length of w, with a constant factor for the quantifier structure. The construction is effective and uniform.

Now the correspondence. If M accepts w in n steps, build a finite structure with domain {0, …, n} and interpret the relations according to the actual computation. Every axiom holds, so φ has a finite model. Conversely, if φ has a finite model, its domain is linearly ordered with a first and a last element, the state relation picks out exactly one state per time step, the transition axioms force the sequence of configurations to follow M’s transition table, the first configuration encodes the start state and the input, and the last encodes the accepting state. Reading the model off time step by time step yields an accepting computation of length equal to the domain size minus one.

Hence φ has a finite model if and only if M accepts w. Finite satisfiability is therefore undecidable, and FinVal — its complement, restricted to sentences — is undecidable as well.

Why the same construction proves less over all structures

Run the same argument with “model” instead of “finite model” and the converse direction fails. A model of φ can have an infinite domain, ordered like the naturals or like an order with no last element. Such a model describes an infinite computation, and an infinite computation is exactly what a non-halting machine produces. So φ has a model whenever M runs forever: the model is the limit of the finite prefixes, and compactness guarantees it exists as a single structure.

This is not a technicality. It is the precise sense in which first-order logic cannot distinguish “halts” from “runs forever” over infinite structures: the theory of the infinite computation satisfies every finite approximation, so it satisfies the whole sentence. Church’s theorem therefore cannot be established by a reduction to satisfiability over arbitrary structures, because the direction of the correspondence points the wrong way: satisfiability over all structures is co-r.e., while the construction here needs the yes-instances to be the halting ones. It needs a different encoding, one that forces a finite witness — typically by coding the computation into a term structure where the halting step is a syntactic object rather than a domain element.

Trakhtenbrot’s contribution is that restricting to finite domains restores the correspondence. The price is that the resulting problem is not the validity problem of a proof system. There is no complete finitary proof calculus for finite validity, because no recursively enumerable set of axioms can generate exactly the sentences true in all finite structures. The set FinVal is co-recursively enumerable, and it is not recursively enumerable, so no effectively presented proof system proves exactly its members.

The asymmetry, laid out

The two problems sit at different levels of the arithmetical hierarchy, and the levels explain why neither restriction rescues decidability.

Problem	Status	Reason
Val (all structures)	r.e.-complete	Enumerate proofs; undecidable by Church
Satisfiability, all structures	co-r.e., not r.e.	Complement of Val
Finite satisfiability	r.e.-complete	Enumerate finite structures; undecidable by Trakhtenbrot
FinVal (finite structures)	co-r.e., not r.e.	Complement of finite satisfiability

The two r.e. entries are r.e. for different reasons, and the difference is the point of the section. Validity over all structures is r.e. because a complete proof calculus exists: enumerate proofs until one proves the sentence. Finite satisfiability is r.e. because finite objects can be enumerated: try every domain size and every interpretation. Neither enumeration decides the complementary question, so both problems remain undecidable.

The complement operation is what moves between the rows. The two upper rows are complements of one another, and so are the two lower rows. Validity over all structures is r.e., so satisfiability over all structures, being its complement, is co-r.e. and not r.e. Finite satisfiability is r.e.-complete, so FinVal, being its complement, is co-r.e. and not r.e.

Neither problem is decidable, and neither is a candidate for a practical tool. The reason finite model theory is nevertheless a live subject is that restricting the logic or the class of structures restores decidability: monadic second-order logic over trees and over words describes the regular tree and word languages, and first-order logic over structures of bounded treewidth can be evaluated by algorithms whose cost depends on the width and on the formula but not on the size of the domain. Those results are the theoretical basis of query evaluation algorithms and of verification of finite-state systems.

from itertools import product

def finite_models(sentence_checker, domain_size, relations):
    """Enumerate interpretations of each relation symbol over a domain of the
    given size, and yield those satisfying the sentence. The number of
    interpretations is 2 ** sum(domain_size ** arity) for each relation,
    so the enumeration is exhaustive in the domain size."""
    cells = {r: list(product(range(domain_size), repeat=arity))
             for r, arity in relations.items()}
    for bits in product([False, True], repeat=sum(len(c) for c in cells.values())):
        it = iter(bits)
        interp = {r: {t for t in cells[r] if next(it)} for r in relations}
        if sentence_checker(interp, domain_size):
            yield interp

The enumeration is finite for each size, which is why finite satisfiability is semi-decidable: run the loop for n = 1, 2, 3, … and stop when a model appears. It never stops when no finite model exists, and that is the entire difference between semi-decidability and decidability.

Consequences that reach outside logic

Three practical consequences follow, and each is a design constraint rather than a curiosity.

Query languages and database theory. Relational databases are finite structures. The expressive power of a query language is measured by which properties of finite structures it can define, and the standard results — that first-order logic cannot express connectivity or transitivity, that it can express only local properties — are theorems about finite structures specifically. The infinite case behaves differently, and the finite case is the one that governs query optimisation.

Verification of parameterised systems. A system with an unbounded number of components is a family of finite structures of increasing size. Asking whether a property holds for every size is an infinite conjunction of finite questions, and no single decision procedure covers it in general. The tractable cases are those where the family has a bound on some structural parameter, or where the components are uniform enough that the whole family can be described by a finite-state abstraction; either way an unbounded quantification becomes finite.

The spectrum problem. The spectrum of a sentence is the set of domain sizes in which it has a model. Which sets of naturals are spectra is Scholz’s problem, posed in the 1950s and still open: it is not known whether the class of spectra is closed under complement. The question is a precise measure of how much structure a single first-order sentence can impose on the sizes of its models, and it remains unresolved despite the surrounding theory being well developed.

Where the boundary sits

The pair of results is often summarised as “first-order logic is undecidable, whether or not the semantics is restricted to finite structures”. That summary is true and hides the useful part. Over infinite structures, the undecidability comes from the failure of compactness to respect halting: a non-halting computation has a model. Over finite structures, the undecidability comes from the unbounded size of the domain, which lets a single sentence quantify over computations of every length. Remove either source — bound the domain size, or restrict the quantifier pattern — and decidability can return.

The distinction also clarifies what a decision procedure for a logic actually promises. A procedure that decides validity over all structures is a proof checker plus a completeness theorem. A procedure that decides validity over finite structures would be something stronger, and Trakhtenbrot’s theorem says it cannot exist for full first-order logic. Restricted logics recover it by giving up expressiveness until the halting encoding no longer fits, which is the same trade made in Presburger Arithmetic and the Decidable Side of Number Theory when multiplication is dropped from the signature.