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.ladderLevel_subset {β γ : Ordinal.{0}} (h : β ≤ γ) : ladderLevel β ⊆ ladderLevel γ

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

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)

@[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.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}.