Finite Ehrenfeucht–Fraïssé strategies

EFStrategy L k a b is a winning strategy for Duplicator for k more rounds, starting with paired tuples a and b. At each round Spoiler chooses an element of either structure and Duplicator supplies a matching element and a continuation strategy. Atomic agreement is checked also at the initial position, so empty structures with different nullary relations cannot win by having no legal moves.

Existence of a strategy is equivalent to finite-level BFEquiv. The strategy is data, rather than just the alternating-quantifier condition: its branches specify responses to every move. Different finite lengths need not choose compatible responses; a coherent infinite strategy is a separate object.

The game interpretation is the classical Ehrenfeucht–Fraïssé interpretation of back-and-forth relations; see Wilfrid Hodges, Model Theory (1993), the treatment of back-and-forth games.

inductive TauCeti.EFStrategy (L : FirstOrder.Language) [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : ℕ → {n : ℕ} → (Fin n → M) → (Fin n → N) → Type (max w w')

A winning finite-round Duplicator strategy. Every branch records a response and a winning continuation, and every reached position must preserve the atomic type.

• zero {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} {a : Fin n → M} {b : Fin n → N} (atomic : SameAtomicType a b) : EFStrategy L 0 a b

  With no moves remaining, atomic agreement is exactly the winning condition.

• succ {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k n : ℕ} {a : Fin n → M} {b : Fin n → N} (atomic : SameAtomicType a b) (forth : M → N) (back : N → M) (forth_cont : (x : M) → EFStrategy L k (Fin.snoc a x) (Fin.snoc b (forth x))) (back_cont : (y : N) → EFStrategy L k (Fin.snoc a (back y)) (Fin.snoc b y)) : EFStrategy L (k + 1) a b

  Respond to a move on either side, with a strategy for the remaining rounds.

def TauCeti.EFStrategy.dropLast {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k n : ℕ} {a : Fin n → M} {b : Fin n → N} : EFStrategy L (k + 1) a b → EFStrategy L k a b

Forget the last round of a finite strategy.

@[simp]

theorem TauCeti.EFStrategy.dropLast_one {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} {a : Fin n → M} {b : Fin n → N} (h : SameAtomicType a b) (f : M → N) (g : N → M) (fc : (x : M) → EFStrategy L 0 (Fin.snoc a x) (Fin.snoc b (f x))) (gc : (y : N) → EFStrategy L 0 (Fin.snoc a (g y)) (Fin.snoc b y)) : (succ h f g fc gc).dropLast = zero h

@[simp]

theorem TauCeti.EFStrategy.dropLast_succ {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k n : ℕ} {a : Fin n → M} {b : Fin n → N} (h : SameAtomicType a b) (f : M → N) (g : N → M) (fc : (x : M) → EFStrategy L (k + 1) (Fin.snoc a x) (Fin.snoc b (f x))) (gc : (y : N) → EFStrategy L (k + 1) (Fin.snoc a (g y)) (Fin.snoc b y)) : (succ h f g fc gc).dropLast = succ h f g (fun (x : M) => (fc x).dropLast) fun (y : N) => (gc y).dropLast

theorem TauCeti.EFStrategy.bfEquiv {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k n : ℕ} {a : Fin n → M} {b : Fin n → N} (s : EFStrategy L k a b) : BFEquiv (↑k) n a b

A winning k-round strategy implies back-and-forth equivalence at level k.

theorem TauCeti.EFStrategy.nonempty_iff_bfEquiv {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k n : ℕ} {a : Fin n → M} {b : Fin n → N} : Nonempty (EFStrategy L k a b) ↔ BFEquiv (↑k) n a b

Finite back-and-forth equivalence is exactly existence of a winning finite strategy.

theorem TauCeti.EFStrategy.nonempty_family_iff_bfEquiv_omega0 {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} {a : Fin n → M} {b : Fin n → N} : Nonempty ((k : ℕ) → EFStrategy L k a b) ↔ BFEquiv Ordinal.omega0 n a b

An unrelated winning strategy for every finite length amounts only to level-ω back-and-forth equivalence. No compatibility between these strategies is imposed.