Reflecting an existential into a stage

The separation chapter carved subsets of a stage using formulas whose quantifiers were already bounded, and that sufficed because a bounded formula asks only about what a stage already contains. An unbounded existential does not: it asks whether somewhere in L there is a witness, and L is a proper class. To carve with such a formula, the class-sized question has to be answered inside a set.

It can be, and the argument is Montague's. Fix a matrix and an environment of parameters. If a witness exists at all, there is a least stage containing one, and that stage is a set-sized answer to a class-sized question. Run over all tuples of parameters drawn from one stage, bound the answers, and the result is a single stage that answers for every tuple from the stage below. Iterate that step through the natural numbers and take the union: the limit answers for its own parameters, because any finite tuple from the limit already lies in some finite layer, whose answers were bounded at the next.

Two things are done differently here than they usually are. The choice of witness is where a well-ordering of L is normally invoked, and it is not needed: what the argument wants is a canonical ordinal, not a canonical element, and the ordinals are already well-ordered by membership. So the least stage that holds a witness is taken directly, by the descent of the stage chapter, and which witness lives there is never decided. And the parameters are a tuple from the start. Writing the one-parameter case first and generalizing later would mean writing the whole construction twice, since every step of it is indifferent to how many parameters there are; the only place the tuple is felt at all is in locating it, where finitely many layers have to be merged into one.

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; ∃̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset-in; Lset-out
        ; Lset→isL )
open import L.Ordinal {ℓ} using ( ∅-ord; boundingOrd; bound2; setUnion-ord )
open import L.Stage {ℓ} lem using ( LeastOrd; leastOrd )

open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Data.Nat using ( _+_; +-comm )
open import Cubical.Data.Unit using ( Unit*; tt* )
import Cubical.Data.Empty as Empty
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Functions.Logic using ( ⇔toPath; ∃[∶]-syntax )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; sett; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ⋃_; union-ax )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ʟ using ( S )

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )

Environments drawn from a stage

An element of a stage becomes an element of the class model by the tower's membership criterion, so a stage's index set is a supply of parameters, and a tuple of indices is a supply of environments. That is what makes the bounding lemma applicable below: the tuples form a type of the ambient size, being a vector over one.

An environment lies below a stage when each of its entries does. Reading the tuple of indices back off such an environment is the inverse operation, and it returns the equation as well, since the construction will need to know that the environment it bounded is the one it was given. The equation is where constructibility being a proposition is used: two elements of the model agree as soon as their underlying sets do.

LsetElt : (σ : V ℓ) → IsOrd σ → ⟪ Lset σ ⟫ → S
LsetElt σ oσ m = ⟪ Lset σ ⟫↪ m
               , Lset→isL σ oσ (⟪ Lset σ ⟫↪ m)
                   (∈∈ₛ {a = ⟪ Lset σ ⟫↪ m} {b = Lset σ} .snd (∈ₛ⟪ Lset σ ⟫↪ m))

LsetEnv : (σ : V ℓ) (oσ : IsOrd σ) {k : ℕ} → ⟪ Lset σ ⟫ ^ k → S ^ k
LsetEnv σ oσ []       = []
LsetEnv σ oσ (m ∷ ms) = LsetElt σ oσ m ∷ LsetEnv σ oσ ms

Below : (σ : V ℓ) {k : ℕ} → S ^ k → Type (ℓ-suc ℓ)
Below σ []      = Unit*
Below σ (p ∷ ρ) = ⟨ fst p ∈ Lset σ ⟩ × Below σ ρ

Below-mono : {σ τ : V ℓ} → ⟨ σ ∈ τ ⟩ → {k : ℕ} {ρ : S ^ k}
           → Below σ ρ → Below τ ρ
Below-mono σ∈τ {ρ = []}    _         = tt*
Below-mono σ∈τ {ρ = p ∷ ρ} (h , hs) =
  Lset-mono σ∈τ h , Below-mono σ∈τ hs

indexEnv : (σ : V ℓ) (oσ : IsOrd σ) {k : ℕ} (ρ : S ^ k) → Below σ ρ
         → Σ[ ms ∈ ⟪ Lset σ ⟫ ^ k ] (LsetEnv σ oσ ms ≡ ρ)
indexEnv σ oσ []      _        = [] , refl
indexEnv σ oσ (p ∷ ρ) (h , hs) = (m ∷ fst rest) , cong₂ _∷_ eltEq (snd rest)
  where
  fib = ∈-asFiber {a = fst p} {b = Lset σ} h
  m   = fib .fst
  eltEq : LsetElt σ oσ m ≡ p
  eltEq = Σ≡Prop (λ x → (isL x) .snd) (fib .snd)
  rest = indexEnv σ oσ ρ hs

