The index of the least constructible stage

Every constructible set x belongs to Lset α for at least one ordinal α. This chapter turns that mere existence into a canonical bound: the least ordinal whose stage contains x. The construction first solves a more general problem. For any hProp-valued property P of ordinals, a well-founded descent finds its least witness, while ordinal trichotomy proves that the resulting witness is unique.

The descent begins at any ordinal satisfying P. At α it asks whether some smaller ordinal β ∈ α also satisfies P. A positive answer invokes the induction result at β; a negative answer proves α minimal. Membership induction makes this definition well founded. Both the assertion of a smaller witness and the initial witness are propositionally truncated, but LeastOrd P is itself a proposition, so each truncation may be eliminated into that complete package.

Specializing P σ to x ∈ Lset σ gives stage x hx. Its accompanying theorems state that this index is an ordinal, that its stage contains x, and that no smaller ordinal stage contains x. The proof uses excluded middle only to decide the existence of a smaller witness and to compare two candidate ordinals.

Work at a fixed universe level ℓ and assume excluded middle at level ℓ-suc ℓ. The assumption will be used in two mathematically distinct ways: ord-tri compares ordinal candidates, while the descent decides the hProp asserting that a smaller candidate exists.

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

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

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

Membership supplies both the strict order on ordinals and its well-founded induction principle. Constructibility supplies the predicate IsOrd, the stage family Lset and the assertion isL x that x occurs in some ordinal-indexed stage. Thus the same membership relation controls descent among candidate indices and, after specialization, membership of x in a stage.

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction )
open import L.Constructible {ℓ} using ( IsOrd; isPropIsOrd; Lset; isL )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )

open import Cubical.Data.Sum using ( _⊎_; inl; inr )

The assertion that a smaller witness exists is represented by a propositionally truncated existential. It records existence without exposing a chosen β. The eliminator PT.rec can use such evidence only when the target is a proposition; the uniqueness proof below supplies exactly this fact for LeastOrd P. Products and dependent function spaces preserve propositionhood, which will also show that the evidence attached to a fixed ordinal index is unique.

import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
open import Cubical.Functions.Logic using ( ∃[∶]-syntax )
open import Cubical.Data.Sigma using ( Σ≡Prop )

A property P is a map into Ω, the type of hProps. Hence ⟨ P α ⟩ is its underlying proposition at α, and snd (P α) proves that any two of its witnesses agree. This propositionhood is needed when equality of ordinal indices is lifted to equality of complete least-witness packages.

open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ )

open hPropStructure 𝒮ᵥ

The least ordinal satisfying a property

For a property P of ordinals, LeastOrd P packages an ordinal α satisfying P together with the proof that no smaller ordinal satisfies it. This definition concerns the ordinal index itself; only the later specialization P σ = (x ∈ Lset σ) turns such an index into the index of a constructible stage.

Uniqueness uses the fact that the property takes values in an hProp: the two candidates are compared by trichotomy, each strict direction is refuted by the other's minimality, and the remaining components are propositions, so the equality of the ordinals is the equality of the packages.

Leastness is stated as a refutation: isLeastOrd α is the assertion, for every set γ, that γ cannot be an ordinal satisfying P with γ ∈ α. Minimality by contradiction is the right shape here because the strict order on ordinals is read off membership; there is no smaller-ordinal value to return, only an impossible situation to derive. The full package LeastOrd then bundles an ordinal, its ordinalhood, a proof of P at it, and this minimality clause.

module _ (P : S → hProp (ℓ-suc ℓ)) where

  isLeastOrd : S → Type (ℓ-suc ℓ)
  isLeastOrd α = (γ : S) → IsOrd γ → ⟨ P γ ⟩ → ⟨ γ ∈ˢ α ⟩ → Empty.⊥

  LeastOrd : Type (ℓ-suc ℓ)
  LeastOrd = Σ[ α ∈ S ] (IsOrd α × ⟨ P α ⟩ × isLeastOrd α)

