Counting Models

This file states model-counting results for Lω₁ω, connecting Scott rank bounds to the structure of the isomorphism relation.

Main Results

• bounded_scottHeight_iso_eq_BFEquiv: When all models of a sentence have Scott height bounded by α, isomorphism equals BF-equivalence at level α.
• morley_counting_dichotomy: Placeholder for the full Morley counting theorem. The conditional bounded-height version is in Descriptive/CountingDichotomy.lean as counting_coded_models_dichotomy.

References

• [Mar16]
• [KK04]

theorem FirstOrder.Language.stabilization_bound_iso_eq_BFEquiv {L : Language} [L.IsRelational] {M N : Type w} [L.Structure M] [L.Structure N] [Countable M] [Countable N] {α : Ordinal.{0}} (_hα : α < Ordinal.omega 1) (hstab : StabilizesCompletely M α) (hBF : BFEquiv α 0 Fin.elim0 Fin.elim0) : Nonempty (L.Equiv M N)

When a structure has StabilizesCompletely M α (with α < ω₁) and BFEquiv α holds, the structures are isomorphic. Unconditional (no CountableRefinementHypothesis needed).

This decouples the isomorphism conclusion from scottRank entirely, taking StabilizesCompletely as a direct hypothesis.

theorem FirstOrder.Language.bounded_scottHeight_iso_eq_BFEquiv_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) {φ : L.Sentenceω} {α : Ordinal.{0}} (hα : α < Ordinal.omega 1) (hbound : ∀ (M : Type w) [inst : L.Structure M] [inst_1 : Countable M], φ.Realize M → scottHeight M ≤ α) {M N : Type w} [L.Structure M] [L.Structure N] [Countable M] [Countable N] (hM : φ.Realize M) (_hN : φ.Realize N) : Nonempty (L.Equiv M N) ↔ BFEquiv α 0 Fin.elim0 Fin.elim0

When all countable models of a sentence have Scott height bounded by α (with α < ω₁), isomorphism between countable models is equivalent to BF-equivalence at level α. Conditional on CountableRefinementHypothesis.

This uses scottHeight (which has a clean conditional relationship to StabilizesCompletely) rather than scottRank.

Unconditional Wrapper (via CRH)

theorem FirstOrder.Language.bounded_scottHeight_iso_eq_BFEquiv {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {φ : L.Sentenceω} {α : Ordinal.{0}} (hα : α < Ordinal.omega 1) (hbound : ∀ (M : Type w) [inst : L.Structure M] [inst_1 : Countable M], φ.Realize M → scottHeight M ≤ α) {M N : Type w} [L.Structure M] [L.Structure N] [Countable M] [Countable N] (hM : φ.Realize M) (hN : φ.Realize N) : Nonempty (L.Equiv M N) ↔ BFEquiv α 0 Fin.elim0 Fin.elim0

When all countable models of a sentence have Scott height bounded by α (with α < ω₁), isomorphism between countable models is equivalent to BF-equivalence at level α.

theorem FirstOrder.Language.morley_counting_dichotomy {L : Language} (_φ : L.Sentenceω) : True

Placeholder for the full Morley counting theorem (the number of isomorphism classes of countable models of an Lω₁ω sentence is either at most ℵ₁ or exactly 2^ℵ₀).

The conditional version is proved as FirstOrder.Language.morley_counting (in ModelTheory/MorleyCounting.lean).