Potential isomorphism of countably generated structures

A back-and-forth system between countably generated structures yields an isomorphism, and indeed every member of the system extends to one. The countable case therefore identifies potential isomorphism with isomorphism. No relational-language or countability-of-symbols hypothesis is needed.

The proof adapts FirstOrder.Language.equiv_between_cg in Mathlib/ModelTheory/PartialEquiv.lean, by Aaron Anderson, Gabin Kolly, and David Wärn. Instead of requiring all finitely generated partial equivalences to extend, we apply Order.sequenceOfCofinals to the subtype of a single back-and-forth system. Mathlib's DirectLimit.partialEquivLimit then assembles the resulting increasing chain. This is the countable back-and-forth argument underlying Carol Karp, Finite-quantifier equivalence (1965).

theorem TauCeti.exists_le_equiv_of_cg {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {S : Set (L.FGEquiv M N)} (hforth : ∀ f ∈ S, ∀ (m : M), ∃ g ∈ S, m ∈ (↑g).dom ∧ f ≤ g) (hback : ∀ f ∈ S, ∀ (n : N), ∃ g ∈ S, n ∈ (↑g).cod ∧ f ≤ g) {g : L.FGEquiv M N} (hg : g ∈ S) (hM : FirstOrder.Language.Structure.CG L M) (hN : FirstOrder.Language.Structure.CG L N) : ∃ (e : L.Equiv M N), ↑g ≤ e.toEmbedding.toPartialEquiv

Between countably generated structures, every member of a back-and-forth system of finitely generated partial equivalences extends to an isomorphism.

theorem TauCeti.PotentialIso.nonempty_equiv_of_cg {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (h : PotentialIso M N) (hM : FirstOrder.Language.Structure.CG L M) (hN : FirstOrder.Language.Structure.CG L N) : Nonempty (L.Equiv M N)

Potentially isomorphic countably generated structures are isomorphic. Countable generation suffices even when function symbols generate uncountably many elements.

theorem TauCeti.countable_potentialIso_iff_iso {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [Countable M] [Countable N] : PotentialIso M N ↔ Nonempty (L.Equiv M N)

For countable structures, potential isomorphism is equivalent to isomorphism. This includes empty structures and languages with function or nullary relation symbols.