To prove two such packages equal, compare their ordinal indices first. Trichotomy delivers one of three cases: α ∈ α′, α = α′, or α′ ∈ α. The plan is to eliminate both strict cases by contradiction and keep the equality case; decide is the function turning that trichotomy result into a path α ≡ α′. Crucially, this argument shows the indices equal; the packages are dependent pairs over the index, so an equality of packages is not yet obtained from an equality of indices alone.

  isPropLeastOrd : isProp LeastOrd
  isPropLeastOrd (α , ordα , pα , leastα) (α' , ordα' , pα' , leastα') =
    Σ≡Prop propRest α≡α'
    where
    decide : (⟨ α ∈ˢ α' ⟩ ⊎ ((α ≡ α') ⊎ ⟨ α' ∈ˢ α ⟩)) → α ≡ α'

Each strict case contradicts minimality, but minimality of the other candidate. If α were a member of α′, then α is an ordinal satisfying P that lies strictly below α′, and leastα' refutes exactly that; the case α′ ∈ α is symmetric, using leastα. The middle case is the path itself. Feeding ord-tri's verdict into decide thus yields the path α≡α', and note that no assumption about P beyond its values being propositions was used so far.

    decide (inl α∈α')       = Empty.rec (leastα' α ordα pα α∈α')
    decide (inr (inl e))    = e
    decide (inr (inr α'∈α)) = Empty.rec (leastα α' ordα' pα' α'∈α)
    α≡α' : α ≡ α'
    α≡α' = decide (ord-tri α ordα α' ordα')

It remains to lift the path of indices to a path of packages, and this uses propositionhood of the dependent remainder. The component that varies with the index is IsOrd β × ⟨ P β ⟩ × isLeastOrd β; IsOrd β is a proposition by the constructible chapter, ⟨ P β ⟩ is a proposition because P is hProp-valued, and isLeastOrd β is a function type into the empty type, hence a proposition by isPropΠ iterated. So propRest β certifies propositionhood of the whole remainder, and Σ≡Prop turns the base path into the required equality of packages: once the index agrees, the dependent remainder cannot disagree.

    propRest : (β : S) → isProp (IsOrd β × ⟨ P β ⟩ × isLeastOrd β)
    propRest β = isProp× (isPropIsOrd β)
      (isProp× (snd (P β))
        (isPropΠ λ _ → isPropΠ λ _ → isPropΠ λ _ → isPropΠ λ _ → Empty.isProp⊥))

Descent to the least ordinal

Starting from any ordinal satisfying P, leastOrdBelow asks whether a strictly smaller ordinal also satisfies P and recurses when one does. Membership induction defines the result from the results at strictly smaller ordinals, yielding the least ordinal satisfying P, before the construction is specialized to constructible stages.

The result being a proposition, the starting ordinal may be given truncated, and that is the form the callers have: they know a suitable ordinal exists without having chosen one.

The descent is organized as well-founded induction on membership, the principle ∈-induction from the hierarchy chapter. Its step receives an ordinal α, its ordinalhood, a proof of P at α, and an induction hypothesis valid for every strictly smaller member β: provided β is again an ordinal satisfying P, the globally least P-witness obtained by starting the induction at β is already available. The step's only job is to decide, at α, whether the descent must continue or has arrived.

  leastOrdBelow : (α : S) → IsOrd α → ⟨ P α ⟩ → LeastOrd
  leastOrdBelow = ∈-induction step
    where
    step : (α : S) → (∀ β → ⟨ β ∈ˢ α ⟩ → IsOrd β → ⟨ P β ⟩ → LeastOrd)
         → IsOrd α → ⟨ P α ⟩ → LeastOrd

The question to decide is Smaller: merely whether there exists a β with β ∈ α, ordinal, and satisfying P, all packaged with conjunctions into a single hProp. Two features matter. First, the existential is truncated: Smaller carries no chosen β, only the assertion that one exists. Second, excluded middle at level ℓ-suc ℓ, applied via lem, decides this question outright, delivering either an inhabitant of the truncation or a refutation. This is precisely where the classical assumption enters the descent.

    step α IH ordα pα = decide (lem Smaller)
      where
      Smaller : hProp (ℓ-suc ℓ)
      Smaller = ∃[ β ∶ S ] ((β ∈ˢ α) ⊓ ((IsOrd β , isPropIsOrd β) ⊓ P β))
      decide : (⟨ Smaller ⟩ ⊎ (⟨ Smaller ⟩ → Empty.⊥)) → LeastOrd

The two branches of the decision build the answer directly. In the positive branch, the truncated witness cannot be taken apart into data, but PT.rec may eliminate it into any proposition, and LeastOrd is one: so the witness is converted, without being chosen, into the globally least package supplied by the induction hypothesis at β. In the negative branch there is no smaller witness at all, so α itself is least. Recursion happens only through ∈-induction's controlled induction hypothesis.

      decide (inl ∃β) = PT.rec isPropLeastOrd
        (λ { (β , (β∈α , (ordβ , pβ))) → IH β β∈α ordβ pβ }) ∃β
      decide (inr ¬∃β) = α , ordα , pα , leastProof
        where
        leastProof : isLeastOrd α

The negative branch's minimality clause is where the refutation earns its keep: given any γ below α that is an ordinal satisfying P, the witness (γ , γ∈α , ordγ , pγ) is packaged into the very truncation Smaller that was denied, and applying ¬∃β to it yields the required contradiction. Finally, leastOrd handles the form callers actually have: an ordinal satisfying P merely exists. Again the elimination into LeastOrd is licensed by its propositionhood, proved in the previous section, so a truncated existence is refined into the canonical least index without eliminating the truncation into an arbitrary data type.

        leastProof γ ordγ pγ γ∈α = ¬∃β ∣ γ , (γ∈α , (ordγ , pγ)) ∣₁

  leastOrd : ∥ (Σ[ α ∈ S ] (IsOrd α × ⟨ P α ⟩)) ∥₁ → LeastOrd
  leastOrd = PT.rec isPropLeastOrd
    (λ { (α , (ordα , pα)) → leastOrdBelow α ordα pα })

The stage-index function

For P σ = (x ∈ Lset σ), the descent returns the least ordinal index α whose stage Lset α contains x. The function stage selects α, stage-ord proves that it is an ordinal, and stage-mem and stage-earliest relate that index to its stage.

The index is exposed through three stable facts rather than its recursive construction: it is an ordinal, its stage contains x, and it is minimal among ordinal indices with that property. Declaring stage opaque preserves this abstraction boundary.

A constructibility certificate ⟨ isL x ⟩ is exactly the input form leastOrd expects: by the class's definition in the constructible chapter, an element of isL x is merely a pair of an ordinal σ, its ordinalhood, and a membership x ∈ˢ Lset σ. So the property λ σ → x ∈ˢ Lset σ satisfies the hypotheses of the descent, and theEarliest applies leastOrd to this property. Thus constructibility supplies exactly the truncated existence premise needed to obtain a least stage index.

theEarliest : (x : S) → ⟨ isL x ⟩ → LeastOrd (λ σ → x ∈ˢ Lset σ)
theEarliest x = leastOrd (λ σ → x ∈ˢ Lset σ)

opaque
  stage : (x : S) → ⟨ isL x ⟩ → S
  stage x p = theEarliest x p .fst

The package theEarliest x p contains the least index together with its three proofs. The function stage projects the index and keeps its recursive construction opaque, so later arguments use its ordinalhood, membership and minimality. It is an ordinal-valued function of a constructible set and its witness; it is neither a universe level nor the rank function.

opaque
  unfolding stage
  stage-ord : (x : S) (p : ⟨ isL x ⟩) → IsOrd (stage x p)
  stage-ord x p = theEarliest x p .snd .fst

  stage-mem : (x : S) (p : ⟨ isL x ⟩) → ⟨ x ∈ˢ Lset (stage x p) ⟩

The three theorems are the interface, each a projection of the package. stage-ord states that the chosen index is an ordinal, so it can later be compared with other indices. stage-mem places x in the stage Lset (stage x p), the membership fact established by the descent. stage-earliest recovers the minimality clause itself: no smaller ordinal σ has x ∈ˢ Lset σ. Together they say that stage x p is precisely the least index promised at the head of the chapter, reached by projection rather than by reopening the recursion.

  stage-mem x p = theEarliest x p .snd .snd .fst

  stage-earliest : (x : S) (p : ⟨ isL x ⟩)
                 → isLeastOrd (λ σ → x ∈ˢ Lset σ) (stage x p)
  stage-earliest x p = theEarliest x p .snd .snd .snd

Recap

leastOrd extracts the least ordinal satisfying a property from a truncated existence witness. Its specialization stage x hx returns the ordinal index α of the least Lset α containing x; stage-ord, stage-mem, and stage-earliest state exactly those facts. Later arguments can therefore compare or bound these ordinal indices and then use the corresponding constructible stages.