The powerset witness: ladder stage α = 0

The α = 0 instance of the common ladder sentence (HanfSpectrum/LadderSyntax.lean): the index order Index 0 has exactly the two levels ⊥ ⋖ ⊤, so a ladder model is a set of "elements" (U_⊤ = everything) whose E-predecessors all lie in the countable base U_⊥ (enumerated by the constants), with E-extensionality. The maximal model is the full powerset:

• powersetStructure — Set ℕ with cₙ = {n}, U_⊥ = the singletons, E x y ↔ ∃ n, x = {n} ∧ n ∈ y; it satisfies IsLadderModel 0 and has size 2 ^ ℵ₀;
• mk_le_continuum_of_isLadderModel — EVERY ladder model at α = 0 has size ≤ 2 ^ ℵ₀ (E-extensionality injects M into the powerset of the countable U_⊥);
• beth_one_lt_Lomega1omegaHanfNumber — the second sharpness step, through the generic bounded-spectrum endpoint lt_Lomega1omegaHanfNumber_of_maximal_model.

The two-element order facts (covBy_of_lt_index_zero, not_isSuccLimit_index_zero) are isolated here so they do not contaminate the model verification; the general-stage analogues (typein-recursion) belong to BethLadder.lean.

Reference: Marker, Lectures on Infinitary Model Theory, Exercise 5.3 (the φ_1 stage).

The two-element index order Index 0

instance FirstOrder.Language.HanfLadder.instCountableIndexOfNatOrdinal : Countable (Index 0)

theorem FirstOrder.Language.HanfLadder.bot_lt_top_index : ⊥ < ⊤

theorem FirstOrder.Language.HanfLadder.covBy_of_lt_index_zero {i j : Index 0} (hij : i < j) : i ⋖ j

In the two-element order Index 0, every strict inequality is a covering: there is no middle element (the typein values would form a strict 3-chain below 2).

theorem FirstOrder.Language.HanfLadder.not_isSuccLimit_index_zero (j : Index 0) : ¬Order.IsSuccLimit j

The two-element order Index 0 has no successor-limit elements.

The powerset model on Set ℕ

@[reducible]

def FirstOrder.Language.HanfLadder.powersetStructure : (ladderLang 0).Structure (Set ℕ)

The powerset structure: constants are the singletons, U_⊥ is the set of singletons (U_i trivial for i ≠ ⊥), and E x y says x is a singleton {n} with n ∈ y.

Equations

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

theorem FirstOrder.Language.HanfLadder.powerset_isLadderModel : IsLadderModel 0

The upper bound: every α = 0 ladder model has size ≤ 2 ^ ℵ₀

theorem FirstOrder.Language.HanfLadder.edge_mem_base_of_isLadderModel {M : Type} [(ladderLang 0).Structure M] (h : IsLadderModel 0) {x y : M} (hxy : Edge 0 x y) : Level 0 ⊥ x

In any α = 0 ladder model, E-predecessors lie in the base level: ⊥ ⋖ ⊤, everything is in U_⊤, and predecessor descent lands in U_⊥.

theorem FirstOrder.Language.HanfLadder.mk_le_continuum_of_isLadderModel {M : Type} [(ladderLang 0).Structure M] (h : IsLadderModel 0) : Cardinal.mk M ≤ 2 ^ Cardinal.aleph0

The maximal-size bound at α = 0: E-extensionality injects the model into the powerset of the countable base level.

theorem FirstOrder.Language.beth_one_lt_Lomega1omegaHanfNumber : Cardinal.beth 1 < Lomega1omegaHanfNumber

The second sharpness step: ℶ_1 < Lomega1omegaHanfNumber — the α = 0 ladder sentence has the powerset Set ℕ as a maximal model of size exactly 2 ^ ℵ₀ = ℶ_1.