Infinitary equivalence and Karp's theorem

InfEquivAt κ M N says that M and N satisfy the same L_{∞ω} sentences whose conjunctions and disjunctions are indexed by the carrier κ. Agreement transports contravariantly along index codings: agreement at κ gives agreement at every carrier ι coded into κ, since recoding a sentence along an IndexCoding ι κ preserves its meaning.

Karp's theorem says that structures in a relational language are potentially isomorphic exactly when they satisfy the same infinitary sentences. The forward direction holds at every carrier, and the converse at any carrier κ into which the second structure is coded. Full infinitary equivalence InfEquivW quantifies, outside the syntax, over all carriers in the universe of M ⊕ N, and the carrier M ⊕ N packages the converse. No countability is assumed, and the carrier and the universes of the two structures are independent. For countable structures, which are coded into ℕ, agreement on the L_{ω₁ω} sentences is therefore isomorphism.

The theorem is Carol Karp's, Finite-quantifier equivalence (1965). Cameron Freer's cameronfreer/infinitary-logic, InfinitaryLogic/Karp/CarrierTheorem.lean at checkpoint 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4, proves both directions at a common carrier.

Main definitions

• TauCeti.InfEquivAt: agreement on all sentences with a given branching carrier.
• TauCeti.InfEquivW: agreement at every carrier in the universe of M ⊕ N.

Main results

• TauCeti.InfEquivAt.of_reindex: agreement transports contravariantly along index codings.
• TauCeti.IsTupleBFSystem.realize_iff: the tuples of a pair in a tuple back-and-forth system satisfy the same infinitary formulas.
• TauCeti.BFEquiv.realize_iff_of_qrank_le: tuples that are back-and-forth equivalent at level α satisfy the same infinitary formulas of quantifier rank at most α.
• TauCeti.BFEquiv.elementarilyEquivalent: back-and-forth equivalence of the empty tuples at level ω gives elementary equivalence.
• TauCeti.PotentialIso.infEquivAt: potentially isomorphic structures satisfy the same infinitary sentences at every carrier.
• TauCeti.exists_forall_realize_snoc_iff_of_forall_realize_iff and TauCeti.exists_forall_realize_snoc_iff_of_forall_realize_iff_right: tuples agreeing on every formula with a carrier into which the second structure is coded admit matching one-element extensions, forth and back.
• TauCeti.karp_theorem_at: Karp's theorem at a carrier into which the second structure is coded.
• TauCeti.karp_theorem: Karp's theorem for full infinitary equivalence.
• TauCeti.InfEquivAt.infEquivW and TauCeti.InfEquivW.infEquivAt: agreement at one carrier coding the second structure gives full infinitary equivalence, which gives agreement at carriers in every universe.
• TauCeti.countable_infEquivAt_nat_iff_iso: on countable structures, agreement on the L_{ω₁ω} sentences is isomorphism.

def TauCeti.InfEquivAt {L : FirstOrder.Language} (κ : Type uκ) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] : Prop

M and N satisfy the same L_{∞ω} sentences whose conjunctions and disjunctions are indexed by κ.

theorem TauCeti.infEquivAt_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {κ : Type uκ} : InfEquivAt κ M N ↔ ∀ (φ : L.SentenceInf κ), φ.Realize M ↔ φ.Realize N

Agreement at κ means agreement on every sentence with branching carrier κ.

