The ordinal interpretation of the ladder index order

The ladder syntax (LadderSyntax.lean) keeps all clause indexing internal to the order on Index α = (α + 2).ToType; this file is the deferred typein layer that the SEMANTIC files use to interpret indices as ordinals:

• idxVal : Index α → Ordinal (with idxOf inverse) — order-isomorphic onto Iio (α + 2);
• the endpoint values idxVal_bot = 0, idxVal_top = α + 1;
• the structural transfers: covBy_iff_idxVal (adjacency = ordinal successor) and isSuccLimit_iff_idxVal (order limits = ordinal limits);
• countable_index_of_lt_omega1 — the [Countable (Index α)] hypothesis of the sentence, discharged for every α < ω₁.

noncomputable def FirstOrder.Language.HanfLadder.idxVal {α : Ordinal.{0}} (i : Index α) : Ordinal.{0}

The ordinal value of a ladder index (the inverse of ToType.mk).

Equations

• FirstOrder.Language.HanfLadder.idxVal i = ↑(Ordinal.ToType.mk.symm i)

theorem FirstOrder.Language.HanfLadder.idxVal_lt {α : Ordinal.{0}} (i : Index α) : idxVal i < α + 2

noncomputable def FirstOrder.Language.HanfLadder.idxOf {α : Ordinal.{0}} (β : Ordinal.{0}) (h : β < α + 2) : Index α

The ladder index with a given ordinal value.

Equations

• FirstOrder.Language.HanfLadder.idxOf β h = Ordinal.ToType.mk ⟨β, ⋯⟩

@[simp]

theorem FirstOrder.Language.HanfLadder.idxVal_idxOf {α : Ordinal.{0}} (β : Ordinal.{0}) (h : β < α + 2) : idxVal (idxOf β h) = β

@[simp]

theorem FirstOrder.Language.HanfLadder.idxOf_idxVal {α : Ordinal.{0}} (i : Index α) : idxOf (idxVal i) ⋯ = i

theorem FirstOrder.Language.HanfLadder.idxVal_lt_idxVal_iff {α : Ordinal.{0}} {i j : Index α} : idxVal i < idxVal j ↔ i < j

theorem FirstOrder.Language.HanfLadder.idxVal_le_idxVal_iff {α : Ordinal.{0}} {i j : Index α} : idxVal i ≤ idxVal j ↔ i ≤ j

theorem FirstOrder.Language.HanfLadder.idxVal_injective {α : Ordinal.{0}} : Function.Injective idxVal

@[simp]

theorem FirstOrder.Language.HanfLadder.idxVal_bot {α : Ordinal.{0}} : idxVal ⊥ = 0

@[simp]

theorem FirstOrder.Language.HanfLadder.idxVal_top {α : Ordinal.{0}} : idxVal ⊤ = α + 1

theorem FirstOrder.Language.HanfLadder.covBy_iff_idxVal {α : Ordinal.{0}} {i j : Index α} : i ⋖ j ↔ idxVal j = idxVal i + 1

Adjacency in the index order is ordinal successor on values.

theorem FirstOrder.Language.HanfLadder.isSuccLimit_iff_idxVal {α : Ordinal.{0}} {j : Index α} : Order.IsSuccLimit j ↔ Order.IsSuccLimit (idxVal j)

Order limits of the index order are ordinal limits of values.

theorem FirstOrder.Language.HanfLadder.countable_index_of_lt_omega1 {α : Ordinal.{0}} (hα : α < Ordinal.omega 1) : Countable (Index α)

Below ω₁ the index order is countable — the formation hypothesis of the ladder sentence.