Morley's theorem on the number of countable models

How many countable models can an infinitary sentence φ with countable branching have, up to isomorphism, in a relational language with countably many relation symbols of each arity? Morley's theorem answers: either at most ℵ₁, or φ has a nonempty perfect set of pairwise non-isomorphic countable models, and therefore continuum many. Neither the continuum hypothesis nor its negation is assumed: under the continuum hypothesis ℵ₁ and 𝔠 coincide, so the witnessed form with a perfect set is strictly more informative than the cardinal dichotomy "≤ ℵ₁ or = 𝔠".

Isomorphism of structures on ℕ is analytic rather than Borel in general, so Silver's theorem cannot be applied to it directly. Instead, Silver's theorem enters level by level through the decreasing hierarchy of back-and-forth equivalence relations bfEquivSetoid L ℕ α (TauCeti.RelationalConfiguration.countable_quotient_comap_bfEquivSetoid_or_hasPerfectAntichainOn). On ℕ, if a Borel set K contains no perfect set of pairwise non-isomorphic configurations, every countable back-and-forth level on K has countably many classes (TauCeti.BFScattered.of_isThinOn), and the isolating-rank stratification bound (TauCeti.mk_isoClasses_le_aleph_one_of_countable_levels) bounds the isomorphism classes met by K by ℵ₁ (TauCeti.mk_isoClasses_le_aleph_one_or_hasPerfectAntichainOn). Specializing to the Borel model class modelsOf φ on ℕ and combining with the finite-carrier dichotomy across all Fin n (TauCeti.sum_mk_quotient_isoSetoidOn_fin_le_aleph0_or_hasPerfectlyManyCountableModels) yields Morley's theorem in its witnessed form (TauCeti.morley_countableModelCount_le_aleph_one_or_hasPerfectlyMany), from which the cardinal form (TauCeti.morley_countableModelCount) follows via TauCeti.HasPerfectlyManyCountableModels.countableModelCount_eq. The purely cardinal transfer from levelwise and finite-tier "≤ ℵ₀ or = 𝔠" dichotomies to "≤ ℵ₁ or = 𝔠" is also isolated in TauCeti.countableModelCount_le_aleph_one_or_eq_continuum_of_dichotomy, without assuming a countable language, countable branching, or Cantor or perfect antichains.

Finally, TauCeti.IsThinOnNatModels φ records that modelsOf (V := ℕ) φ carries no perfect set of pairwise non-isomorphic configurations. A thin sentence is back-and-forth scattered on ℕ, has at most ℵ₁ models on ℕ (and exactly ℵ₁ when uncountable), and has countably many models on ℕ precisely when any isolating rank is bounded below ω₁ on its models on ℕ. Conversely, fewer than 𝔠 models on ℕ forces φ to be thin and hence scattered.

Main definitions

• TauCeti.IsThinOnNatModels φ: the model class of φ on ℕ contains no nonempty perfect set of pairwise non-isomorphic configurations.

Main results

• TauCeti.mk_isoClasses_le_aleph_one_or_hasPerfectAntichainOn and TauCeti.mk_isoClasses_le_aleph_one_or_eq_continuum: a Borel set of configurations on ℕ meets at most ℵ₁ isomorphism classes or contains a nonempty perfect set of pairwise non-isomorphic configurations (hence ≤ ℵ₁ or = 𝔠).
• TauCeti.mk_quotient_isoSetoidOn_nat_le_aleph_one_or_hasPerfectAntichainOn and TauCeti.mk_quotient_isoSetoidOn_nat_le_aleph_one_or_eq_continuum: Morley's dichotomy on the tier ℕ.
• TauCeti.morley_countableModelCount_le_aleph_one_or_hasPerfectlyMany and TauCeti.morley_countableModelCount: Morley's theorem in witnessed and cardinal forms.
• TauCeti.countableModelCount_le_aleph_one_or_eq_continuum_of_dichotomy: the cardinal form of Morley's theorem from abstract levelwise and finite-tier "≤ ℵ₀ or = 𝔠" dichotomies.
• TauCeti.IsThinOnNatModels.bfScattered_modelsOf, TauCeti.IsThinOnNatModels.mk_quotient_isoSetoidOn_le_aleph_one, TauCeti.IsThinOnNatModels.mk_quotient_isoSetoidOn_eq_aleph_one, TauCeti.IsThinOnNatModels.countable_quotient_isoSetoidOn_iff_bounded, and TauCeti.isThinOnNatModels_of_mk_quotient_lt_continuum: thin sentences on ℕ, their level and isomorphism-class counts, and thinness from fewer than 𝔠 models.

References

