Ehrenfeucht-Fraïssé Games

Origin. Ehrenfeucht (1961) building on Fraïssé (1954). Game characterization of elementary equivalence. Spoiler vs Duplicator. n-round game captures n-quantifier equivalence.

Models. Two structures A, B. Spoiler tries to show difference. Duplicator maintains isomorphism. Duplicator wins n rounds iff A ≡ₙ B (agree on sentences of quantifier depth n).

Formalism.

Game setup: Structures A, B over same signature. n-round game Gₙ(A, B).

Round i: Spoiler: picks element from A or B. If picks aᵢ ∈ A: Duplicator responds with bᵢ ∈ B. If picks bᵢ ∈ B: Duplicator responds with aᵢ ∈ A.

Winning condition: After n rounds: (a₁,...,aₙ) and (b₁,...,bₙ). Duplicator wins iff the map aᵢ ↦ bᵢ is a partial isomorphism. Preserves atomic relations and equalities.

Strategy: Duplicator has winning strategy in Gₙ(A, B) iff A ≡ₙ B.

Theorem (Ehrenfeucht): A ≡ₙ B (agree on FO sentences of quantifier depth ≤n) iff Duplicator has winning strategy in Gₙ(A, B).

Pebble games: k pebbles: captures k-variable logic. Spoiler reuses pebbles. L^k: FO with k variables.

Applications: Proving inexpressibility in FO. "Parity not FO-definable": EF argument. Lower bounds on quantifier depth.

Symbols.

Symbol	Unicode	Name	Meaning
ω	U+03C9	Omega	Finite quantifier depth in L_{∞ω}
↦	U+21A6	Maps to	The partial map aᵢ ↦ bᵢ built by the play
∈	U+2208	Element of	Choice of an element from a structure
∞	U+221E	Infinity	Infinitary equivalence, ≡_{∞ω}
≅	U+2245	Isomorphism	What Duplicator must approximate
≡	U+2261	Elementary equivalence	Agreement on all first-order sentences
≤	U+2264	Less than or equal	Bound on quantifier depth
≡ₙ	—	n-equivalence	Same theory up to quantifier depth n
Gₙ	—	Game	The n-round Ehrenfeucht–Fraïssé game
↔ₚ	—	Partial isomorphism	A back-and-forth system of partial maps
A, B	—	Structures	The two structures being compared
aᵢ, bᵢ	—	Chosen elements	The moves of round i
<	—	Linear order	A built-in order, which neutralizes the method
BIT	—	Bit predicate	Numerical predicate in FO(<, BIT)
L^k	—	k-variable logic	Fragment captured by the k-pebble game
C^k	—	k-variable counting logic	Fragment captured by the bijection game
L_{∞ω}	—	Infinitary logic	Arbitrary conjunctions, finite quantifier depth

Metatheory. The theorem needs a finite relational signature, and that hypothesis is what makes it work: over such a signature there are only finitely many formulas of quantifier rank n up to logical equivalence, so each ≡ₙ class is defined by a single Hintikka sentence, and the game is a combinatorial reading of that sentence. Because ≡ₙ classes are themselves first-order definable, the method is complete for first-order inexpressibility: a property is not FO-definable exactly when for every n there are structures with and without it that Duplicator separates in Gₙ. The standard calculation is that two finite linear orders of size at least 2^n are ≡ₙ, which shows that evenness of the universe is not first-order definable; separate constructions give the undefinability of connectivity, acyclicity, and reachability on graphs. Karp (1965) proved the infinite version: Duplicator wins the unbounded game iff the structures are partially isomorphic, which is equivalent to L_{∞ω}-equivalence, and for countable structures to isomorphism. Pezzoli (1998) proved that deciding the winner of the r-move game on two finite structures is PSPACE-complete when r is part of the input, while Grohe (1996) showed the k-pebble equivalence is P-complete for fixed k.

Applies to. Finite model theory. Descriptive complexity. Lower bounds. Logic expressiveness. Database theory.

Limitations. The characterization presupposes a finite relational signature; with infinitely many symbols, or with function symbols left unrelativized, the finiteness of the rank-n type space fails and the correspondence has to be restated. The game gives elementary equivalence, not isomorphism — over infinite structures ≡ is strictly weaker than ≅, and only the countable back-and-forth case closes the gap. A built-in linear order defeats the method in practice: with the order fixed, Duplicator's replies are constrained to preserve position, and no useful winning strategy survives — which is why the undefinability of parity in FO(<, BIT) is a circuit lower bound rather than an Ehrenfeucht–Fraïssé argument, and why the technique has contributed nothing to the order-based captures of descriptive complexity. Strategies must be built by hand for each n, and there is no shortcut: Pezzoli showed deciding the winner is PSPACE-complete. Finally the theorem is about first-order logic alone; monadic second-order, counting, and modal fragments each require a separate game — Ajtai–Fagin, bijection, bisimulation — rather than an instance of one theorem.