Countable Corollary to Karp's Theorem

This file proves that for countable structures, Lω₁ω-elementary equivalence (and hence L∞ω-elementary equivalence) implies isomorphism.

Main Results

• countable_LomegaEquiv_implies_iso: For countable structures in a countable relational language, Lω₁ω-elementary equivalence implies isomorphism (KK04 Corollary 1.2.2).
• countable_LinfEquiv_implies_iso: Same result for L∞ω-elementary equivalence.

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_LinfEquiv_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.LinfEquiv M N → Nonempty (L.Equiv M N)

Conditional variant of countable_LinfEquiv_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_BFEquiv_all_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] (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.

theorem FirstOrder.Language.countable_LinfEquiv_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.LinfEquiv M N → Nonempty (L.Equiv M N)

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