The first stage meeting a set

This chapter provides two ingredients of the internal choice construction. The first is a lemma about least stages. When a property of ordinals holds for the first time, it holds at a least stage; whether that stage is a successor is not automatic, for the property may hold first at the zero ordinal. The chapter proves the conditional form that the argument needs: if, besides the least stage, a carve merely exists, an ordinal below it at whose successor the property already holds, then the least stage is a successor with a unique predecessor. The second ingredient is a bounding ordinal: for a constructible set, one ordinal whose stage contains the set, its members, the members of its members, and the limit level of the tower.

The material serves a comparison that proceeds by two keys. Two sets that first appear at different stages are compared by their birth ordinals and by nothing else; only sets that first appear at the same stage are compared by their names within that stage. The first ingredient makes each birth ordinal a definite object rather than a mere existence, and the second guarantees that the material of a whole family of candidates lives inside one stage, so that the name comparison has a common arena.

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

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

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

The chapter runs under one hypothesis, an excluded-middle instance at the successor of the model's level, and every statement below is made inside that setting.

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-irrefl )
open import V.Model {ℓ} using ( ∈sucV-elim; self∈sucV )

The question of the chapter is one about first appearances. A constructible set enters the tower of stages at some point; the ambient hierarchy, in which the tower lives, has irreflexive membership, so no ordinal contains itself, and its successors are understood: an ordinal sits inside its own successor, and a member of a successor is a member of the ordinal or the ordinal itself.

open import L.Constructible {ℓ}
  using ( IsOrd; isPropIsOrd; isL; Lset; Lset-layer; Lset-out
        ; Lset-mono; layer-trans )

The constructible side answers with its tower Lset, indexed by ordinals, which are sets of the hierarchy, never by universe levels of the host. Ordinality IsOrd is itself a proposition; the tower has a layer relation, an outward decomposition, and monotonicity; and transitivity moves members across layers.

open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; bound2; ω-ord )
open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ )
open import L.Stage {ℓ} lem
  using ( isLeastOrd; stage; stage-ord; stage-mem )
open import L.Axioms.Basic {ℓ} using ( Lset-suc )

The argument turns on comparisons and on stages. Comparing an ordinal below a stage with the stage itself is what decides whether the stage overshoots a successor, and members of ordinals and successors of ordinals are again ordinals. Each constructible set carries its earliest ordinal, delivered with ordinality and membership, and minimality stated refutationally. Two ordinals have a common bound. And the successor identity says the next stage is exactly the definable subsets of the previous one, which is the step by which anything enters the tower at all.

import Cubical.Data.Sum as Sum
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )

The argument is written in three propositional moves: a split into cases, a refutation ending in the empty type, and an existence known only to be existence.

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )

A predecessor pairs an ordinal with propositional evidence. Such pairs are determined by their first component, and the cumulative hierarchy itself is a set, so equality of predecessors reduces to equality of the underlying ordinals.

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( sucV; ω )

The hierarchy's infinity construction supplies both the von Neumann successor sucV and the limit level ω used in the bound.

open hPropStructure 𝒮ᵥ

Structure membership ∈ˢ is the relation in which ordinality, stages and minimality are all stated.

The predecessor of a least stage

The question is whether the least stage at which something appears is a successor, and which stage it succeeds. A least stage taken alone need not be one, for the property may begin at zero; what the construction produces, under the additional hypothesis of a carve below, is the unique predecessor.

A successor determines what it succeeds, at least among ordinals. Compare a candidate predecessor with another: each belongs to the successor of the other, so each is a member of the other or equal to it, and two ordinals cannot be members of each other, since transitivity would then make one a member of itself. So being the predecessor of a given ordinal is a proposition, which is what lets a merely-existing predecessor be read as a definite one.

That a least stage has a predecessor at all takes two inputs, and it is worth seeing them separately. The first is the least stage itself: an ordinal σ at which the property holds, with minimality stated refutationally, that no smaller ordinal has it. The second is the mere existence of a carve at σ: some ordinal δ below σ at whose successor the property already holds. Given a carve, minimality rules out the successor staying strictly below, and the no-overshoot comparison leaves one case: the successor of the carved ordinal is exactly σ. So the least stage is a successor, and the carved ordinal is its predecessor. Without the carve nothing follows: the property may hold first at the zero ordinal, below which no ordinal exists at all.

IsPredOf : S → S → Type (ℓ-suc ℓ)
IsPredOf σ δ = IsOrd δ × (sucV δ ≡ σ)

A candidate predecessor δ of an ordinal σ is an ordinal whose von Neumann successor is σ itself. Both halves matter: ordinality is what the comparison needs, and the equation is what pins δ to σ.

private
  cycle₂ : (a b : S) → IsOrd a → ⟨ a ∈ˢ b ⟩ → ⟨ b ∈ˢ a ⟩ → Empty.⊥
  cycle₂ a b orda a∈b b∈a = ∈-irrefl a (orda .fst a∈b b∈a)