theorem TauCeti.infEquivAt_iff_forall_realize {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {κ : Type uκ} : InfEquivAt κ M N ↔ ∀ (φ : L.BoundedFormulaInf κ Empty 0), φ.Realize Empty.elim Fin.elim0 ↔ φ.Realize Empty.elim Fin.elim0

Agreement at κ is agreement on the formulas with carrier κ, no free variables, and no bound-variable slots, under the empty valuations.

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

M and N satisfy the same L_{∞ω} sentences at every carrier in the universe of M ⊕ N. The carriers are quantified outside the syntax.

theorem TauCeti.infEquivW_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : InfEquivW M N ↔ ∀ (κ : Type (max w w')), InfEquivAt κ M N

Full infinitary equivalence is agreement at every carrier in the universe of M ⊕ N.

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

Agreement at a carrier κ gives agreement at every carrier ι coded into κ.

theorem TauCeti.InfEquivAt.elementarilyEquivalent {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {κ : Type uκ} (h : InfEquivAt κ M N) : L.ElementarilyEquivalent M N

Agreement on the infinitary sentences at any carrier implies elementary equivalence, since first-order sentences embed at every carrier.

theorem TauCeti.exists_forall_realize_snoc_iff_of_forall_realize_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {κ : Type uκ} (cN : IndexCoding N κ) {n : ℕ} {a : Fin n → M} {b : Fin n → N} (hab : ∀ (φ : L.BoundedFormulaInf κ Empty n), φ.Realize Empty.elim a ↔ φ.Realize Empty.elim b) (x : M) : ∃ (y : N), ∀ (φ : L.BoundedFormulaInf κ Empty (n + 1)), φ.Realize Empty.elim (Fin.snoc a x) ↔ φ.Realize Empty.elim (Fin.snoc b y)

Matching one more element. If two tuples agree on every infinitary formula with carrier κ and the second structure is coded into κ, then every one-element extension of the first tuple is matched by a one-element extension of the second that again agrees on every such formula.

theorem TauCeti.exists_forall_realize_snoc_iff_of_forall_realize_iff_right {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {κ : Type uκ} (cN : IndexCoding N κ) {n : ℕ} {a : Fin n → M} {b : Fin n → N} (hab : ∀ (φ : L.BoundedFormulaInf κ Empty n), φ.Realize Empty.elim a ↔ φ.Realize Empty.elim b) (y : N) : ∃ (x : M), ∀ (φ : L.BoundedFormulaInf κ Empty (n + 1)), φ.Realize Empty.elim (Fin.snoc a x) ↔ φ.Realize Empty.elim (Fin.snoc b y)

Matching one more element, backwards. If two tuples agree on every infinitary formula with carrier κ and the second structure is coded into κ, then every one-element extension of the second tuple is matched by a one-element extension of the first that again agrees on every such formula. Only the second structure needs a coding.

theorem TauCeti.BFEquiv.realize_iff_of_qrank_le {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] {κ : Type uκ} {n : ℕ} (φ : L.BoundedFormulaInf κ Empty n) {α : Ordinal.{o}} {a : Fin n → M} {b : Fin n → N} : BFEquiv α n a b → Ordinal.lift.{o, uκ} φ.qrank ≤ Ordinal.lift.{uκ, o} α → ∀ (v : Empty → M) (w : Empty → N), φ.Realize v a ↔ φ.Realize w b

Back-and-forth equivalence at level α gives agreement up to quantifier rank α. Tuples that are back-and-forth equivalent at level α satisfy the same infinitary formulas of quantifier rank at most α, at every carrier. The rank and the level are compared after lifting them to a common universe.

theorem TauCeti.BFEquiv.elementarilyEquivalent {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] (h : BFEquiv Ordinal.omega0 0 Fin.elim0 Fin.elim0) : L.ElementarilyEquivalent M N

Back-and-forth equivalence at level ω gives elementary equivalence. Relational structures whose empty tuples are back-and-forth equivalent at level ω satisfy the same first-order sentences, since a first-order sentence has finite quantifier rank.

theorem TauCeti.IsTupleBFSystem.realize_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] {S : Set ((n : ℕ) × (Fin n → M) × (Fin n → N))} (hS : IsTupleBFSystem S) {κ : Type uκ} {n : ℕ} (φ : L.BoundedFormulaInf κ Empty n) {a : Fin n → M} {b : Fin n → N} : ⟨n, (a, b)⟩ ∈ S → ∀ (v : Empty → M) (w : Empty → N), φ.Realize v a ↔ φ.Realize w b

Pairs in a tuple back-and-forth system satisfy the same infinitary formulas, at every carrier.

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

Karp's theorem, forward direction. Potentially isomorphic structures in a relational language satisfy the same infinitary sentences, at every carrier.

The converse

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

Karp's theorem, converse direction. Structures in a relational language that satisfy the same infinitary sentences with a carrier κ into which the second structure is coded are potentially isomorphic.

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

Karp's theorem at a carrier. Structures in a relational language, the second coded into κ, are potentially isomorphic exactly when they satisfy the same infinitary sentences with carrier κ.

theorem TauCeti.karp_theorem {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] : PotentialIso M N ↔ InfEquivW M N

Karp's theorem. Structures in a relational language are potentially isomorphic exactly when they satisfy the same infinitary sentences. The converse uses the carrier M ⊕ N.

theorem TauCeti.InfEquivAt.infEquivW {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] {κ : Type uκ} (cN : IndexCoding N κ) (h : InfEquivAt κ M N) : InfEquivW M N

Agreement at one carrier into which the second structure is coded gives full infinitary equivalence.

theorem TauCeti.InfEquivW.infEquivAt {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] (h : InfEquivW M N) (μ : Type uμ) : InfEquivAt μ M N

Full infinitary equivalence gives agreement at a carrier in any universe.

theorem TauCeti.countable_infEquivAt_nat_iff_iso {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] [Countable M] [Countable N] : InfEquivAt ℕ M N ↔ Nonempty (L.Equiv M N)

Karp's theorem for countable structures. Countable structures in a relational language are isomorphic exactly when they satisfy the same L_{ω₁ω} sentences, the infinitary sentences whose conjunctions and disjunctions are indexed by ℕ.