Coherent infinite Ehrenfeucht–Fraïssé strategies

CoherentEFStrategy L a b records the paired tuples after every finite history of Spoiler moves, preserving atomic type and extending the preceding position by exactly the chosen move and its response. Histories list the most recent move first. An M ⊕ N move specifies both which structure Spoiler plays in and the chosen element. Every such history is legal, so the strategy carries no arbitrary values on unreachable histories.

Existence of a coherent strategy from the empty tuples is equivalent to potential isomorphism. A tuple back-and-forth system constructs a strategy by recursively choosing responses within the same system; conversely, the reached positions of one strategy form a system.

There is a genuine quantifier-order distinction: BFEquiv ω gives a winning strategy for each finite length, allowing the response to depend on that length. A coherent strategy must fix a response before knowing how many further moves will be made. The former condition does not supply the latter: a response that works for every finite continuation must be chosen once, not separately for each length. EFStrategy.nonempty_family_iff_bfEquiv_omega0 states precisely what the unrelated family expresses, while potentialIso_iff_nonempty_coherentEFStrategy characterizes the coherent object. The orders ℤ and ℤ ⊕ₗ ℤ separate the two notions: see TauCeti.isEmpty_coherentEFStrategy_int_sumLex_int in TauCeti.ModelTheory.BackAndForth.DiscreteOrder.

See Wilfrid Hodges, Model Theory (1993), for back-and-forth games, and Carol Karp, Finite-quantifier equivalence (1965), for back-and-forth systems. This construction uses the existing tuple-system API, not a family of unrelated finite strategies.

structure TauCeti.CoherentEFStrategy (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) : Type (max w w')

One winning Duplicator strategy for arbitrarily long play. The positions at all histories are compatible, so responses cannot depend on the future length of the game.

• left (h : List (M ⊕ N)) : Fin (n + h.length) → M

  The first tuple after a history of Spoiler moves, newest move first.

• right (h : List (M ⊕ N)) : Fin (n + h.length) → N

  The second tuple after the same history.

• left_nil : self.left [] = a

  The first tuple starts at a.

• right_nil : self.right [] = b

  The second tuple starts at b.

• forth_left (h : List (M ⊕ N)) (x : M) : self.left (Sum.inl x :: h) = Fin.snoc (self.left h) x

  A move in the first structure appends exactly the element played.

• forth_right (h : List (M ⊕ N)) (x : M) : self.right (Sum.inl x :: h) = Fin.snoc (self.right h) (self.right (Sum.inl x :: h) (Fin.last (n + h.length)))

  The matching response extends, rather than changes, the second tuple.

• back_left (h : List (M ⊕ N)) (y : N) : self.left (Sum.inr y :: h) = Fin.snoc (self.left h) (self.left (Sum.inr y :: h) (Fin.last (n + h.length)))

  The matching response extends, rather than changes, the first tuple.

• back_right (h : List (M ⊕ N)) (y : N) : self.right (Sum.inr y :: h) = Fin.snoc (self.right h) y

  A move in the second structure appends exactly the element played.

• sameAtomicType (h : List (M ⊕ N)) : SameAtomicType (self.left h) (self.right h)

  Duplicator wins at every finite position, including the initial position.

@[simp]

theorem TauCeti.CoherentEFStrategy.forth_right_castSucc {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} (s : CoherentEFStrategy L a b) (h : List (M ⊕ N)) (x : M) (i : Fin (n + h.length)) : s.right (Sum.inl x :: h) i.castSucc = s.right h i

A response to a move in the first structure preserves every earlier entry.

@[simp]

theorem TauCeti.CoherentEFStrategy.back_left_castSucc {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} (s : CoherentEFStrategy L a b) (h : List (M ⊕ N)) (y : N) (i : Fin (n + h.length)) : s.left (Sum.inr y :: h) i.castSucc = s.left h i

A response to a move in the second structure preserves every earlier entry.

theorem TauCeti.CoherentEFStrategy.ext {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} {s t : CoherentEFStrategy L a b} (hl : ∀ (h : List (M ⊕ N)), s.left h = t.left h) (hr : ∀ (h : List (M ⊕ N)), s.right h = t.right h) : s = t

A coherent strategy is determined by its paired positions at every history.

theorem TauCeti.CoherentEFStrategy.ext_iff {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} {s t : CoherentEFStrategy L a b} : s = t ↔ (∀ (h : List (M ⊕ N)), s.left h = t.left h) ∧ ∀ (h : List (M ⊕ N)), s.right h = t.right h

def TauCeti.CoherentEFStrategy.toFinite {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} (s : CoherentEFStrategy L a b) (k : ℕ) (h : List (M ⊕ N)) : EFStrategy L k (s.left h) (s.right h)

Restrict one coherent strategy, at any reached history, to a finite number of future rounds. All these restrictions use the same responses at their common histories.

@[simp]

theorem TauCeti.CoherentEFStrategy.toFinite_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} (s : CoherentEFStrategy L a b) (h : List (M ⊕ N)) : s.toFinite 0 h = EFStrategy.zero ⋯