The answering stage

Fix a matrix in one witness variable and k parameters. "Some witness for this environment lives in this stage" is a property of ordinals, so the stage chapter's descent applies to it directly. Its premise is that some ordinal has the property, which follows from satisfiability alone: a witness is an element of L, and an element of L lies in some stage by definition.

Totality then wants a value even when no witness exists, and the excluded middle supplies the case distinction. As in the stage chapter, the distinction is made by an explicit auxiliary rather than by a with, because the load-bearing lemma below has to name the very same decision value and match on it.

Sat : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k) → S → Ω
Sat ψ ρ q = (q ∷ ρ) ⊨ ψ

SatEx : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k) → Ω
SatEx ψ ρ = ∃[ q ∶ S ] Sat ψ ρ q

Wit : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k) → V ℓ → Ω
Wit ψ ρ σ = ∃[ q ∶ S ] ((fst q ∈ Lset σ) ⊓ Sat ψ ρ q)

witnessed : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k) → ⟨ SatEx ψ ρ ⟩
          → ∥ (Σ[ α ∈ V ℓ ] (IsOrd α × ⟨ Wit ψ ρ α ⟩)) ∥₁
witnessed ψ ρ = PT.rec squash₁
  (λ { (q , satq) → PT.map
      (λ { (α , (oα , q∈Lα)) → α , (oα , ∣ q , (q∈Lα , satq) ∣₁) })
      (q .snd) })

pick : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k) → ⟨ SatEx ψ ρ ⟩
     → LeastOrd (Wit ψ ρ)
pick ψ ρ sat = leastOrd (Wit ψ ρ) (witnessed ψ ρ sat)

decideStage : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k)
            → ⟨ SatEx ψ ρ ⟩ ⊎ (⟨ SatEx ψ ρ ⟩ → Empty.⊥) → V ℓ
decideStage ψ ρ (inl sat) = pick ψ ρ sat .fst
decideStage ψ ρ (inr _)   = ∅

pickStage : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k) → V ℓ
pickStage ψ ρ = decideStage ψ ρ (lem (SatEx ψ ρ))

decideStage-ord : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k)
                  (d : ⟨ SatEx ψ ρ ⟩ ⊎ (⟨ SatEx ψ ρ ⟩ → Empty.⊥))
                → IsOrd (decideStage ψ ρ d)
decideStage-ord ψ ρ (inl sat) = pick ψ ρ sat .snd .fst
decideStage-ord ψ ρ (inr _)   = ∅-ord

pickStage-ord : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k)
              → IsOrd (pickStage ψ ρ)
pickStage-ord ψ ρ = decideStage-ord ψ ρ (lem (SatEx ψ ρ))

And the property the whole construction rests on: if the environment is satisfiable at all, its answering stage really does hold a witness. The proof has to know which branch the decision took, and it cannot ask, because the decision is a value of the excluded middle and nothing computes it. So it does the standard thing: quantify over the branch, remember the equation that the branch is the decision, and transport along it. In the false branch the hypothesis refutes itself.

pickWitness : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k) → ⟨ SatEx ψ ρ ⟩
            → ⟨ Wit ψ ρ (pickStage ψ ρ) ⟩
pickWitness ψ ρ sat = go (lem (SatEx ψ ρ)) refl
  where
  go : (d : ⟨ SatEx ψ ρ ⟩ ⊎ (⟨ SatEx ψ ρ ⟩ → Empty.⊥))
     → lem (SatEx ψ ρ) ≡ d → ⟨ Wit ψ ρ (pickStage ψ ρ) ⟩
  go (inl s) e = subst (λ d → ⟨ Wit ψ ρ (decideStage ψ ρ d) ⟩) (sym e)
                   (pick ψ ρ s .snd .snd .fst)
  go (inr ¬s) e = Empty.rec (¬s sat)

Ladders and their limits

What the argument actually needs is not one particular tower but a ladder: an ascending chain of ordinals indexed by the naturals. Its limit is the union, an ordinal because the union of a family of ordinals is; each rung belongs to the limit, since it belongs to its own successor and the successor is one of the sets being unioned; and the chain reaches forward, a rung belonging to every strictly later one, by composing one step with the transitivity of the later rung.

Stating the reach with the gap as an explicit summand, rather than through an order relation, is what makes two rungs mergeable by addition alone. That matters because merging rungs is the only thing a tuple of parameters costs, and it is worth not paying for arithmetic to do it.

