---
title: "Numerals in a successor-closed ordinal stage"
module: L.Coding.NumeralBound
lang: en
site: "Bedrock"
description: "Numerals in a successor-closed ordinal stage"
stage: "Internal coding: tables and uniform satisfaction"
reading_order: 56
canonical: https://bedrock.institute/en/L.Coding.NumeralBound.html
html: L.Coding.NumeralBound.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/NumeralBound.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, L.Constructible, L.Axioms.Numerals, L.Ordinal, L.Ordinal.Stages]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Coding.NumeralBound.md, https://bedrock.institute/ja/L.Coding.NumeralBound.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

```agda
{-# 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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
  (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.

```agda
  #∈λ : (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.

```agda
  #∈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`.

```agda
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.

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