The two presentations of back-and-forth systems

For relational languages, tuple back-and-forth systems and systems of finitely generated partial equivalences give the same notion of potential isomorphism. Matching atomic types produce an equivalence between the finite ranges of the tuples. Conversely, a partial equivalence preserves the atomic type of every tuple in its domain. Neither countability nor nonemptiness of the structures is required; nullary relations are retained. When the first tuple is onto its structure, matching atomic types even give an embedding of the whole structure.

The comparison is the relational back-and-forth argument of Carol Karp, Finite-quantifier equivalence (1965). The tuple presentation also appears in Cameron Freer's cameronfreer/infinitary-logic, InfinitaryLogic/Karp/PotentialIso.lean at checkpoint 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4. Here potential isomorphism uses Mathlib's FGEquiv, and the comparison with tuple systems is explicit.

theorem FirstOrder.Language.PartialEquiv.sameAtomicType {L : Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) {n : ℕ} (a : Fin n → ↥f.dom) : TauCeti.SameAtomicType (fun (i : Fin n) => ↑(a i)) (⇑f.toEmbedding ∘ a)

A partial equivalence preserves the atomic type of each tuple in its domain.

theorem FirstOrder.Language.PartialEquiv.le_of_dom_eq_range {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.PartialEquiv M N} {n : ℕ} {a : Fin n → M} {b : Fin n → N} (a' : Fin n → ↥f.dom) (ha : ∀ (i : Fin n), ↑(a' i) = a i) (hb : ∀ (i : Fin n), f.toEmbedding (a' i) = b i) (hd : ↑f.dom = Set.range a) (c : Fin n → ↥g.dom) (hc : ∀ (i : Fin n), ↑(c i) = a i) (he : ∀ (i : Fin n), g.toEmbedding (c i) = b i) : f ≤ g

If the domain of a partial equivalence f is enumerated by a tuple a that f sends to b, then every partial equivalence sending a to b extends f.

theorem TauCeti.SameAtomicType.exists_fgEquiv {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 : L.FGEquiv M N) (a' : Fin n → ↥(↑f).dom), (∀ (i : Fin n), ↑(a' i) = a i) ∧ (∀ (i : Fin n), (↑f).toEmbedding (a' i) = b i) ∧ ↑(↑f).dom = Set.range a

Tuples with matching atomic types induce a finitely generated partial equivalence whose whole domain is the range of the first tuple. Repeated entries are allowed.

theorem TauCeti.SameAtomicType.exists_embedding_comp_eq {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) (ha : Function.Surjective a) : ∃ (f : L.Embedding M N), ⇑f ∘ a = b

If a tuple onto M has the same atomic type as a tuple b of N, then sending each entry to the corresponding entry of b is an embedding of M into N. Repeated entries are allowed.

theorem TauCeti.IsTupleBFSystem.exists_fgEquiv_system {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))} (hS : IsTupleBFSystem S) {n : ℕ} {a : Fin n → M} {b : Fin n → N} (hab : ⟨n, (a, b)⟩ ∈ S) : ∃ (T : Set (L.FGEquiv M N)), (∀ f ∈ T, ∀ (m : M), ∃ g ∈ T, m ∈ (↑g).dom ∧ f ≤ g) ∧ (∀ f ∈ T, ∀ (y : N), ∃ g ∈ T, y ∈ (↑g).cod ∧ f ≤ g) ∧ ∃ f ∈ T, ∃ (a' : Fin n → ↥(↑f).dom), (∀ (i : Fin n), ↑(a' i) = a i) ∧ ∀ (i : Fin n), (↑f).toEmbedding (a' i) = b i

A tuple back-and-forth system gives a system of finitely generated partial equivalences, closed under extensions on both sides, in which each pair of the tuple system is matched by some member.

theorem TauCeti.IsTupleBFSystem.potentialIso {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))} (hS : IsTupleBFSystem S) : PotentialIso M N

A tuple back-and-forth system gives a system of finitely generated partial equivalences.

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

A system of finitely generated partial equivalences supplies a tuple back-and-forth system by taking all tuples whose entries are simultaneously matched by a member of the system.

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

For relational languages, potential isomorphism is equivalently witnessed by a tuple back-and-forth system. This includes empty structures and languages with nullary relations.