Potential isomorphism and all back-and-forth levels

Two relational structures are potentially isomorphic exactly when their empty tuples are back-and-forth equivalent at every ordinal level. More generally, equivalence at every level is itself closed under matching one-element extensions. The extension argument takes the supremum of one failure level for each possible match.

For countable structures, the countable back-and-forth construction upgrades this to isomorphisms: tuples are equivalent at every level exactly when an isomorphism carries one to the other. Inside one countable structure, equivalence at every level is therefore the same as lying in one automorphism orbit.

This is the all-level characterization in Carol Karp, Finite-quantifier equivalence (1965). The tuple-system formulation follows Cameron Freer's cameronfreer/infinitary-logic, InfinitaryLogic/Karp/PotentialIso.lean at checkpoint 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4. Here it is connected to the finitely generated partial-equivalence definition of potential isomorphism through IsTupleBFSystem.

theorem TauCeti.BFEquiv.exists_forth_of_all {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 : ∀ (α : Ordinal.{max w w'}), BFEquiv α n a b) (x : M) : ∃ (y : N), ∀ (α : Ordinal.{max w w'}), BFEquiv α (n + 1) (Fin.snoc a x) (Fin.snoc b y)

Tuples equivalent at every ordinal level admit a matching extension for each element of the first structure.

theorem TauCeti.BFEquiv.exists_back_of_all {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 : ∀ (α : Ordinal.{max w w'}), BFEquiv α n a b) (y : N) : ∃ (x : M), ∀ (α : Ordinal.{max w w'}), BFEquiv α (n + 1) (Fin.snoc a x) (Fin.snoc b y)

Tuples equivalent at every ordinal level admit a matching extension for each element of the second structure.

theorem TauCeti.isTupleBFSystem_bfEquiv_all {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (h : ∀ (α : Ordinal.{max w w'}), BFEquiv α 0 Fin.elim0 Fin.elim0) : IsTupleBFSystem {p : (n : ℕ) × (Fin n → M) × (Fin n → N) | ∀ (α : Ordinal.{max w w'}), BFEquiv α p.fst p.snd.1 p.snd.2}

The pairs of tuples equivalent at every level form a tuple back-and-forth system as soon as the empty tuples are equivalent at every level.

theorem TauCeti.potentialIso_iff_bfEquiv_all {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : PotentialIso M N ↔ ∀ (α : Ordinal.{max w w'}), BFEquiv α 0 Fin.elim0 Fin.elim0

Two relational structures are potentially isomorphic exactly when their empty tuples are back-and-forth equivalent at every ordinal level in the joint structure universe.

theorem TauCeti.IsTupleBFSystem.exists_equiv_comp_eq {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [Countable M] [Countable 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) : ∃ (e : L.Equiv M N), ⇑e ∘ a = b

Between countable relational structures, each pair of a tuple back-and-forth system is carried one to the other by an isomorphism.

theorem TauCeti.bfEquiv_all_iff_exists_equiv_comp_eq {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [Countable M] [Countable N] {n : ℕ} {a : Fin n → M} {b : Fin n → N} : (∀ (α : Ordinal.{max w w'}), BFEquiv α n a b) ↔ ∃ (e : L.Equiv M N), ⇑e ∘ a = b

Tuples in one isomorphism orbit. Tuples of countable relational structures are back-and-forth equivalent at every level exactly when an isomorphism carries one to the other.