Potential Isomorphism

This file defines potential isomorphism between structures and connects it to back-and-forth equivalence at all ordinal levels.

Main Definitions

• PotentialIso: A potential isomorphism between structures M and N is a family of finite partial maps containing the empty map and closed under extension in both directions.

Main Results

• PotentialIso.countable_toEquiv: Potentially isomorphic countable structures are isomorphic.
• BFEquiv_all_implies_potentialIso: Back-and-forth equivalence at every ordinal yields a potential isomorphism.

References

• [KK04], Theorem 1.2.1

structure FirstOrder.Language.PotentialIso (L : Language) [L.IsRelational] (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] : Type (max w w')

A potential isomorphism between structures M and N is a family of finite partial maps (given as pairs of compatible tuples) that contains the empty map and is closed under extension in both directions.

This is the model-theoretic notion corresponding to "back-and-forth system" or "winning strategy in the infinite EF game."

• family : Set ((n : ℕ) × (Fin n → M) × (Fin n → N))

  The family of partial maps, represented as pairs of tuples of equal length.

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

  The family contains the empty map.

• compatible (p : (n : ℕ) × (Fin n → M) × (Fin n → N)) : p ∈ self.family → SameAtomicType p.snd.1 p.snd.2

  Each pair in the family preserves atomic type.

• forth (p : (n : ℕ) × (Fin n → M) × (Fin n → N)) : p ∈ self.family → ∀ (m : M), ∃ (n' : N), ⟨p.fst + 1, (Fin.snoc p.snd.1 m, Fin.snoc p.snd.2 n')⟩ ∈ self.family

  Forth: for any pair and any element of M, there's an extension in the family.

• back (p : (n : ℕ) × (Fin n → M) × (Fin n → N)) : p ∈ self.family → ∀ (n' : N), ∃ (m : M), ⟨p.fst + 1, (Fin.snoc p.snd.1 m, Fin.snoc p.snd.2 n')⟩ ∈ self.family

  Back: for any pair and any element of N, there's an extension in the family.

noncomputable def FirstOrder.Language.PotentialIso.refl {L : Language} [L.IsRelational] (M : Type w) [L.Structure M] : L.PotentialIso M M

The trivial potential isomorphism from M to itself via the identity.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def FirstOrder.Language.PotentialIso.symm {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] (p : L.PotentialIso M N) : L.PotentialIso N M

Potential isomorphism is symmetric.

Equations

• p.symm = { family := {q : (n : ℕ) × (Fin n → N) × (Fin n → M) | ⟨q.fst, (q.snd.2, q.snd.1)⟩ ∈ p.family}, empty_mem := ⋯, compatible := ⋯, forth := ⋯, back := ⋯ }

PotentialIso implies isomorphism for countable structures

theorem FirstOrder.Language.PotentialIso.countable_toEquiv {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] (P : L.PotentialIso M N) : Nonempty (L.Equiv M N)

For countable structures, a potential isomorphism implies actual isomorphism.

This is a direct back-and-forth construction that doesn't go through Scott sentences or Karp's theorem, avoiding circular dependencies in the formalization.

theorem FirstOrder.Language.BFEquiv_all_implies_potentialIso {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] (hBF : ∀ (α : Ordinal.{w}), BFEquiv α 0 Fin.elim0 Fin.elim0) : Nonempty (L.PotentialIso M N)

BF-equivalence at all ordinals implies potential isomorphism.

The proof constructs the family of tuples (n, a, b) such that BFEquiv α n a b holds for every ordinal α, and verifies the forth and back properties by a supremum contradiction argument.

Universe constraint: The proof requires the ordinal universe to match the type universe w (via Ordinal.bddAbove_of_small). This is because the contradiction argument takes a supremum of ordinals indexed by N : Type w, which requires Ordinal.{w}.