The von Neumann ladder model

The maximal model of the ladder sentence at a general stage α: the levels are the von Neumann stages ladderLevel β := V_{ω+β} (so card (ladderLevel β) = ℶ_β by Mathlib's card_vonNeumann and beth_eq_preBeth), the carrier is the Shrink-transport of the members of ladderLevel (α+1) to Type 0, constants enumerate the countable base V_ω, the level predicate U_i is membership in ladderLevel (idxVal i), and E is ∈. Outputs:

• vStructure_isLadderModel — the transported structure satisfies all six ladder clauses (transitivity of the stages gives extensionality; ranks give limit covering);
• mk_vCarrier — the carrier has size exactly ℶ_{α+1}.

The upper-bound half (every ladder model has size ≤ ℶ_{α+1}) is LadderBound.lean; the per-stage endpoint and the supremum assembly are BethLadder.lean.

noncomputable def FirstOrder.Language.HanfLadder.ladderLevel (β : Ordinal.{0}) : ZFSet.{0}

The β-th ladder level: the von Neumann stage V_{ω+β}.

Equations

• FirstOrder.Language.HanfLadder.ladderLevel β = ZFSet.vonNeumann (Ordinal.omega0 + β)

theorem FirstOrder.Language.HanfLadder.card_ladderLevel (β : Ordinal.{0}) : (ladderLevel β).card = Cardinal.beth β

theorem FirstOrder.Language.HanfLadder.ladderLevel_subset {β γ : Ordinal.{0}} (h : β ≤ γ) : ladderLevel β ⊆ ladderLevel γ

theorem FirstOrder.Language.HanfLadder.isTransitive_ladderLevel (β : Ordinal.{0}) : (ladderLevel β).IsTransitive

theorem FirstOrder.Language.HanfLadder.ladderLevel_add_one (β : Ordinal.{0}) : ladderLevel (β + 1) = (ladderLevel β).powerset

noncomputable def FirstOrder.Language.HanfLadder.omegaEnum : ℕ ≃ Shrink.{0, 1} ↥(ladderLevel 0)

The countable enumeration of the base level V_ω.

Equations

• FirstOrder.Language.HanfLadder.omegaEnum = Classical.choice FirstOrder.Language.HanfLadder.omegaEnum._proof_2

noncomputable def FirstOrder.Language.HanfLadder.omegaEnumZ (n : ℕ) : ZFSet.{0}

The n-th base element, as a ZFSet.

Equations

• FirstOrder.Language.HanfLadder.omegaEnumZ n = ↑((equivShrink ↥(FirstOrder.Language.HanfLadder.ladderLevel 0)).symm (FirstOrder.Language.HanfLadder.omegaEnum n))

theorem FirstOrder.Language.HanfLadder.omegaEnumZ_mem (n : ℕ) : omegaEnumZ n ∈ ladderLevel 0

theorem FirstOrder.Language.HanfLadder.omegaEnumZ_surjective {z : ZFSet.{0}} (hz : z ∈ ladderLevel 0) : ∃ (n : ℕ), omegaEnumZ n = z

noncomputable def FirstOrder.Language.HanfLadder.VCarrier (α : Ordinal.{0}) : Type

The model carrier: the members of V_{ω+α+1}, shrunk to Type 0.

Equations

• FirstOrder.Language.HanfLadder.VCarrier α = Shrink.{0, 1} ↥(FirstOrder.Language.HanfLadder.ladderLevel (α + 1))

noncomputable def FirstOrder.Language.HanfLadder.toZ (α : Ordinal.{0}) (x : VCarrier α) : ZFSet.{0}

The underlying ZFSet of a carrier element.

Equations

• FirstOrder.Language.HanfLadder.toZ α x = ↑((equivShrink ↥(FirstOrder.Language.HanfLadder.ladderLevel (α + 1))).symm x)

theorem FirstOrder.Language.HanfLadder.toZ_mem (α : Ordinal.{0}) (x : VCarrier α) : toZ α x ∈ ladderLevel (α + 1)

theorem FirstOrder.Language.HanfLadder.toZ_injective (α : Ordinal.{0}) : Function.Injective (toZ α)

theorem FirstOrder.Language.HanfLadder.toZ_surjective (α : Ordinal.{0}) {z : ZFSet.{0}} (hz : z ∈ ladderLevel (α + 1)) : ∃ (x : VCarrier α), toZ α x = z

@[reducible]

noncomputable def FirstOrder.Language.HanfLadder.vStructure (α : Ordinal.{0}) : (ladderLang α).Structure (VCarrier α)

The von Neumann ladder structure: constants enumerate the base, U_i is membership in ladderLevel (idxVal i), and E is ∈.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.HanfLadder.toZ_constVal (α : Ordinal.{0}) (n : ℕ) : toZ α (constVal α n) = omegaEnumZ n

theorem FirstOrder.Language.HanfLadder.vStructure_isLadderModel (α : Ordinal.{0}) : IsLadderModel α

The six ladder clauses hold in the von Neumann model.

theorem FirstOrder.Language.HanfLadder.mk_vCarrier (α : Ordinal.{0}) : Cardinal.mk (VCarrier α) = Cardinal.beth (α + 1)

The von Neumann model has size exactly ℶ_{α+1}.