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 α)

@[implicit_reducible]

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

Equations

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

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

def FirstOrder.Language.HanfLadder.const {α : Ordinal.{0}} (n : ℕ) {γ : Type} : (ladderLang α).Term γ

The n-th constant, as a term over any variable type.

Equations

• FirstOrder.Language.HanfLadder.const n = FirstOrder.Language.func (have this := n; this) Fin.elim0

def FirstOrder.Language.HanfLadder.levelAtom {α : Ordinal.{0}} (i : Index α) {γ : Type} {n : ℕ} (t : (ladderLang α).Term (γ ⊕ Fin n)) : (ladderLang α).BoundedFormulaω γ n

The level atom U_i t.

Equations

• FirstOrder.Language.HanfLadder.levelAtom i t = FirstOrder.Language.BoundedFormulaω.rel (have this := i; this) fun (x : Fin 1) => t

def FirstOrder.Language.HanfLadder.eAtom {α : Ordinal.{0}} {γ : Type} {n : ℕ} (t u : (ladderLang α).Term (γ ⊕ Fin n)) : (ladderLang α).BoundedFormulaω γ n

The edge atom E t u.

Equations

• FirstOrder.Language.HanfLadder.eAtom t u = FirstOrder.Language.BoundedFormulaω.rel (have this := (); this) ![t, u]

@[reducible, inline]

abbrev FirstOrder.Language.HanfLadder.bvar {α : Ordinal.{0}} {n : ℕ} (i : Fin n) : (ladderLang α).Term (Empty ⊕ Fin n)

Variable i at arity n, over Empty free variables.

Equations

• FirstOrder.Language.HanfLadder.bvar i = FirstOrder.Language.var (Sum.inr i)

noncomputable def FirstOrder.Language.HanfLadder.baseInC (α : Ordinal.{0}) : (ladderLang α).Sentenceω

Base, ⊇: every constant is in the bottom level.

Equations

• FirstOrder.Language.HanfLadder.baseInC α = FirstOrder.Language.BoundedFormulaω.iInf fun (n : ℕ) => FirstOrder.Language.HanfLadder.levelAtom ⊥ (FirstOrder.Language.HanfLadder.const n)

noncomputable def FirstOrder.Language.HanfLadder.baseOutC (α : Ordinal.{0}) : (ladderLang α).Sentenceω

Base, ⊆: every bottom-level element is a constant.

Equations

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

noncomputable def FirstOrder.Language.HanfLadder.topC (α : Ordinal.{0}) : (ladderLang α).Sentenceω

Top: every element is in the top level.

Equations

• FirstOrder.Language.HanfLadder.topC α = (FirstOrder.Language.HanfLadder.levelAtom ⊤ (FirstOrder.Language.HanfLadder.bvar 0)).all

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

Nesting: U_i ⊆ U_j for i < j.

Equations

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

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

Limit covering: at an order-limit level j, U_j x → ⋁_{i<j} U_i x.

Equations

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

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

Predecessor descent: for adjacent i ⋖ j, U_j x → E y x → U_i y (x = bound variable 0, y = bound variable 1).

Equations

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

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

Extensionality, curried: (∀x, E x y → E x z) → (∀x, E x z → E x y) → y = z (y = bound variable 0, z = bound variable 1, x = bound variable 2).

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_const {α : Ordinal.{0}} {M : Type} [(ladderLang α).Structure M] {γ : Type} (v : γ → M) (n : ℕ) : Term.realize v (const n) = constVal α n

Constant terms realize to their values, at any valuation.

theorem FirstOrder.Language.HanfLadder.realize_levelAtom {α : Ordinal.{0}} {M : Type} [(ladderLang α).Structure M] {γ : Type} {n : ℕ} (i : Index α) (t : (ladderLang α).Term (γ ⊕ Fin n)) (v : γ → M) (xs : Fin n → M) : (levelAtom i t).Realize v xs ↔ Level α i (Term.realize (Sum.elim v xs) t)

theorem FirstOrder.Language.HanfLadder.realize_eAtom {α : Ordinal.{0}} {M : Type} [(ladderLang α).Structure M] {γ : Type} {n : ℕ} (t u : (ladderLang α).Term (γ ⊕ Fin n)) (v : γ → M) (xs : Fin n → M) : (eAtom t u).Realize v xs ↔ Edge α (Term.realize (Sum.elim v xs) t) (Term.realize (Sum.elim v xs) u)

theorem FirstOrder.Language.HanfLadder.realize_bvar1 {α : Ordinal.{0}} {M : Type} [(ladderLang α).Structure M] (x : M) : Term.realize (Sum.elim Empty.elim (Fin.snoc Fin.elim0 x)) (bvar 0) = x

The bound variable at arity 1 realizes to the snoc value.

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.