Tuple back-and-forth systems

A tuple back-and-forth system is a set of pairs of equally long finite tuples containing the empty pair, preserving atomic types, and admitting one-element extensions in both directions within the same set. Every pair in such a system is back-and-forth equivalent at every ordinal, and every tuple of either structure occurs in some pair of the system. These systems allow characteristic sentences to produce potential isomorphisms without requiring every finite partial isomorphism to extend.

This is the tuple presentation of back-and-forth systems used in Carol Karp, Finite-quantifier equivalence (1965). See also Cameron Freer's cameronfreer/infinitary-logic, InfinitaryLogic/Karp/PotentialIso.lean at checkpoint 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4. Here the system is an explicit set of tuple pairs.

structure TauCeti.IsTupleBFSystem {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (S : Set ((n : ℕ) × (Fin n → M) × (Fin n → N))) : Prop

A set of pairs of finite tuples containing the empty pair, preserving atomic types, and closed under matching one-element extensions in both directions within the set.

• empty_mem : ⟨0, (Fin.elim0, Fin.elim0)⟩ ∈ S

  The empty tuples belong to the system.

• sameAtomicType {n : ℕ} {a : Fin n → M} {b : Fin n → N} : ⟨n, (a, b)⟩ ∈ S → SameAtomicType a b

  Every pair in the system agrees on all atomic tests, including nullary relations.

• forth {n : ℕ} {a : Fin n → M} {b : Fin n → N} : ⟨n, (a, b)⟩ ∈ S → ∀ (x : M), ∃ (y : N), ⟨n + 1, (Fin.snoc a x, Fin.snoc b y)⟩ ∈ S

  Every element of the first structure has a matching extension in the system.

• back {n : ℕ} {a : Fin n → M} {b : Fin n → N} : ⟨n, (a, b)⟩ ∈ S → ∀ (y : N), ∃ (x : M), ⟨n + 1, (Fin.snoc a x, Fin.snoc b y)⟩ ∈ S

  Every element of the second structure has a matching extension in the system.

theorem TauCeti.IsTupleBFSystem.symm {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {S : Set ((n : ℕ) × (Fin n → M) × (Fin n → N))} (h : IsTupleBFSystem S) : IsTupleBFSystem {p : (n : ℕ) × (Fin n → N) × (Fin n → M) | ⟨p.fst, (p.snd.2, p.snd.1)⟩ ∈ S}

Swapping the two tuples of every pair of a tuple back-and-forth system gives a tuple back-and-forth system in the other direction.

theorem TauCeti.IsTupleBFSystem.bfEquiv {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {S : Set ((n : ℕ) × (Fin n → M) × (Fin n → N))} (h : IsTupleBFSystem S) (α : Ordinal.{o}) {n : ℕ} {a : Fin n → M} {b : Fin n → N} (hab : ⟨n, (a, b)⟩ ∈ S) : BFEquiv α n a b

Pairs in one back-and-forth system agree at every ordinal level.

theorem TauCeti.IsTupleBFSystem.exists_snd_mem {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {S : Set ((n : ℕ) × (Fin n → M) × (Fin n → N))} (h : IsTupleBFSystem S) {n : ℕ} (a : Fin n → M) : ∃ (b : Fin n → N), ⟨n, (a, b)⟩ ∈ S

Every tuple of M is the first component of some pair in a tuple back-and-forth system: repeated forth moves extend the empty pair.

theorem TauCeti.IsTupleBFSystem.exists_fst_mem {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {S : Set ((n : ℕ) × (Fin n → M) × (Fin n → N))} (h : IsTupleBFSystem S) {n : ℕ} (b : Fin n → N) : ∃ (a : Fin n → M), ⟨n, (a, b)⟩ ∈ S

Every tuple of N is the second component of some pair in a tuple back-and-forth system: repeated back moves extend the empty pair.