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

Height function on iso classes

Morley counting: ℕ-coded models

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).