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