• M. Morley, The number of countable models, J. Symbolic Logic 35 (1970), 14–18.
• J. H. Silver, Counting the number of equivalence classes of Borel and coanalytic equivalence relations, Annals of Mathematical Logic 18 (1980), 1–28.
• A. Montalbán, Computable Structure Theory: Beyond the Arithmetic, Part 2, Chapter XII, §XII.1 (Morley's theorem via Silver's theorem).
• D. Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016, the chapters on the space of countable models and Vaught counterexamples.
• The counting assembly follows morley_counting in InfinitaryLogic/ModelTheory/MorleyCounting.lean, morley_counting_or_perfect and morley_counting_or_perfect_cardinal in InfinitaryLogic/Conditional/MorleyPerfect.lean, and IsThinOnNatModels in InfinitaryLogic/Descriptive/StructureIsoSetoid.lean of Cameron Freer's cameronfreer/infinitary-logic (checkpoint 518a366cba97b1ae8c4dc64a297a396939bc3e0b, Apache-2.0). There morley_counting counts coded models in Type from a dichotomy hypothesis; here Silver's theorem is discharged unconditionally, Borel configuration sets are covered before specializing to model classes, the finite tiers are included, and the language and branching universes are arbitrary.

Borel sets of configurations on ℕ

theorem TauCeti.mk_isoClasses_le_aleph_one_or_hasPerfectAntichainOn {L : FirstOrder.Language} [L.IsRelational] [∀ (n : ℕ), Countable (L.Relations n)] {K : Set (RelationalConfiguration L ℕ)} (hK : MeasurableSet K) : Cardinal.mk (Quotient (Setoid.comap Subtype.val (RelationalConfiguration.isoSetoid L ℕ))) ≤ Cardinal.aleph 1 ∨ (RelationalConfiguration.isoSetoid L ℕ).HasPerfectAntichainOn K

Morley's dichotomy for Borel sets on ℕ. In a relational language with countably many relation symbols of each arity, any Borel set K of configurations on ℕ meets at most ℵ₁ isomorphism classes or contains a nonempty perfect set of pairwise non-isomorphic configurations. No isomorphism invariance of K is required.

theorem TauCeti.mk_isoClasses_le_aleph_one_or_eq_continuum {L : FirstOrder.Language} [L.IsRelational] [∀ (n : ℕ), Countable (L.Relations n)] {K : Set (RelationalConfiguration L ℕ)} (hK : MeasurableSet K) : Cardinal.mk (Quotient (Setoid.comap Subtype.val (RelationalConfiguration.isoSetoid L ℕ))) ≤ Cardinal.aleph 1 ∨ Cardinal.mk (Quotient (Setoid.comap Subtype.val (RelationalConfiguration.isoSetoid L ℕ))) = Cardinal.continuum

Morley's cardinal dichotomy for Borel sets on ℕ. In a relational language with countably many relation symbols of each arity, any Borel set K of configurations on ℕ meets either at most ℵ₁ or 𝔠 isomorphism classes.

Morley's theorem

theorem TauCeti.mk_quotient_isoSetoidOn_nat_le_aleph_one_or_hasPerfectAntichainOn {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] (φ : L.SentenceInf ι) : Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn ℕ φ)) ≤ Cardinal.aleph 1 ∨ (RelationalConfiguration.isoSetoid L ℕ).HasPerfectAntichainOn (RelationalConfiguration.modelsOf φ)

Morley's dichotomy on the tier ℕ. In a relational language with countably many relation symbols of each arity, the models on ℕ of an infinitary sentence with countable branching have at most ℵ₁ isomorphism classes, or contain a nonempty perfect set of pairwise non-isomorphic models.

theorem TauCeti.mk_quotient_isoSetoidOn_nat_le_aleph_one_or_eq_continuum {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] (φ : L.SentenceInf ι) : Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn ℕ φ)) ≤ Cardinal.aleph 1 ∨ Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn ℕ φ)) = Cardinal.continuum

Morley's cardinal dichotomy on the tier ℕ. In a relational language with countably many relation symbols of each arity, the models of φ on ℕ have either at most ℵ₁ or 𝔠 isomorphism classes.

theorem TauCeti.morley_countableModelCount_le_aleph_one_or_hasPerfectlyMany {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] (φ : L.SentenceInf ι) : countableModelCount φ ≤ Cardinal.aleph 1 ∨ HasPerfectlyManyCountableModels φ

Morley's theorem (witnessed form). In a relational language with countably many relation symbols of each arity, an infinitary sentence with countable branching (in particular every sentence of L_{ω₁ω}) either has at most ℵ₁ countable models up to isomorphism, finite models included, or has a nonempty perfect set of pairwise non-isomorphic countable models at the tier ℕ or at some finite tier Fin n. Neither the continuum hypothesis nor its negation is assumed.