No ordinal can be a member of one of its own members: transitivity would carry the membership around the two-step cycle back to a itself, contradicting irreflexivity. This two-step impossibility forbids two ordinals from containing each other.

  mem-branch : (δ δ' : S) → IsOrd δ → ⟨ δ' ∈ˢ sucV δ ⟩ → ⟨ δ ∈ˢ δ' ⟩ → δ ≡ δ'
  mem-branch δ δ' ordδ δ'∈sδ δ∈δ' =
    ∈sucV-elim {A = δ} {x = δ'} (setIsSet δ δ') δ'∈sδ
      (λ δ'∈δ → Empty.rec (cycle₂ δ δ' ordδ δ∈δ' δ'∈δ))
      (λ δ'≡δ → sym δ'≡δ)

The membership branch reads: δ' is a member of the successor of δ, and δ is a member of δ'; the conclusion must be δ ≡ δ'. If δ' were a member of δ itself, the two-step cycle would close; so δ' is δ itself, and the elimination returns exactly that.

ord-suc-inj : (δ δ' : S) → IsOrd δ → sucV δ ≡ sucV δ' → δ ≡ δ'
ord-suc-inj δ δ' ordδ e =
  ∈sucV-elim {A = δ'} {x = δ} (setIsSet δ δ') δ∈sδ'
    (mem-branch δ δ' ordδ δ'∈sδ)
    (λ δ≡δ' → δ≡δ')

The successor operation is injective on ordinals. From the equation of successors, δ is a member of sucV δ'; the elimination offers two readings. Either δ is a member of δ', in which case the membership branch closes the cycle and gives the equality, or δ already is δ'. A successor determines what it succeeds.

  where
  δ∈sδ' : ⟨ δ ∈ˢ sucV δ' ⟩
  δ∈sδ' = subst (λ w → ⟨ δ ∈ˢ w ⟩) e (self∈sucV δ)
  δ'∈sδ : ⟨ δ' ∈ˢ sucV δ ⟩
  δ'∈sδ = subst (λ w → ⟨ δ' ∈ˢ w ⟩) (sym e) (self∈sucV δ')

The two memberships feeding the elimination come from the standing fact that an ordinal sits inside its own successor, transported along the equation and its reverse.

isPropPredOf : (σ : S) → isProp (Σ[ δ ∈ S ] IsPredOf σ δ)
isPropPredOf σ (δ , (ordδ , e)) (δ' , (ordδ' , e')) =
  Σ≡Prop (λ d → isProp× (isPropIsOrd d) (setIsSet (sucV d) σ))
    (ord-suc-inj δ δ' ordδ (e ∙ sym e'))

Any two predecessors of one ordinal are therefore equal. The first components agree by injectivity, and the remaining data are propositions, so the whole type of predecessors is a proposition. This is what makes a merely-existing predecessor usable as a definite one: unwrapping a truncation into a proposition-valued target is always legitimate.

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

The least-stage argument is now run once for every property of ordinals at once: the property is a parameter, and nothing below ever reads into it.

  Carved : S → Type (ℓ-suc ℓ)
  Carved σ = Σ[ δ ∈ S ] (⟨ δ ∈ˢ σ ⟩ × ⟨ P (sucV δ) ⟩)

A carve at σ is the datum the argument runs on: an ordinal δ strictly below σ whose successor already carries the property. If a carve merely exists, the least stage cannot be far above δ, for the property already holds at sucV δ.

  private
    below-case : (σ δ : S) → isLeastOrd P σ → IsOrd δ → ⟨ P (sucV δ) ⟩
               → ⟨ sucV δ ∈ˢ σ ⟩ → sucV δ ≡ σ
    below-case σ δ least ordδ m s∈σ =
      Empty.rec (least (sucV δ) (suc-ord ordδ) m s∈σ)

The below branch handles the case in which the successor stays strictly below the least stage. Minimality is stated refutationally, and the hypotheses of this branch are exactly its premises, so least yields a contradiction first; Empty.rec then eliminates that contradiction to the path the branch owes, sucV δ ≡ σ.

    same-case : (σ δ : S) → sucV δ ≡ σ → sucV δ ≡ σ
    same-case σ δ e = e

The equal case needs no work at all: the identification of the successor with the least stage is what the case was handed.

    atCarve : (σ : S) → IsOrd σ → isLeastOrd P σ
            → Carved σ → Σ[ δ ∈ S ] IsPredOf σ δ
    atCarve σ ordσ least (δ , (δ∈σ , m)) = δ , (ordδ , suc≡σ)

atCarve turns a carve into a definite predecessor. The witness δ is kept, its ordinality is recovered from belonging to the ordinal σ, and the equation pinning sucV δ to σ is the content of the case analysis.

      where
      ordδ : IsOrd δ
      ordδ = mem-ord {A = σ} ordσ δ δ∈σ

Ordinality of δ is inherited from the ordinal σ, members of ordinals being ordinals.

      suc≡σ : sucV δ ≡ σ
      suc≡σ = Sum.rec (below-case σ δ least ordδ m) (same-case σ δ)
        (suc∈or≡ δ σ ordδ ordσ δ∈σ)

Given δ ∈ σ, suc∈or≡ leaves exactly two possibilities for its successor: it remains strictly below σ, or it equals σ. Minimality refutes the first, so the second gives the required equation.

  predOf : (σ : S) → IsOrd σ → isLeastOrd P σ → ∥ Carved σ ∥₁
         → Σ[ δ ∈ S ] IsPredOf σ δ
  predOf σ ordσ least = PT.rec (isPropPredOf σ) (atCarve σ ordσ least)

predOf consumes a carve known only to exist and returns the predecessor. The truncated input is eliminated into the proposition that the predecessor type is, so no choice among hypothetical carves is ever made; whichever carve the truncation hands over, the answer is the same definite predecessor.

  carveAt : (σ z : S) → ⟨ z ∈ˢ Lset σ ⟩
          → ((δ : S) → ⟨ z ∈ˢ Lset (sucV δ) ⟩ → ⟨ P (sucV δ) ⟩)
          → ∥ Carved σ ∥₁

carveAt produces a carve from a member z of the least stage, together with the observation that whenever z appears at a successor stage, the property already holds there. That observation is exactly the shape of the descent into the tower: appearing at a stage is appearing inside a definable powerset of an earlier stage, and every definable powerset is a successor stage by the successor identity.

  carveAt σ z z∈Lσ k = PT.map
    (λ { (δ , (δ∈σ , z∈𝒟)) → δ , (δ∈σ
      , k δ (subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (Lset-suc δ)) z∈𝒟)) })
    (Lset-out σ z z∈Lσ)

