The beth-ladder syntax (Marker, Exercise 5.3)

The common sentence of the bounded-spectrum ladder: for an ordinal α, the language ladderLang α has constants cₙ (n : ℕ), unary level predicates U_i indexed by Index α := (α + 2).ToType (the canonical Type 0 well order of the levels β ≤ α + 1), and one binary relation E. The sentence ladderSentence α asserts, per the audit (docs/hanf-ladder-audit.md):

• base: U_⊥ x ↔ ⋁ₙ x = cₙ;
• top: every element is in U_⊤;
• nesting: U_i ⊆ U_j for i < j;
• limit covering: at an order-limit level j, U_j x → ⋁_{i<j} U_i x;
• predecessor descent: for adjacent levels i ⋖ j, U_j x → E y x → U_i y;
• extensionality: equal E-predecessor sets imply equality.

All clause indexing is INTERNAL to the order on Index α (<, ⋖, Order.IsSuccLimit, ⊥/⊤ from the order instances); typein/enum translation is deferred to the semantic files. Only formation of the countably-indexed sentence needs [Countable (Index α)] (supplied by α < ω₁ downstream); the language itself is Language.{0,0} for every α.

The acceptance interface is the semantic packaging realize_ladderSentence_iff: realization is equivalent to the six named clause predicates bundled in IsLadderModel — downstream files (the α = 0 powerset model, the general upper-bound induction) work with those predicates and never unfold binders, ciInf/ciSup, or valuation bookkeeping again.

@[reducible, inline]

abbrev FirstOrder.Language.HanfLadder.Index (α : Ordinal.{0}) : Type

The level-index order: the canonical Type 0 well order of type α + 2 — the levels β ≤ α + 1. Carries LinearOrder, WellFoundedLT, and (noncomputably) SuccOrder instances.

Equations

• FirstOrder.Language.HanfLadder.Index α = (α + 2).ToType

instance FirstOrder.Language.HanfLadder.instNonemptyIndex (α : Ordinal.{0}) : Nonempty (Index α)

@[instance_reducible]

noncomputable instance FirstOrder.Language.HanfLadder.instOrderBotIndex (α : Ordinal.{0}) : OrderBot (Index α)

Equations

• FirstOrder.Language.HanfLadder.instOrderBotIndex α = WellFoundedLT.toOrderBot (FirstOrder.Language.HanfLadder.Index α)

@[instance_reducible]

noncomputable instance FirstOrder.Language.HanfLadder.instOrderTopIndex (α : Ordinal.{0}) : OrderTop (Index α)

Equations

• FirstOrder.Language.HanfLadder.instOrderTopIndex α = { top := Ordinal.ToType.mk ⟨α + 1, ⋯⟩, le_top := ⋯ }

def FirstOrder.Language.HanfLadder.ladderLang (α : Ordinal.{0}) : Language

The ladder language: ℕ constants, Index α-indexed unary level predicates, one binary relation. Language.{0,0} for every α.

Equations

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

noncomputable def FirstOrder.Language.HanfLadder.ladderSentence (α : Ordinal.{0}) [Countable (Index α)] : (ladderLang α).Sentenceω

The ladder sentence (Marker, Exercise 5.3).

Equations

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

The semantic packaging

def FirstOrder.Language.HanfLadder.constVal (α : Ordinal.{0}) {M : Type} [(ladderLang α).Structure M] (n : ℕ) : M

The value of the n-th constant.

Equations

• FirstOrder.Language.HanfLadder.constVal α n = FirstOrder.Language.Structure.funMap (have this := n; this) Fin.elim0

def FirstOrder.Language.HanfLadder.Level (α : Ordinal.{0}) {M : Type} [(ladderLang α).Structure M] (i : Index α) (x : M) : Prop

The level predicate U_i.

Equations

• FirstOrder.Language.HanfLadder.Level α i x = FirstOrder.Language.Structure.RelMap (have this := i; this) fun (x_1 : Fin 1) => x

def FirstOrder.Language.HanfLadder.Edge (α : Ordinal.{0}) {M : Type} [(ladderLang α).Structure M] (x y : M) : Prop

The edge relation E.

Equations

• FirstOrder.Language.HanfLadder.Edge α x y = FirstOrder.Language.Structure.RelMap (have this := (); this) ![x, y]

structure FirstOrder.Language.HanfLadder.IsLadderModel (α : Ordinal.{0}) {M : Type} [(ladderLang α).Structure M] : Prop

The six clauses of a ladder model — the interface every semantic file works with.

• base (x : M) : Level α ⊥ x ↔ ∃ (n : ℕ), x = constVal α n
• top (x : M) : Level α ⊤ x
• nested {i j : Index α} : i < j → ∀ (x : M), Level α i x → Level α j x
• limit_covered {j : Index α} : Order.IsSuccLimit j → ∀ (x : M), Level α j x → ∃ i < j, Level α i x
• pred_down {i j : Index α} : i ⋖ j → ∀ (x y : M), Level α j x → Edge α y x → Level α i y
• ext (y z : M) : (∀ (x : M), Edge α x y ↔ Edge α x z) → y = z

theorem FirstOrder.Language.HanfLadder.realize_ladderSentence_iff {α : Ordinal.{0}} {M : Type} [(ladderLang α).Structure M] [Countable (Index α)] : (ladderSentence α).Realize M ↔ IsLadderModel α

The acceptance gate: realization of the ladder sentence is exactly the six clauses.