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_iff_BFEquiv_all: Potential isomorphism is equivalent to BF-equivalence at all ordinal levels (for the empty tuple).

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.potentialIso_family_BFEquiv {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] (P : L.PotentialIso M N) (α : Ordinal.{u_1}) {n : ℕ} {a : Fin n → M} {b : Fin n → N} (hab : ⟨n, (a, b)⟩ ∈ P.family) : BFEquiv α n a b

Given a potential isomorphism, BFEquiv holds at every ordinal level for any pair in the family. This is the key inductive step for the (→) direction of the potential isomorphism characterization.

The proof proceeds by ordinal induction: the zero case uses atomic type preservation, the successor case uses the forth/back extension properties, and the limit case follows from the induction hypothesis.

theorem FirstOrder.Language.PotentialIso.implies_BFEquiv_all {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] (P : L.PotentialIso M N) (α : Ordinal.{u_1}) : BFEquiv α 0 Fin.elim0 Fin.elim0

A potential isomorphism implies BF-equivalence at all ordinals for the empty tuple.

theorem FirstOrder.Language.BFEquiv_all_implies_potentialIso {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {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_range). This is because the contradiction argument takes a supremum of ordinals indexed by N : Type w, which requires Ordinal.{w}. The forward direction (PotentialIso.implies_BFEquiv_all) is fully universe-polymorphic.

theorem FirstOrder.Language.potentialIso_iff_BFEquiv_all {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] : Nonempty (L.PotentialIso M N) ↔ ∀ (α : Ordinal.{w}), BFEquiv α 0 Fin.elim0 Fin.elim0

A potential isomorphism exists if and only if BFEquiv holds at all ordinals for the empty tuple. This is the main characterization theorem for potential isomorphism.

Universe note: The ordinal universe is constrained to match the type universe w by BFEquiv_all_implies_potentialIso (which uses a supremum over N : Type w). The forward direction is universe-polymorphic; the backward direction requires this match.