theorem TauCeti.morley_countableModelCount {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] (φ : L.SentenceInf ι) : countableModelCount φ ≤ Cardinal.aleph 1 ∨ countableModelCount φ = Cardinal.continuum

Morley's theorem (cardinal form). In a relational language with countably many relation symbols of each arity, an infinitary sentence with countable branching has either at most ℵ₁ or 𝔠 countable models up to isomorphism. Neither the continuum hypothesis nor its negation is assumed.

theorem TauCeti.countableModelCount_le_aleph_one_or_eq_continuum_of_dichotomy {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} (hlevels : ∀ α < Ordinal.omega 1, Cardinal.mk (Quotient (RelationalConfiguration.bfEquivSetoidOn ℕ φ α)) ≤ Cardinal.aleph0 ∨ Cardinal.mk (Quotient (RelationalConfiguration.bfEquivSetoidOn ℕ φ α)) = Cardinal.continuum) (hfin : ∀ (n : ℕ), Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ)) ≤ Cardinal.aleph0 ∨ Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ)) = Cardinal.continuum) : countableModelCount φ ≤ Cardinal.aleph 1 ∨ countableModelCount φ = Cardinal.continuum

If every countable back-and-forth level on ℕ and every finite carrier Fin n has either at most ℵ₀ or 𝔠 classes of models of φ, then φ has either at most ℵ₁ or 𝔠 countable models up to isomorphism. No countability assumption on the language or on the branching index ι is required.

theorem TauCeti.countableModelCount_le_aleph_one_of_not_hasPerfectlyManyCountableModels {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] {φ : L.SentenceInf ι} (h : ¬HasPerfectlyManyCountableModels φ) : countableModelCount φ ≤ Cardinal.aleph 1

A sentence without perfectly many countable models has at most ℵ₁ countable models up to isomorphism.

theorem TauCeti.countableModelCount_eq_aleph_one_of_aleph0_lt_of_not_hasPerfectlyManyCountableModels {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] {φ : L.SentenceInf ι} (h₀ : Cardinal.aleph0 < countableModelCount φ) (h : ¬HasPerfectlyManyCountableModels φ) : countableModelCount φ = Cardinal.aleph 1

A sentence with uncountably many countable models and no perfect set of pairwise non-isomorphic countable models has ℵ₁ countable models up to isomorphism.

theorem TauCeti.countableModelCount_eq_aleph_one_of_aleph0_lt_of_lt_continuum {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] {φ : L.SentenceInf ι} (h₀ : Cardinal.aleph0 < countableModelCount φ) (hc : countableModelCount φ < Cardinal.continuum) : countableModelCount φ = Cardinal.aleph 1

A sentence with uncountably many, yet fewer than continuum many, countable models has ℵ₁ countable models up to isomorphism.

Thin sentences

def TauCeti.IsThinOnNatModels {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} (φ : L.SentenceInf ι) : Prop

An infinitary sentence is thin on its models on ℕ when its model class on ℕ contains no nonempty perfect set of pairwise non-isomorphic configurations.

theorem TauCeti.isThinOnNatModels_iff_isThinOn {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} : IsThinOnNatModels φ ↔ (RelationalConfiguration.isoSetoid L ℕ).IsThinOn (RelationalConfiguration.modelsOf φ)

TauCeti.IsThinOnNatModels is Setoid.IsThinOn for isomorphism on the model class on ℕ.

theorem TauCeti.isThinOnNatModels_iff {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} : IsThinOnNatModels φ ↔ ¬(RelationalConfiguration.isoSetoid L ℕ).HasPerfectAntichainOn (RelationalConfiguration.modelsOf φ)

Unfolding lemma for TauCeti.IsThinOnNatModels in terms of Setoid.HasPerfectAntichainOn.

@[simp]

theorem TauCeti.isThinOnNatModels_bot {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} : IsThinOnNatModels ⊥

The false sentence has no models on ℕ, hence is thin on ℕ.

theorem TauCeti.isThinOnNatModels_iff_not_hasCantorAntichainOn {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] {φ : L.SentenceInf ι} : IsThinOnNatModels φ ↔ ¬(RelationalConfiguration.isoSetoid L ℕ).HasCantorAntichainOn (RelationalConfiguration.modelsOf φ)

In a vocabulary with countably many relation symbols of each arity, a sentence is thin on ℕ exactly when its model class on ℕ carries no Cantor antichain of pairwise non-isomorphic models.

