Karp's theorem at a common branching carrier

Karp's theorem for the fixed-carrier infinitary syntax: two structures are potentially isomorphic if and only if they satisfy the same L∞ω sentences.

The point of the fixed-carrier formulation is where the quantifier over index types lives. In a syntax whose iSup/iInf nodes each carry their own index type, the theorem has to quantify over index types inside every node, which forces the index universe to track the structure universe. Here each formula branches over a single carrier ι, so the quantifier sits outside the syntax, in InfEquivW, and the backward direction needs only one carrier — any κ admitting codings of both structures.

Main definitions

• InfEquivAt L ι M N: agreement on all L∞ω sentences branching over the carrier ι. The structures may live in different universes.
• InfEquivW L M N: agreement at every carrier in the structures' shared universe.

Main results

• karp_theorem_at: potential isomorphism is equivalent to InfEquivAt L κ M N for any carrier κ admitting codings IndexCoding M κ and IndexCoding N κ.
• karp_theorem_on_sum: the canonical specialization at κ := M ⊕ N.
• karp_theorem_w: the packaged same-universe endpoint, Nonempty (PotentialIso L M N) ↔ InfEquivW L M N. This is the public statement of Karp's theorem.

The separating conjunctions in the backward direction are iInfAlong along the two given codings — a conjunction indexed by one structure's carrier, expressed at κ. That is the whole content of "any common carrier suffices": the sum is canonical, not necessary.

References

• Carol R. Karp, Finite-quantifier equivalence, in The Theory of Models (Addison, Henkin, Tarski, eds.), North-Holland, 1965, pp. 407–412. The theorem.
• Carol R. Karp, Languages with Expressions of Infinite Length, North-Holland, 1964 — the infinitary languages themselves.
• H. Jerome Keisler and Julia F. Knight, Barwise: infinitary logic and admissible sets, Bull. Symbolic Logic 10 (2004), 4–36, doi:10.2178/bsl/1080330272. Theorem 1.2.1 is the statement formalized here.

The common-carrier formulation with IndexCoding is this formalization's presentation, not a statement made in those sources; the mathematics is Karp's.

Equivalence at a carrier

def FirstOrder.Language.InfEquivAt (L : Language) (ι : Type uι) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] : Prop

L∞ω-equivalence at a fixed branching carrier ι: the structures satisfy the same sentences whose infinitary connectives branch over ι. The structures need not share a universe.

Equations

• L.InfEquivAt ι M N = ∀ (φ : L.SentenceInf ι), φ.Realize M ↔ φ.Realize N

def FirstOrder.Language.InfEquivW (L : Language) (M N : Type w) [L.Structure M] [L.Structure N] : Prop

L∞ω-equivalence with branching carriers drawn from the structures' own universe. The quantifier over index types is here, outside the syntax, rather than inside every infinitary node.

Equations

• L.InfEquivW M N = ∀ (ι : Type ?u.1), L.InfEquivAt ι M N

theorem FirstOrder.Language.InfEquivAt.of_reindex {L : Language} {ι : Type uι} {κ : Type uκ} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (c : IndexCoding ι κ) (h : L.InfEquivAt κ M N) : L.InfEquivAt ι M N

Expressive strength is contravariant in codings: a carrier that codes ι can express every ι-branching sentence, so agreement at the larger carrier implies agreement at the smaller.

def FirstOrder.Language.atomicFormulaInf {L : Language} {ι : Type uι} {n : ℕ} (idx : L.AtomicIdx n) : L.BoundedFormulaInf ι Empty n

The atomic formula of an AtomicIdx, with the tuple in bound positions, generic in the branching carrier.

Bound positions are what let the all case below consume forth/back directly: no free-variable relabeling operation appears anywhere in this development.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.atomicFormulaInf (FirstOrder.Language.AtomicIdx.rel R f) = FirstOrder.Language.BoundedFormulaInf.rel R fun (k : Fin l) => FirstOrder.Language.var (Sum.inr (f k))

theorem FirstOrder.Language.realize_atomicFormulaInf {L : Language} {ι : Type uι} {n : ℕ} {P : Type w} [L.Structure P] (idx : L.AtomicIdx n) (xs : Fin n → P) : (atomicFormulaInf idx).Realize Empty.elim xs ↔ idx.holds xs

theorem FirstOrder.Language.PotentialIso.infEquivAt {L : Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (P : L.PotentialIso M N) (ι : Type uι) : L.InfEquivAt ι M N

Forward direction: a potential isomorphism yields agreement at every carrier, in every index universe.

theorem FirstOrder.Language.infEquivAt_implies_potentialIso {L : Language} {κ : Type uκ} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (cM : IndexCoding M κ) (cN : IndexCoding N κ) (h : L.InfEquivAt κ M N) : Nonempty (L.PotentialIso M N)

Backward direction at any common carrier: agreement in a single carrier κ admitting codings of both structures already builds a potential isomorphism.

The separating formula is an iInfAlong — a conjunction indexed by one structure's carrier, expressed at κ along the given coding — closed by ex. The sum carrier plays no role.

theorem FirstOrder.Language.karp_theorem_at {L : Language} {κ : Type uκ} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (cM : IndexCoding M κ) (cN : IndexCoding N κ) : Nonempty (L.PotentialIso M N) ↔ L.InfEquivAt κ M N

Karp's theorem at any sufficiently large common carrier.

Agreement in one carrier admitting codings of both structures already characterizes potential isomorphism. The structures may live in different universes.

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

Karp's theorem at the sum carrier: the canonical specialization of karp_theorem_at, obtained by feeding it the two sum injections.

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

Karp's theorem (Keisler–Knight 2004, Theorem 1.2.1): potential isomorphism is equivalent to agreement on all L∞ω sentences branching over carriers in the structures' universe.

Forward instantiates the generic direction at each ι; backward specializes to the single carrier M ⊕ N. Pure packaging around karp_theorem_at.

The quantifier-rank forward lemma

Back-and-forth equivalence at level α implies agreement on every formula of rank at most α. This is stated at an arbitrary branching carrier, with independent structure universes, and with BFEquiv's ordinal in the same universe as qrank — so no Ordinal.lift enters the induction. Callers whose ordinal genuinely lives elsewhere bridge at the boundary with BFEquiv.ofOrdinalLift / .toOrdinalLift.

The tuple sits in free-variable positions here, because that is what the consumers need; the Fin.append plumbing below is the cost of that choice, and is confined to these two lemmas.

theorem FirstOrder.Language.BFEquiv_implies_agreeQR {L : Language} {ι : Type uι} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (α : Ordinal.{uι}) {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

The Karp lemma, forward direction: back-and-forth equivalence at level α implies agreement on every formula of quantifier rank at most α.

Carrier-polymorphic, with independent structure universes, and with the BFEquiv ordinal in the same universe as the rank.