Ehrenfeucht–Fraïssé games

The n-round Ehrenfeucht–Fraïssé game on two L-structures M and N starts from a position: a k-tuple a of pebbled elements of M and a k-tuple b of N. In each round Spoiler picks an element of one structure and Duplicator answers with an element of the other; the chosen pair is appended to the position. Duplicator wins a play when every position reached, the initial one included, is a partial isomorphism: the map a i ↦ b i is well defined, injective, and preserves and reflects every relation of L.

DuplicatorWins L n a b is the recursive characterization of the positions from which Duplicator has a winning strategy in the n-round game; duplicatorWins_iff_exists_strategy relates it to explicit strategies, and IsBackAndForth.duplicatorWins to back-and-forth systems, the usual way to construct winning strategies. The game is defined for arbitrary languages and structures. For relational languages, DuplicatorWins.realize_iff is the easy direction of the Ehrenfeucht–Fraïssé theorem: a winning position satisfies the same formulas of quantifier rank at most n. The converse needs a finite relational vocabulary and is proved in CslibFrontier.Logics.FirstOrder.EhrenfeuchtFraisse.Hintikka.

The pebbles are recorded as tuples Fin k → M, which Fin.snoc extends; these are the variable assignments of Mathlib's BoundedFormula with k bound variables and no free variables, so the game positions match the semantics of formulas without translation. Constants and function symbols are not handled by the game: positions do not close under terms, so the easy direction assumes L.IsRelational.

Main definitions

• Cslib.Logic.FO.PartialIso: the pebbled tuples define a partial isomorphism.
• Cslib.Logic.FO.DuplicatorWins: Duplicator wins the n-round game from a position.
• Cslib.Logic.FO.Strategy, Cslib.Logic.FO.Strategy.IsWinning: Duplicator strategies and winning strategies. Both bodies are exposed, so clients can build strategies by recursion and check them with Strategy.isWinning_zero and Strategy.isWinning_succ.
• Cslib.Logic.FO.IsBackAndForth: back-and-forth systems indexed by the number of rounds left.

Main results

• Cslib.Logic.FO.duplicatorWins_iff_exists_strategy: Duplicator wins exactly when she has a winning strategy.
• Cslib.Logic.FO.IsBackAndForth.duplicatorWins, Cslib.Logic.FO.isBackAndForth_duplicatorWins: back-and-forth systems consist of winning positions, and the winning positions form the largest one.
• Cslib.Logic.FO.DuplicatorWins.mono, Cslib.Logic.FO.DuplicatorWins.refl, Cslib.Logic.FO.DuplicatorWins.symm, Cslib.Logic.FO.DuplicatorWins.trans, FirstOrder.Language.Equiv.duplicatorWins: monotonicity in the number of rounds, the equivalence-relation laws and invariance under isomorphism.
• Cslib.Logic.FO.DuplicatorWins.realize_iff: Ehrenfeucht–Fraïssé, easy direction; Cslib.Logic.FO.DuplicatorWins.formula_realize_iff is the same for L.Formula (Fin k).

References

• A. Ehrenfeucht, An application of games to the completeness problem for formalized theories
• R. Fraïssé, Sur quelques classifications des systèmes de relations
• L. Libkin, Elements of Finite Model Theory, Chapter 3.
• H.-D. Ebbinghaus and J. Flum, Finite Model Theory, Chapter 2.

Partial isomorphisms

structure Cslib.Logic.FO.PartialIso (L : FirstOrder.Language) {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k : ℕ} (a : Fin k → M) (b : Fin k → N) : Prop

The pebbled tuples a and b define a partial isomorphism a i ↦ b i: the map is well defined and injective, and it preserves and reflects every relation.

• eq_iff (i j : Fin k) : a i = a j ↔ b i = b j

  Two pebbles coincide in M exactly when they coincide in N.

• relMap_iff {l : ℕ} (R : L.Relations l) (f : Fin l → Fin k) : FirstOrder.Language.Structure.RelMap R (a ∘ f) ↔ FirstOrder.Language.Structure.RelMap R (b ∘ f)

  Every relation holds of the pebbles in M exactly when it holds of them in N.

theorem Cslib.Logic.FO.PartialIso.refl {L : FirstOrder.Language} {M : Type w} [L.Structure M] {k : ℕ} (a : Fin k → M) : PartialIso L a a

theorem Cslib.Logic.FO.PartialIso.symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k : ℕ} {a : Fin k → M} {b : Fin k → N} (h : PartialIso L a b) : PartialIso L b a

