The ladder upper bound #
EVERY model of the six ladder clauses at stage α has size at most ℶ_{α+1} — the
maximal-size half of the Marker Exercise 5.3 spectrum computation. The proof is well-founded
induction on the level index: |U_i| ≤ ℶ_{idxVal i} — the base level is enumerated by the
constants (≤ ℵ₀), a covered level E-extensionally injects into the powerset of its
predecessor (≤ 2^ℶ = ℶ⁺, CardinalBounds.mk_le_two_power_of_injective_set), and a limit
level is a countable union of earlier levels (CardinalBounds.mk_iUnion_le_of_countable).
The top clause then bounds the whole model by |U_⊤| ≤ ℶ_{α+1}.
theorem
FirstOrder.Language.HanfLadder.mk_level_le_beth
{α : Ordinal.{0}}
{M : Type}
[(ladderLang α).Structure M]
[Countable (Index α)]
(h : IsLadderModel α)
(i : Index α)
:
The level bound: in any ladder model, |U_i| ≤ ℶ_{idxVal i}.
theorem
FirstOrder.Language.HanfLadder.mk_le_beth_of_isLadderModel
{α : Ordinal.{0}}
{M : Type}
[(ladderLang α).Structure M]
[Countable (Index α)]
(h : IsLadderModel α)
:
The ladder upper bound: every model of the six clauses has size at most ℶ_{α+1}.