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.
• PotentialIso.ofExtensionFamily: builds one from a relation-form extension family. A producer-facing adapter, strictly below the BF-equivalence machinery.
• ExtensionPresentation: the proof-relevant variant, for callers holding states rather than a predicate.
• ExtensionPresentation.toPotentialIso: its induced potential isomorphism, via the existential image of the states and routed solely through ofExtensionFamily.

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 := ⋯ }

Producer-facing adapters

Two thin constructors for callers who have a back-and-forth system in hand and want the standard object. Both build family directly and route through nothing else — no BFEquiv, no ordinal induction, no Scott formulas, no infinitary formula agreement. In particular they sit below implies_BFEquiv_all in this file and below Karp/CarrierTheorem.lean in the import graph.

Contrast bfEquiv_all_of_extensionFamily, which serves the opposite purpose: it consumes an extension family to produce formula-level agreement. These produce the PotentialIso itself.

def FirstOrder.Language.PotentialIso.ofExtensionFamily {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] (R : (n : ℕ) → (Fin n → M) → (Fin n → N) → Prop) (empty : R 0 Fin.elim0 Fin.elim0) (compatible : ∀ {n : ℕ} {a : Fin n → M} {b : Fin n → N}, R n a b → SameAtomicType a b) (forth : ∀ {n : ℕ} {a : Fin n → M} {b : Fin n → N}, R n a b → ∀ (m : M), ∃ (n' : N), R (n + 1) (Fin.snoc a m) (Fin.snoc b n')) (back : ∀ {n : ℕ} {a : Fin n → M} {b : Fin n → N}, R n a b → ∀ (n' : N), ∃ (m : M), R (n + 1) (Fin.snoc a m) (Fin.snoc b n')) : L.PotentialIso M N

Build a potential isomorphism from a relation-form extension family.

The family is literally {p | R p.1 p.2.1 p.2.2}. Tuples are arbitrary functions Fin n → M, so repeated coordinates are supported and no injectivity is assumed; atomic compatibility is exactly SameAtomicType. Carrier universes stay independent.

Equations

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

theorem FirstOrder.Language.PotentialIso.exists_left {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] (P : L.PotentialIso M N) {n : ℕ} (b : Fin n → N) : ∃ (a : Fin n → M), ⟨n, (a, b)⟩ ∈ P.family

Every finite N-tuple is matched to an M-tuple through a potential isomorphism, by iterating back along the tuple.

theorem FirstOrder.Language.PotentialIso.exists_right {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] (P : L.PotentialIso M N) {n : ℕ} (a : Fin n → M) : ∃ (b : Fin n → N), ⟨n, (a, b)⟩ ∈ P.family

Every finite M-tuple is matched to an N-tuple through a potential isomorphism, by iterating forth along the tuple.

PotentialIso implies isomorphism for countable structures

theorem FirstOrder.Language.PotentialIso.countable_toEquiv_graph {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) : ∃ (e : L.Equiv M N), ∀ (m : M), ∃ p ∈ P.family, ∃ (i : Fin p.fst), p.snd.1 i = m ∧ p.snd.2 i = e m

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.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)

Countable structures with a potential isomorphism are isomorphic: the projection of countable_toEquiv_graph that forgets where each element is sent.

theorem FirstOrder.Language.PotentialIso.family_bfEquiv {L : Language} [L.IsRelational] {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.

The structures may live in different universes, and no countability of the language is required: the induction consumes only the family's atomic-type compatibility and its two extension properties.

@[deprecated FirstOrder.Language.PotentialIso.family_bfEquiv (since := "2026-08-14")]

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

Compatibility alias for PotentialIso.family_bfEquiv, which is stated without the countable-language hypothesis and for structures in different universes.

theorem FirstOrder.Language.PotentialIso.implies_BFEquiv_all {L : Language} [L.IsRelational] {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] {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}. The forward direction (PotentialIso.implies_BFEquiv_all) is fully universe-polymorphic.

theorem FirstOrder.Language.potentialIso_iff_BFEquiv_all {L : Language} [L.IsRelational] {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.

Proof-relevant presentations

A second producer-facing adapter, for callers who build states (partial maps, finite approximations, game positions) rather than a predicate. It exists so that certificates need not be flattened into a global relation by hand.

State is proof-relevant on purpose: different certificates may present the same tuple pair, and nothing here quotients or picks canonical representatives. This introduces no competing back-and-forth structure — its output is the existing PotentialIso, built through ofExtensionFamily, and the eventual isomorphism still comes only from PotentialIso.countable_toEquiv.

structure FirstOrder.Language.ExtensionPresentation (L : Language) [L.IsRelational] (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] : Type (max (max (u_1 + 1) w) w')

A back-and-forth system presented by states rather than by a predicate.

• State : ℕ → Type u_1

  The states at each tuple length.

• left {n : ℕ} : self.State n → Fin n → M

  The M-tuple a state presents.

• right {n : ℕ} : self.State n → Fin n → N

  The N-tuple a state presents.

• empty : self.State 0

  A state over the empty tuple.

• compatible {n : ℕ} (s : self.State n) : SameAtomicType (self.left s) (self.right s)

  Every state presents an atomic-type-preserving pair.

• forth {n : ℕ} (s : self.State n) (m : M) : ∃ (n' : N) (s' : self.State (n + 1)), self.left s' = Fin.snoc (self.left s) m ∧ self.right s' = Fin.snoc (self.right s) n'

  Forth, witnessed by a successor state.

• back {n : ℕ} (s : self.State n) (n' : N) : ∃ (m : M) (s' : self.State (n + 1)), self.left s' = Fin.snoc (self.left s) m ∧ self.right s' = Fin.snoc (self.right s) n'

  Back, witnessed by a successor state.

def FirstOrder.Language.ExtensionPresentation.Rel {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] (P : L.ExtensionPresentation M N) (n : ℕ) (a : Fin n → M) (b : Fin n → N) : Prop

The family a presentation induces: the existential image of its states. Two distinct states presenting the same pair collapse here and nowhere earlier.

Equations

• P.Rel n a b = ∃ (s : P.State n), P.left s = a ∧ P.right s = b

theorem FirstOrder.Language.ExtensionPresentation.rel_of_state {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] (P : L.ExtensionPresentation M N) {n : ℕ} (s : P.State n) : P.Rel n (P.left s) (P.right s)

Every state lands in the induced family.

def FirstOrder.Language.ExtensionPresentation.toPotentialIso {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] (P : L.ExtensionPresentation M N) : L.PotentialIso M N

The standard object a presentation produces.

Equations

• P.toPotentialIso = FirstOrder.Language.PotentialIso.ofExtensionFamily P.Rel ⋯ ⋯ ⋯ ⋯