The stage of a constructible set

Constructibility was defined as "some ordinal stage contains it", and the witness was deliberately kept in the statement so that later theory could take it back out. Now it takes it out, and sharpens it: not some stage but the earliest one. That function is what every later construction uses to place a finite collection of constructible sets at a common stage, since bounding the earliest stages bounds every stage that would do.

Two things have to be shown. That a least stage exists, which is a descent: start from any stage that works and ask whether a smaller one also works; if so recurse, and membership is well founded so the recursion stops. And that it is unique, which is trichotomy: two least stages cannot be strictly ordered either way, so they are equal.

Neither argument looks at what the property says. So the chapter proves them for an arbitrary property of ordinals and reads the stage function off as the instance, which costs nothing here and pays later: a canonical choice of ordinal is a thing several constructions want, and each one that gets it this way is one that does not need a well-ordering of L to get it.

Both are classical, for reasons already seen. The descent asks, at each step, a question about an arbitrary set, and uniqueness is comparison. So the least ordinal joins the classical cone, and the chapter is the third and last place the excluded middle enters the L-side machinery.

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

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

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

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 )
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 )
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ᵥ

Being the earliest stage

An ordinal is least for a property when no smaller ordinal has that property. Packaging that with the ordinal and the property gives the data a later chapter wants; and the package is a proposition, which is what lets it be extracted from a truncated witness, as constructibility's is.

Uniqueness is where the property's being an hProp earns its keep: 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.

module _ (P : S → Ω) where

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

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

  isPropLeastOrd : isProp LeastOrd
  isPropLeastOrd (α , ordα , pα , leastα) (α' , ordα' , pα' , leastα') =
    Σ≡Prop propRest α≡α'
    where
    decide : (⟨ α ∈ˢ α' ⟩ ⊎ ((α ≡ α') ⊎ ⟨ α' ∈ˢ α ⟩)) → α ≡ α'
    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α')
    propRest : (β : S) → isProp (IsOrd β × ⟨ P β ⟩ × isLeastOrd β)
    propRest β = isProp× (isPropIsOrd β)
      (isProp× (snd (P β))
        (isPropΠ λ _ → isPropΠ λ _ → isPropΠ λ _ → isPropΠ λ _ → Empty.isProp⊥))

The descent

Given any ordinal with the property, walk down. Ask whether a strictly smaller ordinal also has it; if one does, recurse into it, and membership being well founded the walk terminates; if none does, the current ordinal is least, and the refutation of the question is exactly the minimality proof.

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.

  leastOrdBelow : (α : S) → IsOrd α → ⟨ P α ⟩ → LeastOrd
  leastOrdBelow = ∈-induction step
    where
    step : (α : S) → (∀ β → ⟨ β ∈ˢ α ⟩ → IsOrd β → ⟨ P β ⟩ → LeastOrd)
         → IsOrd α → ⟨ P α ⟩ → LeastOrd
    step α IH ordα pα = decide (lem Smaller)
      where
      Smaller : hProp (ℓ-suc ℓ)
      Smaller = ∃[ β ∶ S ] ((β ∈ˢ α) ⊓ ((IsOrd β , isPropIsOrd β) ⊓ P β))
      decide : (⟨ Smaller ⟩ ⊎ (⟨ Smaller ⟩ → Empty.⊥)) → LeastOrd
      decide (inl ∃β) = PT.rec isPropLeastOrd
        (λ { (β , (β∈α , (ordβ , pβ))) → IH β β∈α ordβ pβ }) ∃β
      decide (inr ¬∃β) = α , ordα , pα , leastProof
        where
        leastProof : isLeastOrd α
        leastProof γ ordγ pγ γ∈α = ¬∃β ∣ γ , (γ∈α , (ordγ , pγ)) ∣₁

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

The stage function

Constructibility carries its witness truncated, and the descent's result is a proposition, so the truncation lifts. The stage is then the ordinal component, with its three properties projected out.

The function is sealed. It unfolds to a well-founded recursion whose steps mention the tower, and every later type mentioning a stage would otherwise drag that unfolding into conversion; the three projections open the seal exactly once each, and no consumer needs it open again.

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

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) ⟩
  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 picks the least ordinal satisfying any property of ordinals, from a truncated witness that one exists. stage is its first instance, naming the earliest stage containing a constructible set, with

stage-ord, stage-mem and stage-earliest its three properties. Existence is a well-founded descent and uniqueness is trichotomy, so the chapter is classical; and the function is sealed, so the descent never reaches a later conversion problem. Reflection is the first consumer, and it uses both: it places a formula's parameters at a common stage by bounding their stages, and it picks a witness for an existential by taking the least stage that has one.