The tower decomposes the membership of z truncatedly: some stage δ below σ with z in the definable powerset of Lset δ. The decomposition is mapped inside the truncation only: the successor identity, read backwards, transports z from 𝒟ₒ (Lset δ) into Lset (sucV δ), the observation k fires at that successor, and the resulting carve is injected back into the truncation.

One stage for everything below a set

This section turns stage transitivity and an ordinal bound into one level that contains a set's members, their members, and the limit level ω.

The other thing the construction needs is a bound, and no comparison is involved in getting one. A stage is transitive, so the stage of a set already holds the set's members, and their members after them; the earliest stage is a stage like any other, so it serves.

One more ordinal remains to be fixed: the tower's limit level. The comparison ahead is written in the object language, and the codes of all parameter-free formulas Formula ⊥* n, of every arity, belong to Lset ω; such a code may have free variables, so these are formulas, not sentences. A full name of a member of a successor stage says more than its code: it names the arity and a vector of parameters from earlier stages. The bound covers the codes, because ω ∈ β and monotonicity lift Lset ω into Lset β; the parameters lie below the bound for the reason the next fact records: members of the set and members of those land in the same level.

stage-below : (a : S) (p : ⟨ isL a ⟩) (x : S) → ⟨ x ∈ˢ a ⟩
            → ⟨ x ∈ˢ Lset (stage a p) ⟩
stage-below a p x x∈a =
  layer-trans (Lset-layer (stage a p)) x∈a (stage-mem a p)

Stages are transitive, and the earliest stage of a is a stage. So a member x of a lies in the tower's level at a's own stage: transitivity moves the membership from the set into the level that holds the set.

stage-below₂ : (a : S) (p : ⟨ isL a ⟩) (x y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ a ⟩
             → ⟨ y ∈ˢ Lset (stage a p) ⟩
stage-below₂ a p x y y∈x x∈a =
  layer-trans (Lset-layer (stage a p)) y∈x (stage-below a p x x∈a)

Transitivity applied twice reaches two levels down: a member of a member of a lies in the same level, because it lies in x and x lies in the level.

stageBound : (a : S) (p : ⟨ isL a ⟩)
           → Σ[ β ∈ S ] (IsOrd β × ⟨ ω ∈ˢ β ⟩ × ⟨ stage a p ∈ˢ β ⟩)
stageBound a p = bound2 ω (stage a p) ω-ord (stage-ord a p)

The two ordinals that must be dominated are the limit level ω and the set's own earliest stage; bound2 returns a single ordinal above both, with its ordinality certified.

bound-below₂ : (a : S) (p : ⟨ isL a ⟩) (x y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ a ⟩
             → ⟨ y ∈ˢ Lset (stageBound a p .fst) ⟩
bound-below₂ a p x y y∈x x∈a =
  Lset-mono (stageBound a p .snd .snd .snd) (stage-below₂ a p x y y∈x x∈a)

Monotonicity of the tower lifts the two-level fact from the earliest stage into the stage of the bounding ordinal. One level now holds a, its members, their members, and the formula codes the comparison reads.

Recap

The chapter's reusable outputs are the unique predecessor of a least stage, when that stage is a successor, and a bounding ordinal large enough for the choice construction. The least-stage lemma is conditional, and the condition is its content. For a property of ordinals with least stage σ, the property may well hold first at the zero ordinal, and then there is nothing below to carve. When a carve at σ merely exists, an ordinal below σ at whose successor the property already holds, carveAt produces it, predOf turns it into the unique predecessor by closing the truncation on isPropPredOf, and ord-suc-inj is why a successor determines what it succeeds. stageBound supplies the bounding ordinal: above a set's own stage, hence above its members and theirs, and above the tower's limit level, where the formula codes live.