Numerals in a successor-closed ordinal stage

Finite ordinals supply the numerals used in formula codes. This chapter shows that every numeral belongs to a stage indexed by an ordinal that contains zero and is closed under successors. The argument first treats any monotone stage family containing each ordinal at its successor stage, then applies it to the constructible hierarchy.

The chapter fixes a universe level ℓ and takes excluded middle at level ℓ-suc ℓ as an explicit parameter lem. The elementary induction putting numerals inside an ordinal will not use it; the assumption is carried here because one ingredient of the constructible specialization, the theorem that an ordinal appears at the stage indexed by its successor, comes from the classical ordinal-stage development.

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Coding.NumeralBound {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

Two presentations of a numeral must be kept apart. The ambient numeral # k is the finite von Neumann ordinal in V ℓ; the model numeral numeralL k is an element of L whose underlying set is # k. The first part proves the bound for the ambient ordinal. Only after that does the projection equation numeralL-fst transfer the result to the model presentation.

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( IsOrd; Lset; Lset-mono )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
open import L.Ordinal {ℓ} using ( numeral-ord )

The ambient numerals live in the cumulative hierarchy itself: ∅ is its empty set, # k is the finite von Neumann ordinal with k members, and sucV is the successor step a ↦ a ∪ {a}. Note that # (suc k) is definitionally sucV (# k), so closing λ under sucV automatically covers every numeral after zero. The truth values here are propositions at level ℓ-suc ℓ, packaged directly in hProp, so each membership claim is a proposition.

open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; module InfinitySet )
open InfinitySet using ( #_; sucV )

All three memberships in the argument have different roles: # k ∈ λ places a finite ordinal below the index; # k ∈ T (sucV (# k)) places it in its canonical successor stage; and # k ∈ T λ is the desired bound. Writing each as a proposition makes the induction and the later transport proof-irrelevant, but the implication between them still comes from the stated closure, ordinal-stage, and monotonicity hypotheses.

open hPropStructure 𝒮ᵥ

A bound for monotone stage families

Let λ contain zero and be closed under successors. Induction puts every numeral # k in λ. To place that same numeral in T λ, use numeral-ord k with the successor-stage hypothesis to obtain # k ∈ T (sucV (# k)); successor closure gives the index relation sucV (# k) ∈ λ, and monotonicity then yields # k ∈ T λ.

The section works over the fixed carrier S with membership ⟨_∈ˢ_⟩, an arbitrary map T on it, and two hypotheses about T. The first, T-mono, converts a membership of stage indices β ∈ α together with x ∈ T β into x ∈ T α. The second, T-ord, is the anchor: an ordinal δ belongs to T (sucV δ), the stage indexed by its own successor.

module BoundOver
  (T : S → S)
  (T-mono : {α β : S} → ⟨ β ∈ˢ α ⟩ → {x : S} → ⟨ x ∈ˢ T β ⟩ → ⟨ x ∈ˢ T α ⟩)
  (T-ord : (δ : S) → IsOrd δ → ⟨ δ ∈ˢ T (sucV δ) ⟩)
  (lam : S) (ordλ : IsOrd lam)

The remaining parameters describe the index λ: it is a set, certified to be an ordinal, containing ∅, and closed under sucV. The certification ordλ records that λ itself is a legitimate ordinal stage index; the two closure facts are the only ones the induction will consume.

  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where

Every ambient numeral lands in λ, and the proof uses only the two closure facts just assumed. This is the purely inductive half of the argument: no excluded middle, no property of T, and not even the ordinal certificate of λ enter it.

Induction on k. The base case is exactly the hypothesis ∅∈λ, since # 0 is ∅. For the step, # (suc k) is definitionally sucV (# k), so succλ applied to the induction hypothesis # k ∈ λ yields # (suc k) ∈ λ. The small cases show the shape: 0 = ∅ ∈ λ, then {∅} = sucV ∅ ∈ λ, then the numeral 2 = sucV (sucV ∅) ∈ λ, each step consuming one use of successor closure.

  #∈λ : (k : ℕ) → ⟨ (# k) ∈ˢ lam ⟩
  #∈λ zero    = ∅∈λ
  #∈λ (suc k) = succλ (# k) (#∈λ k)

Membership in λ is an index-level statement; membership in the stage T λ is a different statement, and it needs the two properties of T rather than only the closure of λ. The route runs through the successor stage of the numeral itself.

Two steps compose. First, T-ord at δ = # k, together with numeral-ord k certifying the numeral is an ordinal, places # k in T (sucV (# k)). Second, T-mono moves the membership from the index sucV (# k) up to the index λ: the needed premise # (suc k) ∈ λ is exactly #∈λ (suc k), and #∈λ (suc k) unfolds to sucV (# k) ∈ λ, precisely the membership of indices T-mono asks for. So the element # k ends in T λ, with the ordinal certificate doing real work in the first step.

  #∈Tλ : (k : ℕ) → ⟨ (# k) ∈ˢ T lam ⟩
  #∈Tλ k = T-mono {α = lam} {β = sucV (# k)} (#∈λ (suc k))
    {x = # k} (T-ord (# k) (numeral-ord k))

Numerals in the constructible hierarchy

Constructible stages are monotone, and each ordinal belongs to the stage indexed by its successor. The general bound therefore applies to L. We also express this membership using the numerals already regarded as elements of the model.

Instantiating the abstraction only requires naming the witnesses. The family T becomes Lset, Lset-mono supplies monotonicity along membership of ordinal indices, and ord∈Lset-suc supplies the anchor that each ordinal sits in Lset (sucV α). The theorem ord∈Lset-suc carries the classical assumption required for this specialization; the induction on numerals itself remains the elementary closure argument already given. The hypotheses about λ are passed through unchanged, so everything proved inside BoundOver about T λ becomes available about Lset lam.

module Bound (lam : S) (ordλ : IsOrd lam)
             (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
             (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where

  open BoundOver Lset Lset-mono ord∈Lset-suc lam ordλ succλ ∅∈λ public

Inside the model, a numeral is not the ambient ordinal itself but a pair numeralL k whose first component denotes it. The bound transfers to that presentation by one transport, not by repeating the induction.

The equation numeralL-fst k is a path fst (numeralL k) ≡ # k in the host theory. Transporting the membership family along this path turns the proof for # k into a proof for fst (numeralL k). Using sym orients the path from the established membership of # k to the desired membership of fst (numeralL k), so #∈Tλ k becomes the required statement about the model numeral.

  num∈λ : (k : ℕ) → ⟨ fst (numeralL k) ∈ˢ Lset lam ⟩
  num∈λ k = subst (λ w → ⟨ w ∈ˢ Lset lam ⟩) (sym (numeralL-fst k)) (#∈Tλ k)