Separating the ladder from the tower is worth a moment's care, because the next chapter needs a ladder built differently: one whose single step closes all the matrices of a formula at once. Everything below is proved of the ladder, so that chapter builds its ladder and gets the argument, rather than running it again.

ClosedFor : (β : V ℓ) {k : ℕ} (ψ : Formula S (suc k)) → Type (ℓ-suc ℓ)
ClosedFor β {k} ψ = (ρ : S ^ k) → Below β ρ → ⟨ SatEx ψ ρ ⟩ → ⟨ Wit ψ ρ β ⟩

module Ladder (G : ℕ → V ℓ) (G-ord : (n : ℕ) → IsOrd (G n))
              (G-up : (n : ℕ) → ⟨ G n ∈ G (suc n) ⟩) where

  reach : (n d : ℕ) → ⟨ G n ∈ G (suc (d + n)) ⟩
  reach n zero    = G-up n
  reach n (suc d) =
    G-ord (suc (suc (d + n))) .fst {x = G (suc (d + n))} {y = G n}
      (reach n d) (G-up (suc (d + n)))

  fam : Lift {ℓ-zero} {ℓ} ℕ → V ℓ
  fam i = G (lower i)

  top : V ℓ
  top = ⋃ (sett (Lift {ℓ-zero} {ℓ} ℕ) fam)

  top-ord : IsOrd top
  top-ord = setUnion-ord (Lift {ℓ-zero} {ℓ} ℕ) fam (λ i → G-ord (lower i))

  G∈top : (n : ℕ) → ⟨ G n ∈ top ⟩
  G∈top n = ∈∈ₛ {a = G n} {b = top} .snd
    (union-ax (sett (Lift {ℓ-zero} {ℓ} ℕ) fam) (G n) .snd
      ∣ G (suc n)
      , ( ∈∈ₛ {a = G (suc n)} {b = sett (Lift {ℓ-zero} {ℓ} ℕ) fam} .fst
            ∣ lift (suc n) , refl ∣₁
        , ∈∈ₛ {a = G n} {b = G (suc n)} .fst (G-up n) ) ∣₁)

The closure argument needs its parameters on a rung, not merely under the limit. For one parameter, two inversions get it there: an ordinal in the limit belongs to one of the sets being unioned, hence to a rung; and a set in the stage of the limit belongs, by the tower's characterization, to the operator applied to the stage of some smaller ordinal, so locating that ordinal and going back in places the set in that rung's stage.