@[simp]

theorem TauCeti.CoherentEFStrategy.toFinite_succ {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} (s : CoherentEFStrategy L a b) (k : ℕ) (h : List (M ⊕ N)) : s.toFinite (k + 1) h = EFStrategy.succ ⋯ (fun (x : M) => s.right (Sum.inl x :: h) (Fin.last (n.add h.length))) (fun (y : N) => s.left (Sum.inr y :: h) (Fin.last (n.add h.length))) (fun (x : M) => have hs := s.toFinite k (Sum.inl x :: h); ⋯.mp (⋯.mp hs)) fun (y : N) => have hs := s.toFinite k (Sum.inr y :: h); ⋯.mp (⋯.mp hs)

Finite restriction uses the coherent response, independently of the remaining length.

theorem TauCeti.CoherentEFStrategy.nonempty_finite {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} (s : CoherentEFStrategy L a b) (k : ℕ) : Nonempty (EFStrategy L k a b)

A coherent infinite strategy gives a winning strategy for every finite number of rounds.

noncomputable def TauCeti.IsTupleBFSystem.coherentEFStrategy {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} {S : Set ((n : ℕ) × (Fin n → M) × (Fin n → N))} (hS : IsTupleBFSystem S) (hab : ⟨n, (a, b)⟩ ∈ S) : CoherentEFStrategy L a b

A pair in a tuple back-and-forth system admits one coherent infinite strategy: each response and its continuation stay inside the same system.

theorem TauCeti.CoherentEFStrategy.exists_isTupleBFSystem_mem {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) (s : CoherentEFStrategy L a b) : ∃ (S : Set ((n : ℕ) × (Fin n → M) × (Fin n → N))), IsTupleBFSystem S ∧ ⟨n, (a, b)⟩ ∈ S

Reindexing the reached positions of a coherent strategy gives a tuple back-and-forth system containing its starting pair, even when the starting tuples are nonempty.

theorem TauCeti.CoherentEFStrategy.nonempty_iff_exists_isTupleBFSystem_mem {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 (CoherentEFStrategy L a b) ↔ ∃ (S : Set ((n : ℕ) × (Fin n → M) × (Fin n → N))), IsTupleBFSystem S ∧ ⟨n, (a, b)⟩ ∈ S

A pair admits a coherent strategy exactly when it belongs to a tuple back-and-forth system. This includes arbitrary starting tuples.

theorem TauCeti.CoherentEFStrategy.exists_isTupleBFSystem {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (s : CoherentEFStrategy L Fin.elim0 Fin.elim0) : ∃ (S : Set ((n : ℕ) × (Fin n → M) × (Fin n → N))), IsTupleBFSystem S

The reached positions of a coherent strategy from the empty tuples form a tuple back-and-forth system.

theorem TauCeti.potentialIso_iff_nonempty_coherentEFStrategy {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : PotentialIso M N ↔ Nonempty (CoherentEFStrategy L Fin.elim0 Fin.elim0)

Potential isomorphism is exactly existence of one winning coherent infinite strategy. Unlike a family of finite-round strategies, the responses are fixed across all lengths.

Regression examples