The Morley–Hanf theorem: public facade and corollaries

The stable entry point for the project's headline Hanf-number result. Importing this file (or any bundle containing it, including the default import InfinitaryLogic) exposes

• morley_hanf : IsHanfBound φ (ℶ_ω₁) — for every L_{ω₁ω} sentence over an arbitrary language, with no hypotheses (proved in Conditional/MorleyHanfSchemaDischarge.lean);

together with the corollaries packaged here:

• hanfNumber_le_beth_omega1 — the per-sentence Hanf number is at most ℶ_{ω₁};
• IsLomega1omegaHanfBound / Lomega1omegaHanfNumber — the GLOBAL Hanf bound/number of the logic L_{ω₁ω} (over all languages and sentences), with beth_omega1_isLomega1omegaHanfBound and Lomega1omegaHanfNumber_le_beth_omega1. This is the upper half of the classical Hanf(L_{ω₁ω}) = ℶ_{ω₁}; the matching lower half and the exact equality Lomega1omegaHanfNumber_eq_beth_omega1 are proved by the beth-ladder spectrum witnesses in HanfSpectrum/BethLadder.lean;
• morley_hanf_theory — every countable L_{ω₁ω}-theory with a model of size ≥ ℶ_{ω₁} has arbitrarily large models (via Theoryω.conjunction).

def FirstOrder.Language.IsLomega1omegaHanfBound (κ : Cardinal.{0}) : Prop

A global Hanf bound for the logic L_{ω₁ω}: a cardinal that is a Hanf bound for every sentence of every language.

Equations

• FirstOrder.Language.IsLomega1omegaHanfBound κ = ∀ (L' : FirstOrder.Language) (φ : L'.Sentenceω), FirstOrder.Language.IsHanfBound φ κ

noncomputable def FirstOrder.Language.Lomega1omegaHanfNumber : Cardinal.{0}

The Hanf number of the logic L_{ω₁ω}: the least global Hanf bound.

Equations

• FirstOrder.Language.Lomega1omegaHanfNumber = sInf {κ : Cardinal.{0} | FirstOrder.Language.IsLomega1omegaHanfBound κ}

theorem FirstOrder.Language.IsLomega1omegaHanfBound.mono {κ μ : Cardinal.{0}} (hκ : IsLomega1omegaHanfBound κ) (hκμ : κ ≤ μ) : IsLomega1omegaHanfBound μ

A global Hanf bound stays a bound at every larger cardinal.

theorem FirstOrder.Language.lt_Lomega1omegaHanfNumber_of_maximal_model {L : Language} {φ : L.Sentenceω} {κ : Cardinal.{0}} (hmodel : ∃ (M : Type) (x : L.Structure M), φ.Realize M ∧ κ ≤ Cardinal.mk M) (hupper : ∀ (M : Type) (x : L.Structure M), φ.Realize M → Cardinal.mk M ≤ κ) : κ < Lomega1omegaHanfNumber

The generic bounded-spectrum argument: a sentence with a model of size ≥ κ whose every model has size ≤ κ is not arbitrarily large, so κ is not a global Hanf bound and κ < Lomega1omegaHanfNumber. The common endpoint for the countable witness, the powerset witness, and every stage of the Marker ℶ_{α+1} ladder.

theorem FirstOrder.Language.Lomega1omegaHanfNumber_le_beth_omega1 : Lomega1omegaHanfNumber ≤ Cardinal.beth (Ordinal.omega 1)

The Hanf number of L_{ω₁ω} is at most ℶ_{ω₁} — the upper half of the classical Hanf(L_{ω₁ω}) = ℶ_{ω₁}; the matching lower half and the exact equality Lomega1omegaHanfNumber_eq_beth_omega1 are proved in HanfSpectrum/BethLadder.lean.