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

theorem FirstOrder.Language.hanfNumber_le_beth_omega1 {L' : Language} (φ : L'.Sentenceω) : HanfNumber φ ≤ Cardinal.beth (Ordinal.omega 1)

The Hanf number of every L_{ω₁ω} sentence is at most ℶ_{ω₁} — morley_hanf through the universal property of HanfNumber.

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.beth_omega1_isLomega1omegaHanfBound : IsLomega1omegaHanfBound (Cardinal.beth (Ordinal.omega 1))

ℶ_{ω₁} is a global Hanf bound for L_{ω₁ω} — the Morley–Hanf theorem in global form.

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.Lomega1omegaHanfNumber_isHanfBound : IsLomega1omegaHanfBound Lomega1omegaHanfNumber

The global Hanf number is itself a global Hanf bound: the set of bounds is nonempty (beth_omega1_isLomega1omegaHanfBound), and an infimum of cardinals is attained.

theorem FirstOrder.Language.Lomega1omegaHanfNumber_le_of_isHanfBound {κ : Cardinal.{0}} (hκ : IsLomega1omegaHanfBound κ) : Lomega1omegaHanfNumber ≤ κ

The global Hanf number is the least global Hanf bound.

theorem FirstOrder.Language.Lomega1omegaHanfNumber_le_iff_isHanfBound {κ : Cardinal.{0}} : Lomega1omegaHanfNumber ≤ κ ↔ IsLomega1omegaHanfBound κ

The universal property of the global Hanf number: Lomega1omegaHanfNumber ≤ κ exactly when κ is a global Hanf bound. The strict dual κ < H ↔ ¬IsBound κ below is the bounded-spectrum witness-consumption interface.

theorem FirstOrder.Language.lt_Lomega1omegaHanfNumber_iff_not_isHanfBound {κ : Cardinal.{0}} : κ < Lomega1omegaHanfNumber ↔ ¬IsLomega1omegaHanfBound κ

The strict dual of the universal property — the bounded-spectrum witness-consumption interface: refuting the global bound at κ is exactly the strict lower bound κ < Lomega1omegaHanfNumber.

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.

theorem FirstOrder.Language.morley_hanf_theory {L' : Language} (T : L'.Theoryω) (hT : Set.Countable T) (hM : ∃ (M : Type) (x : L'.Structure M), T.Model M ∧ Cardinal.mk M ≥ Cardinal.beth (Ordinal.omega 1)) (κ : Cardinal.{0}) : ∃ (N : Type) (x : L'.Structure N), T.Model N ∧ Cardinal.mk N ≥ κ

The Morley–Hanf theorem for countable theories: every countable L_{ω₁ω}-theory with a model of size at least ℶ_{ω₁} has models of arbitrarily large cardinality — apply morley_hanf to the theory's conjunction (Theoryω.conjunction).