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.
• morley_hanf_of_transfer: The Hanf number for Lω₁ω sentences in a countable language is bounded by ℶ_ω₁, conditional on MorleyHanfTransfer.

Definitions

• MorleyHanfTransfer: Deep combinatorial transfer hypothesis encapsulating Erdős-Rado extraction and Ehrenfeucht-Mostowski stretching for Lω₁ω.

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ω₁ω.

def FirstOrder.Language.MorleyHanfTransfer (L : Language) [Countable ((l : ℕ) × L.Relations l)] : Prop

Deep set-theoretic/model-theoretic transfer hypothesis for the Morley-Hanf theorem.

This encapsulates the combined content of:

1. Erdős-Rado extraction: Models of size ≥ ℶ_{ω₁} in a countable language contain Lω₁ω-indiscernible sequences of uncountable length.
2. Ehrenfeucht-Mostowski stretching: Such indiscernible sequences can be stretched to produce models of arbitrary size satisfying the same Lω₁ω sentences.

These deep combinatorial arguments (Ramsey/partition calculus + EM functors) require infrastructure not currently formalized in Lean or Mathlib.

See [Mar16], §5; [KK04], §1.6.

Equations

• L.MorleyHanfTransfer = ∀ (φ : L.Sentenceω) (M : Type) [inst : L.Structure M], φ.Realize M → Cardinal.mk M ≥ Cardinal.beth (Ordinal.omega 1) → FirstOrder.Language.HasArbLargeModels φ

theorem FirstOrder.Language.morley_hanf_of_transfer {L : Language} [Countable ((l : ℕ) × L.Relations l)] (htransfer : L.MorleyHanfTransfer) (φ : L.Sentenceω) : IsHanfBound φ (Cardinal.beth (Ordinal.omega 1))

Morley-Hanf Theorem (conditional on transfer hypothesis).

For a countable language, the Hanf number of any Lω₁ω sentence is bounded by ℶ_ω₁ (the ω₁-th beth number), assuming the deep combinatorial transfer principle MorleyHanfTransfer.

The unconditional version requires formalizing Erdős-Rado partition calculus and Ehrenfeucht-Mostowski functors for Lω₁ω, which are not currently available in Lean or Mathlib.

Boundary: The hypothesis htransfer captures exactly the deep set-theoretic/model-theoretic transfer step. All other reasoning is formalized.