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 bySilverBurgessDichotomy(proved in this repository).
BFEquiv setoid on coded models #
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 := ⋯ }
Instances For
Iso implies BFEquiv α: isoSetoid refines bfEquivSetoid.
The BFEquiv α relation on ModelsOf φ is measurable.
Per-level BFEquiv dichotomy.
The depth-α projection of isomorphism classes onto back-and-forth classes.
Equations
Instances For
The depth-α projection of the isomorphism classes satisfying P: the range of bfProj
restricted to P.
Equations
- FirstOrder.Language.bfProjRange φ P α = Set.range fun (q : { q : Quotient (FirstOrder.Language.isoSetoid φ) // P q }) => FirstOrder.Language.bfProj φ α ↑q
Instances For
Refinement gives: #(BFEquiv α classes) ≤ #(iso classes).
Height function on iso classes #
scottHeight lifted to the ℕ-model quotient.
Equations
- FirstOrder.Language.isoClassHeight q = Quotient.lift (fun (c : ↑(FirstOrder.Language.ModelsOf φ)) => FirstOrder.Language.scottHeight ℕ) ⋯ q
Instances For
Every ℕ-model iso class has height < ω₁.
Morley counting: ℕ-coded models #
Height comparison. Two coded models that are back-and-forth equivalent at a countable
depth α bounding the Scott height of the first are isomorphic. This is the only place the
stratification argument consults the Scott height, and it is exposed so that variants of the
stratification (relativized to a subclass of isomorphism classes, or with weaker per-level
bounds) can reuse it.
Every countable-carrier structure space has at most continuum-many points: it is a
Bool-valued function space on a countable index.
Stated for an arbitrary countable carrier rather than for ℕ alone, since the finite tiers need
exactly the same bound at Fin n.
The cardinality of StructureSpace L is at most continuum.
The Scott-height stratification bound, relativized. Let P be any collection of
isomorphism classes of coded models of φ. If for every α < ω₁ the depth-α back-and-forth
projection of P (bfProjRange φ P α) has size at most ℵ₁, then P has at most ℵ₁ members.
The height-α classes in P inject into that range (bfEquiv_at_height_implies_iso), and the
union over the ω₁ heights is bounded by ℵ₁ · ℵ₁ = ℵ₁. Two things are deliberately weaker
than in the unrelativized statement: only the classes in P are counted at each level, and each
level is allowed ℵ₁ rather than ℵ₀ classes.
The relativized stratification bound with countable levels: if for every α < ω₁ the
depth-α projection of P has countable range, then P has at most ℵ₁ members.
The Scott-height stratification bound. If every back-and-forth level below ω₁ has only
countably many classes, then isomorphism has at most ℵ₁ classes. This is the case P := ⊤ of
mk_isoSetoid_subtype_le_aleph_one_of_countable_levels; both morley_counting_coded and the
witness-bearing route consume it, since the stratification argument is indifferent to how the
countability of each level was established.
Morley counting for ℕ-coded models: ≤ ℵ₁ or = 2^ℵ₀.
Full Morley counting theorem #
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).