A game that decides what can be said

Two structures are given — say a chain of four elements and a chain of five. Is there a sentence of first-order logic true in one and false in the other?

Obviously yes: there exist five distinct elements does it. The interesting question is how complicated such a sentence has to be, and the natural measure of complication is the number of nested quantifiers, the quantifier depth. A sentence of depth $k$ can talk about $k$ elements at once and no more.

Answering that question directly means quantifying over all sentences of a given depth, of which there are infinitely many. The game replaces it with a finite search.

The rules #

There are two players. Spoiler wants to show the structures are different; Duplicator wants to pretend they are the same. A number of rounds $k$ is fixed in advance.

In each round Spoiler picks an element of either structure. Duplicator must reply with an element of the other one. After $k$ rounds, $k$ pairs of elements have been chosen, and Duplicator has survived if the map sending each chosen element to its partner respects the structure: for chains, that the two sequences of pebbles are in the same order; in general, that every relation holding among the chosen elements on one side holds among their partners on the other.

The theorem — Ehrenfeucht’s, following Fraïssé’s algebraic version — is:

Duplicator has a winning strategy in the $k$-round game exactly when the two structures satisfy the same sentences of quantifier depth at most $k$.

The direction that explains the rules is this one. A sentence of depth $k$ is a nesting of $k$ quantifiers, and Spoiler’s moves correspond to the existential ones: to show that $\exists x\, \varphi$ holds in one structure and not the other, point at the witness $x$ on the side where it exists and challenge Duplicator to produce one on the other side. Duplicator’s reply is the other structure’s attempted witness, and after $k$ rounds the innermost, quantifier-free part of the sentence is what the pebble configuration has to satisfy. A winning strategy for Duplicator is precisely a way of defeating every such challenge.

Playing it out #

Two rounds are not enough to separate four from five. The reason is worth following, because it is the whole mechanism in miniature. After Spoiler’s first move Duplicator answers at the corresponding position, matching the number of elements to the left as closely as the lengths allow; the discrepancy of one has to be absorbed somewhere, and Duplicator puts it in the largest available gap. With one round left, Spoiler can probe a gap and Duplicator needs only that the gap on the other side is not empty when the challenged one is not empty.

Three rounds are enough, and Spoiler’s strategy is a bisection: aim at the middle, then at the middle of the resulting discrepancy, and after $\log$-many rounds the gap Duplicator has to fake is a single element wide and cannot be faked.

The pattern in that table is a theorem: Duplicator wins the $k$-round game on chains of lengths $m$ and $n$ exactly when $m = n$, or both are at least $2^k - 1$. The figure computes each square by exhaustive search over both players’ moves and then checks the rule against it — the search is the evidence and the rule is the summary, rather than the other way round.

The count that surprises #

Read off the diagonal of that table and something worth pausing on appears.

To distinguish a chain of $1{,}000$ from a chain of $1{,}001$ takes ten rounds, not a thousand. The naive sentence — there exist $1{,}001$ distinct elements — has depth $1{,}001$, and it is wildly inefficient. The efficient sentence works by bisection, and the number of quantifiers it needs is the logarithm of the length.

Writing that sentence out is unpleasant and the game never requires anybody to. That is the point of the method: the game is an equivalent question that can be answered by search, and the sentence it certifies to exist need never be produced. A proof that something is expressible, obtained without exhibiting the expression.

What it is really for #

Turn the theorem around and it becomes a tool for proving that something cannot be said.

To show a property is not expressible in first-order logic, exhibit for each $k$ a pair of structures — one with the property, one without — on which Duplicator wins the $k$-round game. Then no sentence of depth $k$ can define the property, for any $k$, and since every sentence has some finite depth, no sentence defines it.

The standard examples are all of this shape.

Evenness of a set’s size is not first-order expressible. For any $k$, take chains of length $2^k$ and $2^k + 1$; both are at least $2^k - 1$, so Duplicator wins the $k$-round game, and one has even size while the other does not.

Connectedness of a graph is not first-order expressible: for each $k$, a long cycle and a pair of long cycles look the same to $k$ rounds, and one is connected while the other is not.

Reachability, acyclicity, and being a tree all fail the same way. The pattern behind them is that first-order logic sees only a bounded neighbourhood of each pebbled element — a statement made precise by Gaifman’s theorem — and any property requiring an unbounded count or an unbounded search along a path escapes it.

This is the standing use of the method, and there is no competitor for it. Compactness and the Löwenheim–Skolem theorems prove non-expressibility of statements about infinite structures, and say nothing about finite ones; the game is the only general tool that works on finite structures, which is why it became a basic technique of finite model theory — the finite case being exactly where the diagonal argument and the compactness theorem have nothing to say and of the part of complexity theory that describes classes by the logics that define them.

One argument in full: why evenness cannot be said #

The non-expressibility arguments above are worth doing once at full length, because the shape is the same every time and the shape is the thing to learn.

Claim: no first-order sentence in the language of orders is true exactly of the chains of even length.

Suppose one existed, and let $k$ be its quantifier depth. Take the chains of length $2^k$ and $2^k + 1$. Both are at least $2^k - 1$ long, so by the theorem above Duplicator wins the $k$-round game on them, and therefore the two chains satisfy exactly the same sentences of depth $k$. But one has even length and the other does not, so the supposed sentence is true in one and false in the other — a contradiction.

Three features of that argument recur in every use of the method. The sentence is never examined; only its depth is used. The pair of structures depends on $k$, so a family is required rather than a single example — which is why the conclusion holds for first-order logic as a whole rather than for one depth. And what makes the family work is a threshold: once both chains are long enough, the game cannot tell them apart, and the threshold grows with the rounds exactly as fast as the resource does.

