BedrockReflecting a whole formula
The previous chapter reflected one quantifier. A formula has many, and the aim is to tighten all of them at once: to find a stage at which every unbounded quantifier of a given formula may be read as ranging over that stage only, without changing the formula's truth in L. That is exactly what relativization names, so the statement is that a formula and its relativization to the stage agree, and since a relativization is Δ₀, the effect is to trade an arbitrary formula for a bounded one at the cost of naming a stage.
The proof is structural induction, and it needs two things of the stage. At an unbounded quantifier it needs the previous chapter's closure, for the quantifier's own matrix. At a bounded quantifier it needs the bound to lie in the stage, so that anything the bound admits does too; that is the constants condition the separation chapter already knows how to meet.
No single-matrix limit can serve all the matrices at once, because closure is not inherited by larger stages: enlarging the stage admits more environments to answer for. So the ladder is built jointly. One rung's step merges, over the formula's structure, the single-matrix step of every matrix in it, together with the stage holding the constants. The limit then answers for every matrix, and the previous chapter's argument applies to each without being run again.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.ReflectFo {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇ ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) -- lint-agda: keep (⊤̇ names the defining formula behind `LsetS`) open import FOL.Manipulation.Bounding using ( BoundedTm; BoundedFo ) open import FOL.Manipulation.Relativize using ( relativize; module Correct ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-layer; layer-trans ) open import L.Ordinal {ℓ} using ( ∅-ord; bound2 ) open import L.Axioms.Basic {ℓ} using ( LsetS ) open import L.Axioms.Separation {ℓ} lem using ( Below′; liftFoTo; mkBoundedFo ) open import L.Reflect {ℓ} lem using ( Below; LsetEnv; pickStage; ClosedFor; module Ladder; module Single ) open import Cubical.Data.Unit using ( Unit*; tt* ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁ ) import Cubical.Data.Empty as Empty open import Cubical.Data.Sum using ( _⊎_; inl; inr ) open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅ ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ using ( S ) module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ; ⟦_⟧ᵐ to ⟦_⟧ )
The stage as an element
Relativization bounds the quantifiers by a constant, and the constant has to be an element of the model, so a stage must be shown constructible. It is, and cheaply: the formula "true" defines the whole of a set, so a stage is a definable subset of itself, hence a member of the operator applied to itself, hence constructible one stage later. With that, relativization to a stage is instantiated once and its bounded reading is available for the induction.
The certificate is sealed, and only it: the stage as an element of the model is the pair of the stage with the certificate, and the first component has to keep reducing, since "lies in the bound" and "lies in the stage" are the same statement only because it does. The certificate is a different matter. It unfolds through definability into the smallness machinery, and it sits inside a constant, so every consumer that mentions the constant in a type would carry that unfolding along; a chapter that separates with a relativized formula takes minutes rather than seconds without this one line.
module Cor (β : V ℓ) (oβ : IsOrd β) = Correct (hPropAlgebra (ℓ-suc ℓ)) 𝒮ʟ id (LsetS β oβ)
What a stage owes a formula
Walking a formula, the unbounded quantifiers are the nodes that cost something: each carries a matrix, and the previous chapter's step function for that matrix has to land in the next rung. Collecting those memberships over the formula's structure gives the debt a rung owes, and it is a tree of the same shape as the formula, empty at the atoms and at every node that binds nothing.
A universal quantifier contributes the step for the negated matrix, because the argument for it is by contradiction: to know that everything in the stage satisfies the matrix is to know that nothing in L refutes it, and the refutation is what has to be caught inside the stage.
The debt only grows easier as the rung grows, since each entry is a membership and membership is inherited through an ordinal. That is what lets the merges below raise the pieces to their join.
Answers : ∀ {n} (φ : Formula S n) (σ : V ℓ) (oσ : IsOrd σ) (τ : V ℓ) → Type (ℓ-suc ℓ) Answers (t ∈̇ u) σ oσ τ = Unit* Answers (t ≐ u) σ oσ τ = Unit* Answers (φ ∧̇ ψ) σ oσ τ = Answers φ σ oσ τ × Answers ψ σ oσ τ Answers (φ ∨̇ ψ) σ oσ τ = Answers φ σ oσ τ × Answers ψ σ oσ τ Answers (φ ⇒̇ ψ) σ oσ τ = Answers φ σ oσ τ × Answers ψ σ oσ τ Answers (¬̇ φ) σ oσ τ = Answers φ σ oσ τ Answers ⊤̇ σ oσ τ = Unit* Answers ⊥̇ σ oσ τ = Unit* Answers (∃̇ φ) σ oσ τ = ⟨ Single.Fstep φ σ oσ ∈ τ ⟩ × Answers φ σ oσ τ Answers (∀̇ φ) σ oσ τ = ⟨ Single.Fstep (¬̇ φ) σ oσ ∈ τ ⟩ × Answers φ σ oσ τ Answers (∀̇∈ t φ) σ oσ τ = Answers φ σ oσ τ Answers (∃̇∈ t φ) σ oσ τ = Answers φ σ oσ τ Answers-mono : {τ τ' : V ℓ} → ⟨ τ ∈ τ' ⟩ → IsOrd τ' → ∀ {n} (φ : Formula S n) (σ : V ℓ) (oσ : IsOrd σ) → Answers φ σ oσ τ → Answers φ σ oσ τ' Answers-mono h o (t ∈̇ u) σ oσ _ = tt* Answers-mono h o (t ≐ u) σ oσ _ = tt* Answers-mono h o (φ ∧̇ ψ) σ oσ (a , b) = Answers-mono h o φ σ oσ a , Answers-mono h o ψ σ oσ b Answers-mono h o (φ ∨̇ ψ) σ oσ (a , b) = Answers-mono h o φ σ oσ a , Answers-mono h o ψ σ oσ b Answers-mono h o (φ ⇒̇ ψ) σ oσ (a , b) = Answers-mono h o φ σ oσ a , Answers-mono h o ψ σ oσ b Answers-mono h o (¬̇ φ) σ oσ a = Answers-mono h o φ σ oσ a Answers-mono h o ⊤̇ σ oσ _ = tt* Answers-mono h o ⊥̇ σ oσ _ = tt* Answers-mono {τ} h o (∃̇ φ) σ oσ (F , a) = o .fst {x = τ} {y = Single.Fstep φ σ oσ} F h , Answers-mono h o φ σ oσ a Answers-mono {τ} h o (∀̇ φ) σ oσ (F , a) = o .fst {x = τ} {y = Single.Fstep (¬̇ φ) σ oσ} F h , Answers-mono h o φ σ oσ a Answers-mono h o (∀̇∈ t φ) σ oσ a = Answers-mono h o φ σ oσ a Answers-mono h o (∃̇∈ t φ) σ oσ a = Answers-mono h o φ σ oσ a
The joint step
Now the step that pays the debt. Recursion on the formula produces, from a rung, an ordinal above it carrying the whole tree of memberships. Three shapes cover every constructor: a node that owes nothing takes the rung's own bound; a node with two children merges its children's ordinals; a quantifier adds one step function to its child's.
Each shape is written once, over an arbitrary payload with an arbitrary way of raising it, so the recursion itself is twelve one-line clauses and the ordinal bookkeeping is not restated at each. The alternative, which is what one writes first, is three parallel recursions of twelve clauses each computing the ordinal, its ordinality, and the rung's membership in it; they all traverse the same tree and project the same bounds.
private Box : (σ : V ℓ) (P : V ℓ → Type (ℓ-suc ℓ)) → Type (ℓ-suc ℓ) Box σ P = Σ[ τ ∈ V ℓ ] (IsOrd τ × ⟨ σ ∈ τ ⟩ × P τ) Raise : (P : V ℓ → Type (ℓ-suc ℓ)) → Type (ℓ-suc ℓ) Raise P = {τ τ' : V ℓ} → ⟨ τ ∈ τ' ⟩ → IsOrd τ' → P τ → P τ' unitBox : (σ : V ℓ) (oσ : IsOrd σ) → Box σ (λ _ → Unit*) unitBox σ oσ = b .fst , (b .snd .fst , (b .snd .snd .fst , tt*)) where b = bound2 σ σ oσ oσ joinBox : {σ : V ℓ} {P Q : V ℓ → Type (ℓ-suc ℓ)} → Raise P → Raise Q → Box σ P → Box σ Q → Box σ (λ τ → P τ × Q τ) joinBox {σ} rP rQ (τ₁ , (o₁ , (s₁ , p))) (τ₂ , (o₂ , (_ , q))) = b .fst , ( ob , ( ob .fst {x = τ₁} {y = σ} s₁ (b .snd .snd .fst) , ( rP (b .snd .snd .fst) ob p , rQ (b .snd .snd .snd) ob q ) ) ) where b = bound2 τ₁ τ₂ o₁ o₂ ob = b .snd .fst addBox : {σ : V ℓ} {P : V ℓ → Type (ℓ-suc ℓ)} → Raise P → (F : V ℓ) → IsOrd F → Box σ P → Box σ (λ τ → ⟨ F ∈ τ ⟩ × P τ) addBox {σ} rP F oF (τ , (oτ , (s , p))) = b .fst , ( ob , ( ob .fst {x = τ} {y = σ} s (b .snd .snd .snd) , ( b .snd .snd .fst , rP (b .snd .snd .snd) ob p ) ) ) where b = bound2 F τ oF oτ ob = b .snd .fst raiseAns : ∀ {n} (φ : Formula S n) (σ : V ℓ) (oσ : IsOrd σ) → Raise (Answers φ σ oσ) raiseAns φ σ oσ h o = Answers-mono h o φ σ oσ gstep : ∀ {n} (φ : Formula S n) (σ : V ℓ) (oσ : IsOrd σ) → Box σ (Answers φ σ oσ) gstep (t ∈̇ u) σ oσ = unitBox σ oσ gstep (t ≐ u) σ oσ = unitBox σ oσ gstep (φ ∧̇ ψ) σ oσ = joinBox (raiseAns φ σ oσ) (raiseAns ψ σ oσ) (gstep φ σ oσ) (gstep ψ σ oσ) gstep (φ ∨̇ ψ) σ oσ = joinBox (raiseAns φ σ oσ) (raiseAns ψ σ oσ) (gstep φ σ oσ) (gstep ψ σ oσ) gstep (φ ⇒̇ ψ) σ oσ = joinBox (raiseAns φ σ oσ) (raiseAns ψ σ oσ) (gstep φ σ oσ) (gstep ψ σ oσ) gstep (¬̇ φ) σ oσ = gstep φ σ oσ gstep ⊤̇ σ oσ = unitBox σ oσ gstep ⊥̇ σ oσ = unitBox σ oσ gstep (∃̇ φ) σ oσ = addBox (raiseAns φ σ oσ) (Single.Fstep φ σ oσ) (Single.Fstep-ord φ σ oσ) (gstep φ σ oσ) gstep (∀̇ φ) σ oσ = addBox (raiseAns φ σ oσ) (Single.Fstep (¬̇ φ) σ oσ) (Single.Fstep-ord (¬̇ φ) σ oσ) (gstep φ σ oσ) gstep (∀̇∈ t φ) σ oσ = gstep φ σ oσ gstep (∃̇∈ t φ) σ oσ = gstep φ σ oσ
The joint ladder
Fix a formula and an ordinal holding whatever else the caller needs held: its constants, and any set it will run the reflection on. One rung's step is the joint step with that ordinal merged in; iterating from the empty ordinal gives an ascending chain, so a ladder, and the previous chapter's limit machinery applies to it unchanged.
Two readings come off the step for free, because they were built into it. The extra ordinal is in the first rung, hence under the limit. And at every rung, the whole tree of memberships holds against the next rung, which is the answering hypothesis in the form the induction wants.
module Mk {n : ℕ} (φ₀ : Formula S n) (κ : V ℓ) (oκ : IsOrd κ) (bdd : BoundedFo (Below′ κ) φ₀) where private jstep : (σ : V ℓ) (oσ : IsOrd σ) → Box σ (λ τ → ⟨ κ ∈ τ ⟩ × Answers φ₀ σ oσ τ) jstep σ oσ = addBox (raiseAns φ₀ σ oσ) κ oκ (gstep φ₀ σ oσ) Gₙ : ℕ → V ℓ Gₙ-ord : (N : ℕ) → IsOrd (Gₙ N) Gₙ zero = ∅ Gₙ (suc N) = jstep (Gₙ N) (Gₙ-ord N) .fst Gₙ-ord zero = ∅-ord Gₙ-ord (suc N) = jstep (Gₙ N) (Gₙ-ord N) .snd .fst Gₙ-step : (N : ℕ) → ⟨ Gₙ N ∈ Gₙ (suc N) ⟩ Gₙ-step N = jstep (Gₙ N) (Gₙ-ord N) .snd .snd .fst module Lad = Ladder Gₙ Gₙ-ord Gₙ-step β : V ℓ β = Lad.top oβ : IsOrd β oβ = Lad.top-ord κ∈β : ⟨ κ ∈ β ⟩ κ∈β = oβ .fst {x = Gₙ 1} {y = κ} (jstep ∅ ∅-ord .snd .snd .snd .fst) (Lad.G∈top 1) answersAt : (N : ℕ) → Answers φ₀ (Gₙ N) (Gₙ-ord N) (Gₙ (suc N)) answersAt N = jstep (Gₙ N) (Gₙ-ord N) .snd .snd .snd .snd
Reading the debt back off gives closure. At a rung, the tree says the matrix's step function is inside the next rung, and the previous chapter says the matrix's answering stage is inside its step function; ordinal transitivity composes them into the answering hypothesis, and the ladder's closure follows.
Two small dictionaries and the induction can start: membership in a stage is inherited downward, since a stage is transitive, and a term's value lies in the stage, a constant because it was registered and a variable because the environment lies there.
private closureOf : {k : ℕ} (ψ : Formula S (suc k)) → ((N : ℕ) → ⟨ Single.Fstep ψ (Gₙ N) (Gₙ-ord N) ∈ Gₙ (suc N) ⟩) → ClosedFor β ψ closureOf ψ lands = Lad.closure ψ (λ N ms → Gₙ-ord (suc N) .fst {x = Single.Fstep ψ (Gₙ N) (Gₙ-ord N)} {y = pickStage ψ (LsetEnv (Gₙ N) (Gₙ-ord N) ms)} (Single.pickLand ψ (Gₙ N) (Gₙ-ord N) ms) (lands N)) open Cor β oβ using ( _⊨ᴬ_; relativize-correct ) private transβ : {x y : V ℓ} → ⟨ x ∈ y ⟩ → ⟨ y ∈ Lset β ⟩ → ⟨ x ∈ Lset β ⟩ transβ = layer-trans (Lset-layer β) lookupInLayer : ∀ {m} (i : Fin m) (γ : S ^ m) → Below β γ → ⟨ fst (lookup i γ) ∈ Lset β ⟩ lookupInLayer zero (a ∷ γ) (ha , _) = ha lookupInLayer (suc i) (a ∷ γ) (_ , hγ) = lookupInLayer i γ hγ tmInLayer : ∀ {m} (t : Term S m) (γ : S ^ m) → Below β γ → BoundedTm (Below′ β) t → ⟨ fst (⟦ t ⟧ γ) ∈ Lset β ⟩ tmInLayer (con c) γ _ h = h tmInLayer (var i) γ bγ _ = lookupInLayer i γ bγ
The induction
Atoms and constants are refl, since relativization does not touch them; the connectives are congruence. A bounded quantifier is the first real step: its witnesses already lie in the bound, the bound lies in the stage, and the stage is transitive, so the witnesses lie in the stage and the induction hypothesis applies to the extended environment.
The existential is the previous chapter. Downward, a witness from the stage is a witness in L, and the hypothesis converts it. Upward is closure: the truth of the existential in L is, by definition, the satisfiability the closure lemma consumes, so it hands back a witness already inside the stage, and the hypothesis applies to that one instead. Note which witness is used: not the one L happened to supply, but the one closure chose. That is why nothing circular happens, and why the stage never has to be a fixed point of anything.
The universal is the existential for the negated matrix, argued by contradiction. If some element of L failed the matrix, that failure is a witness for the negated matrix, so closure produces one inside the stage; but the hypothesis says everything in the stage satisfies the matrix, and the two collide. Deciding whether the element fails is where the excluded middle enters the induction, and it is the only place.
reflectFo : ∀ {m} (χ : Formula S m) → ((N : ℕ) → Answers χ (Gₙ N) (Gₙ-ord N) (Gₙ (suc N))) → BoundedFo (Below′ β) χ → (γ : S ^ m) → Below β γ → (γ ⊨ χ) ≡ (γ ⊨ᴬ χ) private reflect∃ : ∀ {m} (χ : Formula S (suc m)) → ClosedFor β χ → ((N : ℕ) → Answers χ (Gₙ N) (Gₙ-ord N) (Gₙ (suc N))) → BoundedFo (Below′ β) χ → (γ : S ^ m) → Below β γ → (γ ⊨ (∃̇ χ)) ≡ (γ ⊨ᴬ (∃̇ χ)) reflect∃ χ cl an bd γ bγ = ⇔toPath fwd bwd where fwd : ⟨ γ ⊨ (∃̇ χ) ⟩ → ⟨ γ ⊨ᴬ (∃̇ χ) ⟩ fwd ex = PT.map (λ { (q , (fq∈ , satq)) → q , (fq∈ , subst ⟨_⟩ (reflectFo χ an bd (q ∷ γ) (fq∈ , bγ)) satq) }) (cl γ bγ ex) bwd : ⟨ γ ⊨ᴬ (∃̇ χ) ⟩ → ⟨ γ ⊨ (∃̇ χ) ⟩ bwd = PT.map (λ { (x , (x∈A , satx)) → x , subst ⟨_⟩ (sym (reflectFo χ an bd (x ∷ γ) (x∈A , bγ))) satx }) reflect∀ : ∀ {m} (χ : Formula S (suc m)) → ClosedFor β (¬̇ χ) → ((N : ℕ) → Answers χ (Gₙ N) (Gₙ-ord N) (Gₙ (suc N))) → BoundedFo (Below′ β) χ → (γ : S ^ m) → Below β γ → (γ ⊨ (∀̇ χ)) ≡ (γ ⊨ᴬ (∀̇ χ)) reflect∀ χ cl an bd γ bγ = ⇔toPath fwd bwd where fwd : ⟨ γ ⊨ (∀̇ χ) ⟩ → ⟨ γ ⊨ᴬ (∀̇ χ) ⟩ fwd h x x∈A = subst ⟨_⟩ (reflectFo χ an bd (x ∷ γ) (x∈A , bγ)) (h x) bwd : ⟨ γ ⊨ᴬ (∀̇ χ) ⟩ → ⟨ γ ⊨ (∀̇ χ) ⟩ bwd H x = decide (lem ((x ∷ γ) ⊨ χ)) where decide : (⟨ (x ∷ γ) ⊨ χ ⟩ ⊎ (⟨ (x ∷ γ) ⊨ χ ⟩ → Empty.⊥)) → ⟨ (x ∷ γ) ⊨ χ ⟩ decide (inl yes) = yes decide (inr no) = PT.rec (snd ((x ∷ γ) ⊨ χ)) collide (cl γ bγ ∣ x , no ∣₁) where collide : Σ[ q ∈ S ] (⟨ fst q ∈ Lset β ⟩ × ⟨ (q ∷ γ) ⊨ (¬̇ χ) ⟩) → ⟨ (x ∷ γ) ⊨ χ ⟩ collide (q , (fq∈ , refute)) = Empty.rec (refute (subst ⟨_⟩ (sym (reflectFo χ an bd (q ∷ γ) (fq∈ , bγ))) (H q fq∈))) reflectFo (t ∈̇ u) an bd γ bγ = refl reflectFo (t ≐ u) an bd γ bγ = refl reflectFo (χ ∧̇ ψ) an bd γ bγ = cong₂ _⊓_ (reflectFo χ (λ N → an N .fst) (bd .fst) γ bγ) (reflectFo ψ (λ N → an N .snd) (bd .snd) γ bγ) reflectFo (χ ∨̇ ψ) an bd γ bγ = cong₂ _⊔_ (reflectFo χ (λ N → an N .fst) (bd .fst) γ bγ) (reflectFo ψ (λ N → an N .snd) (bd .snd) γ bγ) reflectFo (χ ⇒̇ ψ) an bd γ bγ = cong₂ _⇒_ (reflectFo χ (λ N → an N .fst) (bd .fst) γ bγ) (reflectFo ψ (λ N → an N .snd) (bd .snd) γ bγ) reflectFo (¬̇ χ) an bd γ bγ = cong ¬_ (reflectFo χ an bd γ bγ) reflectFo ⊤̇ an bd γ bγ = refl reflectFo ⊥̇ an bd γ bγ = refl reflectFo (∃̇ χ) an bd γ bγ = reflect∃ χ (closureOf χ (λ N → an N .fst)) (λ N → an N .snd) bd γ bγ reflectFo (∀̇ χ) an bd γ bγ = reflect∀ χ (closureOf (¬̇ χ) (λ N → an N .fst)) (λ N → an N .snd) bd γ bγ reflectFo (∀̇∈ t χ) an bd γ bγ = ⇔toPath fwd bwd where tInβ : ⟨ fst (⟦ t ⟧ γ) ∈ Lset β ⟩ tInβ = tmInLayer t γ bγ (bd .fst) fwd : ⟨ γ ⊨ (∀̇∈ t χ) ⟩ → ⟨ γ ⊨ᴬ (∀̇∈ t χ) ⟩ fwd h x x∈t = subst ⟨_⟩ (reflectFo χ an (bd .snd) (x ∷ γ) (transβ x∈t tInβ , bγ)) (h x x∈t) bwd : ⟨ γ ⊨ᴬ (∀̇∈ t χ) ⟩ → ⟨ γ ⊨ (∀̇∈ t χ) ⟩ bwd h x x∈t = subst ⟨_⟩ (sym (reflectFo χ an (bd .snd) (x ∷ γ) (transβ x∈t tInβ , bγ))) (h x x∈t) reflectFo (∃̇∈ t χ) an bd γ bγ = ⇔toPath fwd bwd where tInβ : ⟨ fst (⟦ t ⟧ γ) ∈ Lset β ⟩ tInβ = tmInLayer t γ bγ (bd .fst) fwd : ⟨ γ ⊨ (∃̇∈ t χ) ⟩ → ⟨ γ ⊨ᴬ (∃̇∈ t χ) ⟩ fwd = PT.map (λ { (x , (x∈t , h)) → x , (x∈t , subst ⟨_⟩ (reflectFo χ an (bd .snd) (x ∷ γ) (transβ x∈t tInβ , bγ)) h) }) bwd : ⟨ γ ⊨ᴬ (∃̇∈ t χ) ⟩ → ⟨ γ ⊨ (∃̇∈ t χ) ⟩ bwd = PT.map (λ { (x , (x∈t , h)) → x , (x∈t , subst ⟨_⟩ (sym (reflectFo χ an (bd .snd) (x ∷ γ) (transβ x∈t tInβ , bγ))) h) })
The theorem
Composing the induction with the correctness of relativization turns the bounded reading back into an ordinary satisfaction, of the relativized formula. That is the usable form: the right-hand side is Δ₀, so a formula of any complexity has been traded for a bounded one and a named stage.
Packaged, the theorem takes the formula and any ordinal the caller wants inside the stage, and returns a stage containing it. The extra ordinal is not a convenience: the certificate is not inherited by larger stages, so a caller cannot enlarge the stage afterwards to fit the set it is working with. It has to say up front what must fit, and the joint step carries it.
The package is sealed, and this is the seal that matters most in the book so far. Transparent, the stage it names unfolds through the joint step, the bounding lemma and the excluded middle at every rung; a consumer that mentions the stage in a type, as both consumers do, would drag that whole unfolding into every conversion check, and the next chapter simply does not finish. Sealed, the stage is a name, and the four things a consumer needs of it are the four the package already states.
reflectRel : (γ : S ^ n) → Below β γ → (γ ⊨ φ₀) ≡ (γ ⊨ relativize (LsetS β oβ) φ₀) reflectRel γ bγ = reflectFo φ₀ answersAt (liftFoTo κ∈β φ₀ bdd) γ bγ ∙ sym (relativize-correct φ₀ γ) opaque mkReflect : ∀ {n} (φ : Formula S n) (δ : V ℓ) → IsOrd δ → Σ[ β ∈ V ℓ ] Σ[ oβ ∈ IsOrd β ] (⟨ δ ∈ β ⟩ × ((γ : S ^ n) → Below β γ → (γ ⊨ φ) ≡ (γ ⊨ relativize (LsetS β oβ) φ))) mkReflect φ δ oδ = M.β , (M.oβ , (δ∈β , M.reflectRel)) where bdd : Σ[ σ ∈ V ℓ ] (IsOrd σ × BoundedFo (Below′ σ) φ) bdd = mkBoundedFo φ b : Σ[ τ ∈ V ℓ ] (IsOrd τ × ⟨ bdd .fst ∈ τ ⟩ × ⟨ δ ∈ τ ⟩) b = bound2 (bdd .fst) δ (bdd .snd .fst) oδ module M = Mk φ (b .fst) (b .snd .fst) (liftFoTo (b .snd .snd .fst) φ (bdd .snd .snd)) δ∈β : ⟨ δ ∈ M.β ⟩ δ∈β = M.oβ .fst {x = b .fst} {y = δ} (b .snd .snd .snd) M.κ∈β
Recap
mkReflect produces, for any formula and any ordinal that must fit inside it, a stage at which the formula agrees with its relativization to that stage. Since a relativization is Δ₀, this is the bridge from the whole language to the bounded fragment the separation chapter can already carve with, and it is the last thing standing between that chapter's Δ₀ instruments and the two model fields stated for arbitrary formulas.
The classical cost is unchanged: the excluded middle, in the descent, in deciding satisfiability, and once more in the universal case here. No choice, and no well-ordering of L.