Hanf Numbers

This file defines Hanf numbers for Lω₁ω sentences and states the fundamental existence theorem and the Morley-Hanf bound.

Main Definitions

• HasArbLargeModels: A sentence has arbitrarily large models.
• IsHanfBound: A cardinal κ is a Hanf bound for a sentence φ if having a model of size ≥ κ implies having arbitrarily large models.
• HanfNumber: The least Hanf bound for a sentence.

Main Results

• hanf_existence: Every Lω₁ω sentence has a Hanf number.
• The universal property of HanfNumber: hanfNumber_isHanfBound, hanfNumber_le_of_isHanfBound, hanfNumber_le_iff_isHanfBound, IsHanfBound.mono.

The Morley-Hanf bound itself — morley_hanf : IsHanfBound φ (ℶ_ω₁), unconditional over an arbitrary language — is proved in Conditional/MorleyHanfSchemaDischarge.lean and exposed (with its HanfNumber corollaries) through ModelTheory/MorleyHanf.lean.

References

• [KK04], §1.6
• [Mar16], §5

def FirstOrder.Language.HasArbLargeModels {L : Language} (φ : L.Sentenceω) : Prop

A sentence has arbitrarily large models if for every cardinal κ, there exists a model of size ≥ κ.

Equations

• FirstOrder.Language.HasArbLargeModels φ = ∀ (κ : Cardinal.{0}), ∃ (M : Type) (x : L.Structure M), φ.Realize M ∧ Cardinal.mk M ≥ κ

def FirstOrder.Language.IsHanfBound {L : Language} (φ : L.Sentenceω) (κ : Cardinal.{0}) : Prop

A cardinal κ is a Hanf bound for a sentence φ if the existence of a model of size ≥ κ implies that φ has arbitrarily large models.

Equations

• FirstOrder.Language.IsHanfBound φ κ = ((∃ (M : Type) (x : L.Structure M), φ.Realize M ∧ Cardinal.mk M ≥ κ) → FirstOrder.Language.HasArbLargeModels φ)

noncomputable def FirstOrder.Language.HanfNumber {L : Language} (φ : L.Sentenceω) : Cardinal.{0}

The Hanf number of a sentence is the least cardinal that is a Hanf bound.

Equations

• FirstOrder.Language.HanfNumber φ = sInf {κ : Cardinal.{0} | FirstOrder.Language.IsHanfBound φ κ}

theorem FirstOrder.Language.hanf_existence {L : Language} (φ : L.Sentenceω) : ∃ (κ : Cardinal.{0}), IsHanfBound φ κ

Every Lω₁ω sentence has a Hanf number (i.e., a Hanf bound exists).

This is a fundamental structural result about Lω₁ω.

The universal property of the Hanf number

theorem FirstOrder.Language.IsHanfBound.mono {L : Language} {φ : L.Sentenceω} {κ μ : Cardinal.{0}} (hκ : IsHanfBound φ κ) (hκμ : κ ≤ μ) : IsHanfBound φ μ

A Hanf bound stays a bound at every larger cardinal — the premise only weakens.

theorem FirstOrder.Language.hanfNumber_isHanfBound {L : Language} (φ : L.Sentenceω) : IsHanfBound φ (HanfNumber φ)

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

theorem FirstOrder.Language.hanfNumber_le_of_isHanfBound {L : Language} {φ : L.Sentenceω} {κ : Cardinal.{0}} (hκ : IsHanfBound φ κ) : HanfNumber φ ≤ κ

The Hanf number is the least Hanf bound.

theorem FirstOrder.Language.hanfNumber_le_iff_isHanfBound {L : Language} {φ : L.Sentenceω} {κ : Cardinal.{0}} : HanfNumber φ ≤ κ ↔ IsHanfBound φ κ

The universal property: HanfNumber φ ≤ κ exactly when κ is a Hanf bound (bounds are upward closed and the Hanf number is the least one).

theorem FirstOrder.Language.lt_hanfNumber_iff_not_isHanfBound {L : Language} {φ : L.Sentenceω} {κ : Cardinal.{0}} : κ < HanfNumber φ ↔ ¬IsHanfBound φ κ

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