Karp's Theorem

This file proves Karp's theorem: two structures are potentially isomorphic if and only if they are L∞ω-elementarily equivalent.

Main Results

• karp_theorem_w: Karp's theorem for relational languages: potential isomorphism is equivalent to LinfEquivW (L∞ω-elementary equivalence with index types at universe w matching the structure universe).
• karp_theorem_universe0: Specialization of karp_theorem_w to Type 0, where LinfEquivW and LinfEquiv coincide.
• BFEquiv_implies_agreeQR: Forward direction of the Karp lemma: BF-equivalence at level α implies agreement on all formulas of quantifier rank ≤ α.

Design Notes

The theorem is stated with LinfEquivW (universe-w index types) rather than LinfEquiv (universe-0 index types) because the backward direction constructs formulas with iInf indexed by N : Type w, which requires uι = w.

References

• [KK04]

Fin arithmetic helpers

These lemmas connect Fin.append, Fin.snoc, and Sum.elim and are used throughout the structural induction in BFEquiv_implies_agree_aux. They don't require the section-level IsRelational or Countable instances.

Atomic formula helpers

These relate AtomicIdx to BoundedFormulaInf atomic formulas. The term lemma needs its own [L.IsRelational] since it asserts all terms are variables.

theorem FirstOrder.Language.BFEquiv_implies_agreeQR {L : Language} [L.IsRelational] {M N : Type w} [L.Structure M] [L.Structure N] (α : Ordinal.{0}) {n : ℕ} (a : Fin n → M) (b : Fin n → N) (h : BFEquiv α n a b) (φ : L.BoundedFormulaInf (Fin n) 0) (hφ : φ.qrank ≤ α) : FormulaInf.Realize φ a ↔ FormulaInf.Realize φ b

Karp Lemma, forward direction: BF-equivalence at level α implies agreement on all formulas of quantifier rank ≤ α.

This is a direct corollary of BFEquiv_implies_agree_aux with k = 0 and xs = ys = Fin.elim0.

Karp's Theorem at universe w

This section proves Karp's theorem with LinfEquivW (index universe w matching the structure universe).

Infrastructure for KarpW

Forward: PotentialIso → LinfEquivW

theorem FirstOrder.Language.PotentialIso_implies_LinfEquivW {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] (P : L.PotentialIso M N) : L.LinfEquivW M N

Forward direction: PotentialIso implies LinfEquivW.

Backward: LinfEquivW → PotentialIso

theorem FirstOrder.Language.LinfEquivW_implies_potentialIso {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] (h : L.LinfEquivW M N) : Nonempty (L.PotentialIso M N)

Backward direction: LinfEquivW implies PotentialIso.

The family consists of tuples (n, a, b) such that a and b agree on all BoundedFormulaInf.{u,v,0,w} formulas with Fin n free variables. The forth/back properties use a contradiction argument: if no witness exists, we can build a separating formula using iInf indexed by N : Type w (which requires uι = w).

theorem FirstOrder.Language.karp_theorem_w {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] : Nonempty (L.PotentialIso M N) ↔ L.LinfEquivW M N

Karp's Theorem (KK04 Theorem 1.2.1): For relational languages, two structures are potentially isomorphic if and only if they are L∞ω-elementarily equivalent (with index types at universe w matching the structure universe).

Both directions are fully proved:

• Forward: structural induction on formulas, using PotentialIso.forth/back for all.
• Backward: direct construction of PotentialIso family from formula agreement, using iInf indexed by N : Type w to build separating formulas (requires uι = w).

theorem FirstOrder.Language.LinfEquivW_implies_LinfEquiv {L : Language} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] (h : L.LinfEquivW M N) : L.LinfEquiv M N

LinfEquivW implies LinfEquiv: universe-correct equivalence implies the standard one. This follows from liftUI which embeds BoundedFormulaInf.{u,v,0,0} into BoundedFormulaInf.{u,v,0,w}.

theorem FirstOrder.Language.PotentialIso_implies_LinfEquiv {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] (P : L.PotentialIso M N) : L.LinfEquiv M N

Forward direction of Karp's theorem: PotentialIso → LinfEquiv.

This composes PotentialIso_implies_LinfEquivW with LinfEquivW_implies_LinfEquiv to get the standard LinfEquiv (with Ordinal.{0} index types) from a PotentialIso.

theorem FirstOrder.Language.karp_theorem_forward {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] : Nonempty (L.PotentialIso M N) → L.LinfEquivW M N

Forward direction of Karp's theorem at all universes: Potential isomorphism implies L∞ω-elementary equivalence.

theorem FirstOrder.Language.karp_theorem_universe0 {L : Language} [L.IsRelational] {M N : Type} [L.Structure M] [L.Structure N] : Nonempty (L.PotentialIso M N) ↔ L.LinfEquiv M N

Karp's Theorem at universe 0.

This is karp_theorem_w specialized to M N : Type (i.e., Type 0). At universe 0, LinfEquivW and LinfEquiv coincide (both use BoundedFormulaInf.{u,v,0,0}).