--- title: "Reflection for an arbitrary formula" module: L.FormulaReflection lang: en site: "Bedrock" description: "Reflection for an arbitrary formula" stage: "Constructible stages and the axioms" reading_order: 34 canonical: https://bedrock.institute/en/L.FormulaReflection.html html: L.FormulaReflection.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/FormulaReflection.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantBounding, FOL.Manipulation.Relativization, FOL.Absoluteness, V.Hierarchy, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Separation, L.ExistentialReflection] routes: [constructible-axioms] translations: [https://bedrock.institute/zh/L.FormulaReflection.md, https://bedrock.institute/ja/L.FormulaReflection.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # Reflection for an arbitrary formula Reflection for a whole formula must answer the existential subformulas that appear throughout its syntax. A joint closure condition and ordinal ladder are built recursively over the formula, yielding a stage in which the formula has the same truth value as in the full constructible universe. 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. ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Classical using ( LEM ) module L.FormulaReflection {ℓ : 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`) ```agda open import FOL.Manipulation.ConstantBounding using ( BoundedTm; BoundedFo ) open import FOL.Manipulation.Relativization 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.ExistentialReflection {ℓ} 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 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 the argument is direct: 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. ```agda module Cor (β : V ℓ) (oβ : IsOrd β) = Correct 𝒮ʟ id (LsetS β oβ) ``` ## What a stage owes a formula Walking a formula, the unbounded quantifiers are the nodes that require extra work: 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 conditions a rung must satisfy; 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 included in the stage. These conditions only grow easier to satisfy 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. ```agda 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σ τ = 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σ _ = 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 we construct the step that satisfies these conditions. 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 with no extra conditions 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 ten 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 ten 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. ```agda 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σ = 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. ```agda 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 these conditions back off gives closure. At a rung, the tree gives that the matrix's step function lies inside the next rung, and the previous chapter gives that 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 auxiliary facts let the induction 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. ```agda 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 case is the one from the previous chapter. Downward, a witness from the stage is a witness in L, and the hypothesis transfers it. Upward is the case of closure: the truth of the existential in L is, by definition, the satisfiability the closure lemma consumes, so closure returns 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 no circularity arises here, and why the stage never has to be a fixed point of anything. The universal case is the existential case for the negated matrix, argued by contradiction. If some element of L failed the matrix, that failure would be a witness for the negated matrix, so closure would produce one inside the stage; but the hypothesis asserts that everything in the stage satisfies the matrix, a contradiction. Deciding whether the element fails is where the excluded middle enters the induction, and it is the only place. ```agda 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 , (λ yes → lift (no yes)) ∣₁) where collide : Σ[ q ∈ S ] (⟨ fst q ∈ Lset β ⟩ × ⟨ (q ∷ γ) ⊨ (¬̇ χ) ⟩) → ⟨ (x ∷ γ) ⊨ χ ⟩ collide (q , (fq∈ , refute)) = Empty.rec (lower (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γ = 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 convenient form to use: the right-hand side is Δ₀, so a formula of any complexity has been replaced by 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. ```agda 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 route from the whole language to the bounded fragment that the separation chapter can already use to carve out sets, and it is the final link 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.