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
≡ₙ	—	n-equivalence	Same depth-n theory
Gₙ	—	Game	n-round game
↔ₚ	—	Partial iso	Preserved structure

Metatheory. Characterizes FO equivalence. Back-and-forth systems. Pebble games for fragments. Modal bisimulation as variant.

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

Limitations. Games can be complex. Strategy existence vs finding. Only captures FO. Extensions for other logics.