Morley's Counting Theorem via Scott-Height Stratification

This file proves the full Morley counting theorem: for any Lω₁ω sentence φ, the number of isomorphism classes of countable models is either ≤ ℵ₁ or exactly 2^ℵ₀. The theorem is parametrized by the Silver–Burgess dichotomy (SilverBurgessDichotomy), which the repository proves unconditionally (silverBurgessDichotomy in Conditional/GandyHarrington.lean, via the classical G₀-dichotomy route); supplying it makes the conclusion axiom-clean.

The proof stratifies by Scott height. For each α < ω₁, BFEquiv_α is a Borel equivalence relation on ModelsOf φ, coarser than isomorphism. If any BFEquiv_α has 2^ℵ₀ classes, iso has ≥ 2^ℵ₀ hence = 2^ℵ₀. If all have ≤ ℵ₀, then for each α, the iso classes with height ≤ α inject into BFEquiv_α classes, giving ≤ ℵ₀ iso classes per stratum, hence ≤ ℵ₁ total over ω₁ strata.

Main Result

• morley_counting: Morley counting theorem for all countable models, parametrized by SilverBurgessDichotomy (proved in this repository).

BFEquiv setoid on coded models

def FirstOrder.Language.bfEquivSetoid {L : Language} [L.IsRelational] (φ : L.Sentenceω) (α : Ordinal.{0}) : Setoid ↑(ModelsOf φ)

The BFEquiv α equivalence relation on coded ℕ-models of φ (at the empty tuple).

Equations

• FirstOrder.Language.bfEquivSetoid φ α = { r := fun (c₁ c₂ : ↑(FirstOrder.Language.ModelsOf φ)) => FirstOrder.Language.BFEquiv α 0 Fin.elim0 Fin.elim0, iseqv := ⋯ }

theorem FirstOrder.Language.isoSetoid_refines_bfEquivSetoid {L : Language} [L.IsRelational] (φ : L.Sentenceω) (α : Ordinal.{0}) {c₁ c₂ : ↑(ModelsOf φ)} : (isoSetoid φ) c₁ c₂ → (bfEquivSetoid φ α) c₁ c₂

Iso implies BFEquiv α: isoSetoid refines bfEquivSetoid.

theorem FirstOrder.Language.bfEquivSetoid_measurableSet {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (φ : L.Sentenceω) (α : Ordinal.{0}) (hα : α < Ordinal.omega 1) : MeasurableSet {p : ↑(ModelsOf φ) × ↑(ModelsOf φ) | (bfEquivSetoid φ α) p.1 p.2}

The BFEquiv α relation on ModelsOf φ is measurable.

theorem FirstOrder.Language.bfEquiv_classes_dichotomy {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (silver : SilverBurgessDichotomy) (φ : L.Sentenceω) (α : Ordinal.{0}) (hα : α < Ordinal.omega 1) : Cardinal.mk (Quotient (bfEquivSetoid φ α)) ≤ Cardinal.aleph0 ∨ Cardinal.mk (Quotient (bfEquivSetoid φ α)) = Cardinal.continuum

Per-level BFEquiv dichotomy.

theorem FirstOrder.Language.bfEquiv_classes_le_iso_classes {L : Language} [L.IsRelational] (φ : L.Sentenceω) (α : Ordinal.{0}) : Cardinal.mk (Quotient (bfEquivSetoid φ α)) ≤ Cardinal.mk (Quotient (isoSetoid φ))

Refinement gives: #(BFEquiv α classes) ≤ #(iso classes).

Height function on iso classes

noncomputable def FirstOrder.Language.isoClassHeight {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {φ : L.Sentenceω} (q : Quotient (isoSetoid φ)) : Ordinal.{0}

scottHeight lifted to the ℕ-model quotient.

Equations

• FirstOrder.Language.isoClassHeight q = Quotient.lift (fun (c : ↑(FirstOrder.Language.ModelsOf φ)) => FirstOrder.Language.scottHeight ℕ) ⋯ q

theorem FirstOrder.Language.isoClassHeight_lt_omega1 {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {φ : L.Sentenceω} (q : Quotient (isoSetoid φ)) : isoClassHeight q < Ordinal.omega 1

Every ℕ-model iso class has height < ω₁.

Morley counting: ℕ-coded models

theorem FirstOrder.Language.morley_counting_coded {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (silver : SilverBurgessDichotomy) (φ : L.Sentenceω) : Cardinal.mk (Quotient (isoSetoid φ)) ≤ Cardinal.aleph 1 ∨ Cardinal.mk (Quotient (isoSetoid φ)) = Cardinal.continuum

Morley counting for ℕ-coded models: ≤ ℵ₁ or = 2^ℵ₀.

Full Morley counting theorem

theorem FirstOrder.Language.morley_counting {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (silver : SilverBurgessDichotomy) (φ : L.Sentenceω) : Cardinal.mk (AllCodedIsoClasses φ) ≤ Cardinal.aleph 1 ∨ Cardinal.mk (AllCodedIsoClasses φ) = Cardinal.continuum

Morley's counting theorem (conditional on Silver-Burgess): the number of isomorphism classes of countable models of an Lω₁ω sentence is either ≤ ℵ₁ or exactly 2^ℵ₀.

Combines the ℕ-tier (via Scott-height stratification + BFEquiv Borelness) with finite-carrier tiers (via permutation orbits).