Countable Corollary to Karp's Theorem

This file proves that for countable structures, elementary equivalence in the infinitary logics implies isomorphism.

The two results take genuinely different routes, and the L∞ω one is the stronger. L∞ω-equivalence goes straight through Karp's theorem to a potential isomorphism and then to an isomorphism by back-and-forth on countable structures — no Scott sentence, no refinement counting, and no countable-language hypothesis. Lω₁ω-equivalence has no such route: it is weaker than L∞ω-equivalence, so it must go through the Scott sentence, which is what drags in CountableRefinementHypothesis and the countable relational language.

Main Results

• countable_InfEquivW_implies_iso: for countable structures, L∞ω-elementary equivalence implies isomorphism. Unconditional — no refinement hypothesis, no countable language.
• countable_LomegaEquiv_implies_iso: for countable structures in a countable relational language, Lω₁ω-elementary equivalence implies isomorphism (KK04 Corollary 1.2.2).
• countable_extensionFamily_implies_iso: for countable structures, a relation-form back-and-forth system yields an isomorphism. The relational language need not be countable.
• ExtensionPresentation.countable_toEquiv: the same from a proof-relevant state presentation.

Both endpoints are direct compositions with PotentialIso.countable_toEquiv, which remains the sole implementation of the eventual isomorphism; they add packaging, not mathematics.

References

• [KK04], Corollary 1.2.2

theorem FirstOrder.Language.countable_LomegaEquiv_implies_iso_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] : L.LomegaEquiv M N → Nonempty (L.Equiv M N)

Conditional variant of countable_LomegaEquiv_implies_iso.

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

For countable structures, potential isomorphism implies actual isomorphism.

This is proved by direct back-and-forth construction on the PotentialIso family, avoiding the need for Scott sentences or Karp's theorem.

theorem FirstOrder.Language.countable_InfEquivW_implies_iso {L : Language} [L.IsRelational] {M N : Type w} [L.Structure M] [L.Structure N] [Countable M] [Countable N] : L.InfEquivW M N → Nonempty (L.Equiv M N)

For countable structures, L∞ω-elementary equivalence implies isomorphism.

Unconditional: Karp's theorem turns the equivalence into a potential isomorphism, and back-and-forth on countable structures turns that into an isomorphism. Neither step needs a refinement hypothesis or a countable language, so unlike the Lω₁ω statement below this one has no _of variant to discharge.

theorem FirstOrder.Language.countable_BFEquiv_all_implies_iso {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] (h : ∀ (α : Ordinal.{w}), BFEquiv α 0 Fin.elim0 Fin.elim0) : Nonempty (L.Equiv M N)

For countable structures, BFEquiv at all ordinals implies isomorphism.

Unconditional Wrappers (via CRH)

theorem FirstOrder.Language.countable_LomegaEquiv_implies_iso {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] : L.LomegaEquiv M N → Nonempty (L.Equiv M N)

For countable structures in a countable relational language, Lω₁ω-elementary equivalence implies isomorphism.

Witness-generated back-and-forth systems

Two endpoints for callers who already hold a back-and-forth system. Both are the direct composition with PotentialIso.countable_toEquiv, which remains the sole implementation of the eventual isomorphism.

Countability of the two carriers is the only countability needed — in particular no [Countable (Σ l, L.Relations l)], which the omit clauses below enforce rather than merely assert. That matches countable_InfEquivW_implies_iso and contrasts with the Lω₁ω route.

theorem FirstOrder.Language.countable_extensionFamily_implies_iso {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable 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')) : Nonempty (L.Equiv M N)

From a relation-form extension family to an isomorphism.

Tuples are arbitrary functions Fin n → M, so repeated coordinates are supported; atomic compatibility is exactly SameAtomicType. No complete types, elementary maps, Scott sentences or formula invariance are involved, and the relational language need not be countable.

theorem FirstOrder.Language.ExtensionPresentation.countable_toEquiv {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] (P : L.ExtensionPresentation M N) : Nonempty (L.Equiv M N)

From a proof-relevant state presentation to an isomorphism.

Acceptance tests

The identity system, in both presentations, including the empty-tuple case.