Counting Theorem for All Countable Models

This file provides the user-facing counting theorem for all countable models of an Lω₁ω sentence with bounded Scott height. It combines the ℕ-coded result (via BF-equivalence Borelness) with finite-carrier results (via permutation orbits) from FiniteCarrier.lean.

The type AllCodedIsoClasses φ faithfully represents all isomorphism classes of countable models of φ, as established by the bridge theorems:

• codeModel: maps any countable model to a coded iso class
• codeModel_eq_of_iso: L-isomorphic models yield the same class
• iso_of_codeModel_eq: same class implies L-isomorphic
• codeModel_surjective: every class is realized

Main Result

• counting_countable_models_bounded_scottHeight: The number of isomorphism classes of countable models (with bounded Scott height) is ≤ ℵ₀ or = 2^ℵ₀.

The stronger unconditional-height version (≤ ℵ₁ or 2^ℵ₀) is FirstOrder.Language.morley_counting in ModelTheory/MorleyCounting.lean.

theorem FirstOrder.Language.counting_countable_models_bounded_scottHeight {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (silver : SilverBurgessDichotomy) {φ : L.Sentenceω} {α : Ordinal.{0}} (hα : α < Ordinal.omega 1) (hbound : ∀ (M : Type) [inst : L.Structure M] [inst_1 : Countable M], φ.Realize M → scottHeight M ≤ α) : Cardinal.mk (AllCodedIsoClasses φ) ≤ Cardinal.aleph0 ∨ Cardinal.mk (AllCodedIsoClasses φ) = Cardinal.continuum

Bounded-Scott-height counting theorem for all countable models. The total number of isomorphism classes of countable models of φ (with bounded Scott height) is either ≤ ℵ₀ or exactly 2^ℵ₀.

This combines ℕ-coded models (BF-equivalence Borelness, counting_coded_models_dichotomy) with finite-carrier models (permutation orbits, counting_fin_models_dichotomy). AllCodedIsoClasses φ faithfully represents all iso classes of countable models (by codeModel, codeModel_eq_of_iso, iso_of_codeModel_eq, codeModel_surjective).