The same three features power the harder results. That connectedness is not first-order expressible uses a family of pairs — one long cycle against two shorter ones — with the cycles growing with $k$; the reason Duplicator survives is that after $k$ rounds the pebbles have only seen neighbourhoods of bounded radius, and in a long enough cycle those neighbourhoods are indistinguishable from the ones in a pair of cycles. Making bounded radius precise is Gaifman’s theorem, and with it the game arguments become nearly mechanical.

What the game is not #

Two confusions are worth heading off, because both are natural and both are wrong.

A Duplicator win does not mean the structures are the same. It means no sentence of the given depth separates them, which is a much weaker statement — chains of seven and eight are plainly different and no sentence of depth three notices. Duplicator winning every finite game means the structures satisfy exactly the same sentences, which is still not sameness: two models of one set of axioms can agree on every sentence and disagree in size, which is what the Löwenheim–Skolem theorems are about.

And a Spoiler win does not mean the structures are far apart in any other sense. Spoiler wins in three rounds on chains of four and five, which differ by one element; Duplicator survives three rounds on chains of seven and a thousand, which do not. What the game measures is not similarity but definable similarity, and the two behave differently — a fact worth remembering whenever a logic is being used as a measure of complexity.

The relation to what a quantifier order says #

The game is measuring something the order of quantifiers already hints at.

A sentence’s depth bounds how many elements it can hold in mind at once, and its quantifier alternations bound how much the choice of one element can depend on another. Both are resources, and both have games attached: the pebble game here counts depth, and a variant with a bounded number of reusable pebbles counts width, which is the resource relevant to the logics used in database theory.

What all these games share is the structure of the theorem: a syntactic resource on one side, a combinatorial game on the other, and an equivalence between them. Once the equivalence is established, questions about the syntax — is this expressible? how complicated must the expression be? — become questions about strategies, and strategies on finite structures can be searched.

Where it fails, and what it costs #

The search is expensive. The number of positions after $r$ rounds is roughly $(mn)^r$, so a direct search is exponential in the number of rounds. The figures here memoise on the pebbled configuration and keep the structures small; a general-purpose tool cannot do much better, and hand proofs use a strategy argument rather than a search.

Winning a game is not the same as writing a sentence. The theorem certifies that a distinguishing sentence exists without producing it, and extracting one from Spoiler’s strategy is possible but produces something unreadable. The method proves expressibility and non-expressibility; it does not do syntax.

Infinite structures need care, in the way an infinite tree needs a compactness argument before anything can be concluded from its finite levels. The theorem as stated is about finitely many rounds and holds for infinite structures too, but a Duplicator win at every finite $k$ gives elementary equivalence and not isomorphism — the two structures satisfy the same sentences and may still be different. The dense rational order and the dense real order are the standing example: elementarily equivalent, and one is countable while the other is not.

Only first-order logic. Add a quantifier over sets, or a transitive-closure operator, and the game changes; the corresponding games exist but are harder, and for second-order logic no useful game is known — the gap between what a system can express and what it can prove being a separate question with its own machinery.

What the pictures cannot show #

The game tree is enormous and the figures show one path through it. A transcript in which Spoiler wins is evidence that Spoiler wins; a transcript in which Duplicator survives proves nothing on its own, since Spoiler might have played badly. What makes the drawn transcripts trustworthy is that the verdict beside them comes from the exhaustive search rather than from the transcript, and the two are required to agree.

The tables are drawn for chains up to eight and three rounds, because the search is exponential and because the pattern is visible there. The theorem is about all lengths and all depths, and the drawn evidence is a corner of it.

And the negative results above — evenness, connectedness — cannot be drawn at all. They require a family of structure pairs, one for each $k$, growing without bound, and the argument is that Duplicator wins in every member of the family. A picture can show one member; the induction is prose.

Where it came from #

Fraïssé gave the algebraic version in 1954, in terms of families of partial isomorphisms with an extension property — no game, but the same content. Ehrenfeucht recast it as a game in 1961, and the game version is what survived, because a strategy is easier to describe and to reason about than a family of maps closed under extension.

The technique found its permanent home in finite model theory, which grew in the 1970s and 1980s out of database theory and complexity. There the guiding results are of the form this complexity class is exactly the properties definable in that logic, and proving that something is not in a class often reduces to proving it is not definable, which reduces to a game. The most famous instance is the theorem that parity is not computable by small constant-depth circuits, whose combinatorial heart is a game argument of the same family.

The ladder from here #

Below: what a quantifier order can say, which is the smallest example of a resource limiting expression, and two models of the same axioms, which is what elementary equivalence looks like when the structures are genuinely different. Sideways: resolution, which measures the difficulty of a proof rather than of a statement, and is the other half of the same accounting. Above: the pebble games of finite model theory, and the theorems relating logics to complexity classes.

What is worth carrying away #

The move here is one of the most useful in the subject: replace a quantification over all formulas by a game, and a game by a search.

The reason it works is that the syntax of first-order logic is layered — a sentence of depth $k$ builds on sentences of depth $k-1$ — and a game is layered in the same way, one round per layer. Whenever a formal language has that shape, a game is worth looking for; and when one is found, statements of the form no formula of this kind can say that stop being arguments about all possible formulas and become arguments about one strategy.

The habit generalises past logic. A resource-bounded description of anything — a program with limited memory, a proof with limited length, a circuit with limited depth — invites the same question: what game does the resource correspond to, and who wins it?