theorem Cslib.Logic.FO.PartialIso.trans {L : FirstOrder.Language} {M : Type w} {N : Type w'} {P : Type w''} [L.Structure M] [L.Structure N] [L.Structure P] {k : ℕ} {a : Fin k → M} {b : Fin k → N} {c : Fin k → P} (h₁ : PartialIso L a b) (h₂ : PartialIso L b c) : PartialIso L a c

The game

def Cslib.Logic.FO.DuplicatorWins (L : FirstOrder.Language) {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : ℕ → {k : ℕ} → (Fin k → M) → (Fin k → N) → Prop

Duplicator wins the n-round Ehrenfeucht–Fraïssé game from the position (a, b): the position is a partial isomorphism and, if a round remains, every move of Spoiler in either structure has an answer from which Duplicator wins the remaining rounds.

theorem Cslib.Logic.FO.duplicatorWins_zero {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k : ℕ} {a : Fin k → M} {b : Fin k → N} : DuplicatorWins L 0 a b ↔ PartialIso L a b

theorem Cslib.Logic.FO.duplicatorWins_succ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n k : ℕ} {a : Fin k → M} {b : Fin k → N} : DuplicatorWins L (n + 1) a b ↔ PartialIso L a b ∧ (∀ (c : M), ∃ (d : N), DuplicatorWins L n (Fin.snoc a c) (Fin.snoc b d)) ∧ ∀ (d : N), ∃ (c : M), DuplicatorWins L n (Fin.snoc a c) (Fin.snoc b d)

theorem Cslib.Logic.FO.DuplicatorWins.partialIso {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n k : ℕ} {a : Fin k → M} {b : Fin k → N} (h : DuplicatorWins L n a b) : PartialIso L a b

theorem Cslib.Logic.FO.DuplicatorWins.forth {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n k : ℕ} {a : Fin k → M} {b : Fin k → N} (h : DuplicatorWins L (n + 1) a b) (c : M) : ∃ (d : N), DuplicatorWins L n (Fin.snoc a c) (Fin.snoc b d)

theorem Cslib.Logic.FO.DuplicatorWins.back {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n k : ℕ} {a : Fin k → M} {b : Fin k → N} (h : DuplicatorWins L (n + 1) a b) (d : N) : ∃ (c : M), DuplicatorWins L n (Fin.snoc a c) (Fin.snoc b d)

Strategies

def Cslib.Logic.FO.Strategy {M : Type w} {N : Type w'} : ℕ → {k : ℕ} → (Fin k → M) → (Fin k → N) → Type (max w w')

A Duplicator strategy for the n-round game from the position (a, b): for every move of Spoiler, an answer in the other structure together with a strategy for the remaining rounds. The body is exposed: clients build strategies and read off their answers.

def Cslib.Logic.FO.Strategy.IsWinning {M : Type w} {N : Type w'} (L : FirstOrder.Language) [L.Structure M] [L.Structure N] {n k : ℕ} {a : Fin k → M} {b : Fin k → N} : Strategy n a b → Prop

A strategy is winning when every position reached in a play following it, including the initial one, is a partial isomorphism. The body is exposed so that clients can check that a concrete strategy wins.

@[simp]

theorem Cslib.Logic.FO.Strategy.isWinning_zero {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k : ℕ} {a : Fin k → M} {b : Fin k → N} (σ : Strategy 0 a b) : IsWinning L σ ↔ PartialIso L a b

@[simp]

theorem Cslib.Logic.FO.Strategy.isWinning_succ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n k : ℕ} {a : Fin k → M} {b : Fin k → N} (σ : Strategy (n + 1) a b) : IsWinning L σ ↔ PartialIso L a b ∧ (∀ (c : M), IsWinning L (σ.1 c).snd) ∧ ∀ (d : N), IsWinning L (σ.2 d).snd

theorem Cslib.Logic.FO.duplicatorWins_iff_exists_strategy {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n k : ℕ} {a : Fin k → M} {b : Fin k → N} : DuplicatorWins L n a b ↔ ∃ (σ : Strategy n a b), Strategy.IsWinning L σ

Duplicator wins the n-round game exactly when she has a winning strategy.

Back-and-forth systems

structure Cslib.Logic.FO.IsBackAndForth (L : FirstOrder.Language) {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (I : ℕ → {k : ℕ} → (Fin k → M) → (Fin k → N) → Prop) : Prop

A back-and-forth system: a family I j of sets of positions, j being the number of rounds still to play, each consisting of partial isomorphisms, such that every position of I (j + 1) can be extended, for every move of Spoiler, to a position of I j.

• partialIso {j k : ℕ} {a : Fin k → M} {b : Fin k → N} : I j a b → PartialIso L a b

  Every position of the system is a partial isomorphism.

• forth {j k : ℕ} {a : Fin k → M} {b : Fin k → N} : I (j + 1) a b → ∀ (c : M), ∃ (d : N), I j (Fin.snoc a c) (Fin.snoc b d)

  Every move of Spoiler in M has an answer in N staying in the system.

• back {j k : ℕ} {a : Fin k → M} {b : Fin k → N} : I (j + 1) a b → ∀ (d : N), ∃ (c : M), I j (Fin.snoc a c) (Fin.snoc b d)

  Every move of Spoiler in N has an answer in M staying in the system.

theorem Cslib.Logic.FO.IsBackAndForth.duplicatorWins {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {I : ℕ → {k : ℕ} → (Fin k → M) → (Fin k → N) → Prop} (hI : IsBackAndForth L I) {n k : ℕ} {a : Fin k → M} {b : Fin k → N} : I n a b → DuplicatorWins L n a b

Every position of a back-and-forth system with n rounds to play is won by Duplicator.

theorem Cslib.Logic.FO.isBackAndForth_duplicatorWins (L : FirstOrder.Language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] : IsBackAndForth L fun (n x : ℕ) (a : Fin x → M) (b : Fin x → N) => DuplicatorWins L n a b

The winning positions of Duplicator form the largest back-and-forth system.

Basic properties of the game

theorem Cslib.Logic.FO.DuplicatorWins.mono {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {m n k : ℕ} {a : Fin k → M} {b : Fin k → N} : m ≤ n → DuplicatorWins L n a b → DuplicatorWins L m a b

theorem Cslib.Logic.FO.DuplicatorWins.refl {L : FirstOrder.Language} {M : Type w} [L.Structure M] (n : ℕ) {k : ℕ} (a : Fin k → M) : DuplicatorWins L n a a

theorem Cslib.Logic.FO.DuplicatorWins.symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n k : ℕ} {a : Fin k → M} {b : Fin k → N} : DuplicatorWins L n a b → DuplicatorWins L n b a

theorem Cslib.Logic.FO.DuplicatorWins.trans {L : FirstOrder.Language} {M : Type w} {N : Type w'} {P : Type w''} [L.Structure M] [L.Structure N] [L.Structure P] {n k : ℕ} {a : Fin k → M} {b : Fin k → N} {c : Fin k → P} : DuplicatorWins L n a b → DuplicatorWins L n b c → DuplicatorWins L n a c

theorem FirstOrder.Language.Equiv.duplicatorWins {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (n : ℕ) {k : ℕ} (a : Fin k → M) : Cslib.Logic.FO.DuplicatorWins L n a (⇑e ∘ a)

Duplicator wins every game between a structure and an isomorphic copy, from a position and its image.

The easy direction of the Ehrenfeucht–Fraïssé theorem

theorem Cslib.Logic.FO.DuplicatorWins.realize_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] {n k : ℕ} {a : Fin k → M} {b : Fin k → N} (h : DuplicatorWins L n a b) {φ : L.BoundedFormula Empty k} (hφ : quantifierRank φ ≤ n) : φ.Realize default a ↔ φ.Realize default b

Ehrenfeucht–Fraïssé, easy direction. For a relational language, if Duplicator wins the n-round game from (a, b), then a and b satisfy the same formulas of quantifier rank at most n. No finiteness assumption is needed.

theorem Cslib.Logic.FO.realize_toFormula_relabel {L : FirstOrder.Language} {P : Type u_1} [L.Structure P] {k : ℕ} (φ : L.BoundedFormula Empty k) (a : Fin k → P) : (FirstOrder.Language.Formula.relabel (Sum.elim Empty.elim id) φ.toFormula).Realize a ↔ φ.Realize default a

A bounded formula φ with k bound variables and no free variables, turned into a formula with free variables Fin k by BoundedFormula.toFormula and relabeling, holds of a exactly when φ holds with bound variables a. With quantifierRank_formula_relabel and quantifierRank_toFormula, it moves rank-bounded statements from L.BoundedFormula Empty k to L.Formula (Fin k).

theorem Cslib.Logic.FO.DuplicatorWins.formula_realize_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] {n k : ℕ} {a : Fin k → M} {b : Fin k → N} (h : DuplicatorWins L n a b) {φ : L.Formula (Fin k)} (hφ : quantifierRank φ ≤ n) : φ.Realize a ↔ φ.Realize b

Ehrenfeucht–Fraïssé, easy direction, for formulas with free variables. For a relational language, a winning position (a, b) of the n-round game satisfies the same formulas φ : L.Formula (Fin k) of quantifier rank at most n, the free variables naming the pebbles.