theorem TauCeti.IsThinOnNatModels.of_subset {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {ι' : Type uι'} {φ : L.SentenceInf ι} {ψ : L.SentenceInf ι'} (h : RelationalConfiguration.modelsOf φ ⊆ RelationalConfiguration.modelsOf ψ) (hψ : IsThinOnNatModels ψ) : IsThinOnNatModels φ

Thinness on ℕ passes to any sentence whose models on ℕ are models of a thin sentence.

theorem TauCeti.not_hasPerfectlyManyCountableModels_iff {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} : ¬HasPerfectlyManyCountableModels φ ↔ IsThinOnNatModels φ ∧ ∀ (n : ℕ), (RelationalConfiguration.isoSetoid L (Fin n)).IsThinOn (RelationalConfiguration.modelsOf φ)

A sentence fails to have perfectly many countable models exactly when it is thin on ℕ and on every finite carrier Fin n.

theorem TauCeti.IsThinOnNatModels.of_not_hasPerfectlyManyCountableModels {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} (h : ¬HasPerfectlyManyCountableModels φ) : IsThinOnNatModels φ

A sentence without perfectly many countable models is thin on ℕ.

theorem TauCeti.IsThinOnNatModels.countable_quotient_bfEquivSetoidOn {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] {φ : L.SentenceInf ι} (h : IsThinOnNatModels φ) {α : Ordinal.{o}} (hα : α < Ordinal.omega 1) : Countable (Quotient (RelationalConfiguration.bfEquivSetoidOn ℕ φ α))

A sentence that is thin on ℕ has countably many depth-α back-and-forth classes of models on ℕ at every countable ordinal α.

theorem TauCeti.IsThinOnNatModels.bfScattered_modelsOf {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] {φ : L.SentenceInf ι} (h : IsThinOnNatModels φ) : BFScattered (RelationalConfiguration.modelsOf φ)

Thin sentences are back-and-forth scattered. If φ is thin on ℕ, its model class on ℕ is back-and-forth scattered.

theorem TauCeti.IsThinOnNatModels.mk_quotient_isoSetoidOn_le_aleph_one {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] {φ : L.SentenceInf ι} (h : IsThinOnNatModels φ) : Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn ℕ φ)) ≤ Cardinal.aleph 1

A sentence that is thin on ℕ has at most ℵ₁ models on ℕ up to isomorphism.

theorem TauCeti.IsThinOnNatModels.mk_quotient_isoSetoidOn_eq_aleph_one {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] {φ : L.SentenceInf ι} (h : IsThinOnNatModels φ) [Uncountable (Quotient (RelationalConfiguration.isoSetoidOn ℕ φ))] : Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn ℕ φ)) = Cardinal.aleph 1

A sentence that is thin on ℕ and has uncountably many models on ℕ up to isomorphism has ℵ₁ of them.

theorem TauCeti.IsThinOnNatModels.countable_quotient_isoSetoidOn_iff_bounded {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] {φ : L.SentenceInf ι} (h : IsThinOnNatModels φ) {ρ : RelationalConfiguration L ℕ → Ordinal.{0}} (hρ : IsIsolatingRank ρ) : Countable (Quotient (RelationalConfiguration.isoSetoidOn ℕ φ)) ↔ ∃ β < Ordinal.omega 1, ∀ c ∈ RelationalConfiguration.modelsOf φ, ρ c < β

A sentence that is thin on ℕ has countably many models on ℕ up to isomorphism if and only if any given isolating rank is bounded below ω₁ on its model class on ℕ.

theorem TauCeti.isThinOnNatModels_of_mk_quotient_lt_continuum {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] {φ : L.SentenceInf ι} (h : Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn ℕ φ)) < Cardinal.continuum) : IsThinOnNatModels φ

If φ has fewer than continuum many models on ℕ up to isomorphism, then φ is thin on ℕ. No countability assumption on the branching index ι is required.

theorem TauCeti.not_hasPerfectlyManyCountableModels_of_lt_continuum {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] {φ : L.SentenceInf ι} (h : countableModelCount φ < Cardinal.continuum) : ¬HasPerfectlyManyCountableModels φ

If φ has fewer than continuum many countable models in total, it has no perfect set of pairwise non-isomorphic countable models at any tier.

theorem TauCeti.bfScattered_modelsOf_of_mk_quotient_lt_continuum {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] {φ : L.SentenceInf ι} (h : Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn ℕ φ)) < Cardinal.continuum) : BFScattered (RelationalConfiguration.modelsOf φ)

If an infinitary sentence with countable branching has fewer than continuum many models on ℕ up to isomorphism, its model class on ℕ is back-and-forth scattered.