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

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.