For a tuple, the rungs found for the entries have to be merged, and the reach lemma merges two of them: from rungs n and m, both reach rung suc (n + m), one of them directly and the other after commuting the sum. Recursion on the tuple merges all of them, and monotonicity carries the earlier entries up.

  δ∈top→fin : (δ : V ℓ) → ⟨ δ ∈ top ⟩ → ∥ (Σ[ N ∈ ℕ ] ⟨ δ ∈ G N ⟩) ∥₁
  δ∈top→fin δ δ∈ = PT.rec squash₁
    (λ { (v , (v∈ₛsett , δ∈ₛv)) → PT.map
        (λ { (i , Gi≡v) → lower i
           , ∈∈ₛ {a = δ} {b = G (lower i)} .snd
               (subst (λ w → ⟨ δ ∈ₛ w ⟩) (sym Gi≡v) δ∈ₛv) })
        (∈∈ₛ {a = v} {b = sett (Lift {ℓ-zero} {ℓ} ℕ) fam} .snd v∈ₛsett) })
    (union-ax (sett (Lift {ℓ-zero} {ℓ} ℕ) fam) δ .fst
      (∈∈ₛ {a = δ} {b = top} .fst δ∈))

  localize₁ : (e : V ℓ) → ⟨ e ∈ Lset top ⟩ → ∥ (Σ[ N ∈ ℕ ] ⟨ e ∈ Lset (G N) ⟩) ∥₁
  localize₁ e e∈ = PT.rec squash₁
    (λ { (δ , (δ∈top , e∈𝒟ₒδ)) → PT.map
        (λ { (N , δ∈GN) → N , Lset-in (G N) δ e δ∈GN e∈𝒟ₒδ })
        (δ∈top→fin δ δ∈top) })
    (Lset-out top e e∈)

  localize : {j : ℕ} (ρ : S ^ j) → Below top ρ → ∥ (Σ[ N ∈ ℕ ] Below (G N) ρ) ∥₁
  localize []      _        = ∣ zero , tt* ∣₁
  localize (p ∷ ρ) (h , hs) = PT.rec squash₁
    (λ { (N , h') → PT.map (merge N h') (localize ρ hs) })
    (localize₁ (fst p) h)
    where
    merge : (N : ℕ) → ⟨ fst p ∈ Lset (G N) ⟩
          → Σ[ M ∈ ℕ ] Below (G M) ρ
          → Σ[ M ∈ ℕ ] Below (G M) (p ∷ ρ)
    merge N h' (M , hs') = suc (M + N)
      , ( Lset-mono (reach N M) h'
        , Below-mono (subst (λ n → ⟨ G M ∈ G (suc n) ⟩) (+-comm N M)
                        (reach M N)) hs' )

  land : (q : S) (σ τ : V ℓ)
       → ⟨ fst q ∈ Lset σ ⟩ → ⟨ σ ∈ τ ⟩ → ⟨ τ ∈ top ⟩ → ⟨ fst q ∈ Lset top ⟩
  land q σ τ fq∈σ σ∈τ τ∈top =
    Lset-mono {α = top} {β = τ} τ∈top (Lset-mono {α = τ} {β = σ} σ∈τ fq∈σ)

Closure

A ladder answers for a matrix when every environment indexed from a rung has its answering stage on the next rung. That one hypothesis is all the closure argument uses about how the ladder was built, and it is what the next section and the next chapter each supply in their own way.

Given it, the limit is closed for the matrix. Locate the environment on a rung and name it there: it is the image of some tuple of indices of that rung's stage, up to an equality that the reading lemma returns along with the tuple. Its answering stage is on the next rung, so whatever lives in the answering stage lives in that rung's stage, hence under the limit; two applications of monotonicity, and the equation transported back.

  module _ {k : ℕ} (ψ : Formula S (suc k))
           (answers : (n : ℕ) (ms : ⟪ Lset (G n) ⟫ ^ k)
                    → ⟨ pickStage ψ (LsetEnv (G n) (G-ord n) ms) ∈ G (suc n) ⟩)
           where

    closure : ClosedFor top ψ
    closure ρ below sat = PT.rec squash₁ atRung (localize ρ below)
      where
      atRung : Σ[ N ∈ ℕ ] Below (G N) ρ → ⟨ Wit ψ ρ top ⟩
      atRung (N , belowN) = PT.map found (pickWitness ψ ρₘ satₘ)
        where
        idx = indexEnv (G N) (G-ord N) ρ belowN
        ρₘ : S ^ k
        ρₘ = LsetEnv (G N) (G-ord N) (idx .fst)
        e : ρₘ ≡ ρ
        e = idx .snd
        satₘ : ⟨ SatEx ψ ρₘ ⟩
        satₘ = subst (λ r → ⟨ SatEx ψ r ⟩) (sym e) sat
        found : Σ[ q ∈ S ] (⟨ fst q ∈ Lset (pickStage ψ ρₘ) ⟩ × ⟨ Sat ψ ρₘ q ⟩)
              → Σ[ q ∈ S ] (⟨ fst q ∈ Lset top ⟩ × ⟨ Sat ψ ρ q ⟩)
        found (q , (fq∈pick , satq)) = q
          , ( land q (pickStage ψ ρₘ) (G (suc N))
                fq∈pick (answers N (idx .fst)) (G∈top (suc N))
            , subst (λ r → ⟨ Sat ψ r q ⟩) e satq )

Which gives the theorem the later chapters consume. For an environment under the limit, the class model satisfies the existential exactly when a witness lies in the limit's stage. Forwards is closure; backwards is forgetting where the witness lives.

The forward direction needs no translation step, because the two sides are the same proposition already: the semantics of an existential quantifier is the truncated sum over the carrier, and that is what SatEx was defined to be. So the theorem is closure with its statement rewritten, and nothing is paid to cross between syntax and the meta-level.

    reflect-bwd : (ρ : S ^ k) → ⟨ Wit ψ ρ top ⟩ → ⟨ ρ ⊨ (∃̇ ψ) ⟩
    reflect-bwd ρ = PT.map (λ { (q , (_ , satq)) → q , satq })

    reflect : (ρ : S ^ k) → Below top ρ → (ρ ⊨ (∃̇ ψ)) ≡ Wit ψ ρ top
    reflect ρ below = ⇔toPath (closure ρ below) (reflect-bwd ρ)

The ladder for a single matrix

And the first ladder. A stage's index set is a type of the ambient size, and so is any tuple over it, so the bounding lemma applies: the answering stages of all the environments drawn from one stage have a common bound. Merging that bound with the stage itself gives the step, which therefore both contains its argument, so that iterating it climbs, and contains every answer for the argument's environments, which is exactly the answering hypothesis.

The step is sealed. Unfolded, it is a bound built from a bound built from the excluded middle, and the closure argument matches on rungs repeatedly; a transparent definition would push that whole tower into every conversion check. The three properties open the seal once each, and the last of them is the one place transitivity is used, so the chain from the answer through the bound into the step is closed inside the seal and the caller sees only its conclusion.

module Single {k : ℕ} (ψ : Formula S (suc k)) where

  Fbnd : (σ : V ℓ) (oσ : IsOrd σ)
       → Σ[ β ∈ V ℓ ] (IsOrd β × ((ms : ⟪ Lset σ ⟫ ^ k)
                                 → ⟨ pickStage ψ (LsetEnv σ oσ ms) ∈ β ⟩))
  Fbnd σ oσ = boundingOrd (⟪ Lset σ ⟫ ^ k)
                (λ ms → pickStage ψ (LsetEnv σ oσ ms))
                (λ ms → pickStage-ord ψ (LsetEnv σ oσ ms))

  opaque
    Fstep : (σ : V ℓ) → IsOrd σ → V ℓ
    Fstep σ oσ = bound2 (Fbnd σ oσ .fst) σ (Fbnd σ oσ .snd .fst) oσ .fst

  opaque
    unfolding Fstep

    Fstep-ord : (σ : V ℓ) (oσ : IsOrd σ) → IsOrd (Fstep σ oσ)
    Fstep-ord σ oσ = bound2 (Fbnd σ oσ .fst) σ (Fbnd σ oσ .snd .fst) oσ .snd .fst

    σ∈Fstep : (σ : V ℓ) (oσ : IsOrd σ) → ⟨ σ ∈ Fstep σ oσ ⟩
    σ∈Fstep σ oσ =
      bound2 (Fbnd σ oσ .fst) σ (Fbnd σ oσ .snd .fst) oσ .snd .snd .snd

    pickLand : (σ : V ℓ) (oσ : IsOrd σ) (ms : ⟪ Lset σ ⟫ ^ k)
             → ⟨ pickStage ψ (LsetEnv σ oσ ms) ∈ Fstep σ oσ ⟩
    pickLand σ oσ ms =
      Fstep-ord σ oσ .fst {x = Fbnd σ oσ .fst}
                          {y = pickStage ψ (LsetEnv σ oσ ms)}
        (Fbnd σ oσ .snd .snd ms)
        (bound2 (Fbnd σ oσ .fst) σ (Fbnd σ oσ .snd .fst) oσ .snd .snd .fst)

  βₙ : ℕ → V ℓ
  βₙ-ord : (n : ℕ) → IsOrd (βₙ n)
  βₙ zero        = ∅
  βₙ (suc n)     = Fstep (βₙ n) (βₙ-ord n)
  βₙ-ord zero    = ∅-ord
  βₙ-ord (suc n) = Fstep-ord (βₙ n) (βₙ-ord n)

  βₙ-step : (n : ℕ) → ⟨ βₙ n ∈ βₙ (suc n) ⟩
  βₙ-step n = σ∈Fstep (βₙ n) (βₙ-ord n)

  module L = Ladder βₙ βₙ-ord βₙ-step

  βω : V ℓ
  βω = L.top

  βω-ord : IsOrd βω
  βω-ord = L.top-ord

  answers : (n : ℕ) (ms : ⟪ Lset (βₙ n) ⟫ ^ k)
          → ⟨ pickStage ψ (LsetEnv (βₙ n) (βₙ-ord n) ms) ∈ βₙ (suc n) ⟩
  answers n = pickLand (βₙ n) (βₙ-ord n)

  closed : ClosedFor βω ψ
  closed = L.closure ψ answers

  reflect : (ρ : S ^ k) → Below βω ρ → (ρ ⊨ (∃̇ ψ)) ≡ Wit ψ ρ βω
  reflect = L.reflect ψ answers

Recap

A ladder is an ascending chain of ordinals; it answers for a matrix when each rung's environments have their answering stages on the next rung; and when it does, its limit is closed for that matrix, which reflect restates as the reflection of an existential. Single builds the ladder for one matrix, by bounding a stage's answers and merging with the stage.

The construction used the excluded middle twice, once to decide satisfiability and once inside the descent, and used the axiom of choice not at all. That is the point of taking the least stage rather than the least witness: the ordinals come well-ordered, and nothing here has to ask for a well-ordering of L.

What is delivered is one quantifier, at any number of parameters. An arbitrary formula has many quantifiers, hence many matrices, and no single-matrix limit serves them all; the next chapter builds a ladder whose step closes all of them at once, and gets everything above for it without rerunning any of it.