Bedrock任意公式的反射
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图对整条公式的反射，必须为其语法中各处出现的存在子公式给出答案。本章沿公式递归构造联合封闭条件与序数梯，得到一层，使该公式在其中与整个可构造宇宙中具有相同真值。
证明是结构归纳，它需要该层具备两样东西。在无界量词处，需要上一章的闭包，针对该量词自己的矩阵。在有界量词处，需要那个界落在该层里，好让落在界内的一切也落在其中；那正是分离那一章早已会满足的常元条件。
没有哪个针对单一矩阵的极限能同时覆盖全部矩阵，因为闭包不为更大的层所继承：把层扩大，就有更多环境需要它处理。因此这架梯要联合构造：每一级的步进沿公式的结构进行，把其中每个矩阵的单矩阵步进合并起来，连同包含常元的那一层。于是极限对每个矩阵都给出回答，上一章的论证施于其中每一个即可，无须重做。
{-# 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)
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 ⟦_⟧ )
作为元素的层
相对化以一个常元界住诸量词，而该常元必须是模型的元素，故须证层可构造。确实可构造，而且很直接：公式「真」定义出一个集合的全体，故层是它自身的可定义子集，因而属于施于自身的那个算子，因而在下一层可构造。有了这一条，到某层的相对化便可实例化一次，其有界读法随即供归纳取用。
被封存的只是那份证书：作为模型元素的层是「层与证书」的对，而第一分量必须继续规约，因为「落在界内」与「落在层内」是同一句话，规约恰恰依赖这一点。证书则是另一回事。它经可定义性一路展开到涉及小性的检查，而它又存放于一个常元之中，于是类型中每个提到该常元的部分都会连带承担那次展开的代价；一章若用相对化公式作分离，没有这一行就要以分钟而非秒计。
module Cor (β : V ℓ) (oβ : IsOrd β) = Correct 𝒮ʟ id (LsetS β oβ)
层对公式的义务
沿公式走下去，需要额外处理的节点是无界量词：每个带一个矩阵，而上一章为该矩阵所造的步进函数必须落在下一级里。沿公式的结构把这些隶属关系收集起来，便得到该级必须满足的一组条件；它是一棵与公式同形的树，在原子处，以及在每个不绑定任何东西的节点处为空。
全称量词贡献的是否定后矩阵的步进，因为对它的论证是反证：要知道层中的一切都满足该矩阵，就是要知道 L 中没有东西反驳它，而须被纳入层里的正是那个反驳。
这些条件只会随着级的增大而更易满足，因为每一项都是一条隶属关系，而隶属关系经序数继承。正是这一点使下面的诸次合并能把各部分提升到它们的并处。
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
联合步骤
接下来构造满足这些条件的一步。沿公式递归，从当前一级出发构造位于其上的一个序数，并携带整棵隶属关系树。三种形状覆盖所有构造子：没有额外条件的节点取当前级自身的上界；有两个子节点时合并两个子序数；量词节点则在子节点之上再加入一个步进函数。
每种形状只写一次，并对任意负载与任意提升方式适用，因此递归本身由十条各占一行的子句组成，不必在每条子句中重复序数的计算。另一种直接写法是三套并行递归，每套都有十条子句，分别计算该序数、它的序数性以及当前级属于它；三者遍历同一棵树，并投影同一批上界。
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σ
联合梯
固定一条公式，以及一个装着调用方所需的其余东西的序数：它的常元，以及它将要在其上跑反射的任何集合。一级的步进就是把那个序数并进去的联合步进；自空序数迭代，得到上升的链，即一架梯，而上一章的极限机器原样适用。
有两条读法从该步进白得，因为它们本就被造了进去。那个额外的序数落在第一级里，因而落在极限之下。而在每一级上，整棵隶属树都对下一级成立，这正是归纳所要的、作答假设的那个形式。
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
把这组条件读回来就得到闭包。在某一级上，那棵树给出该矩阵的步进函数落在下一级里，而上一章给出该矩阵的作答层落在它的步进函数里；序数传递性把两者复合成那条作答假设，梯的闭包随之而来。
再补充两个辅助事实，归纳便可开始：属于一层是向下继承的，因为层传递；而词项的取值落在该层里，常元是因为它被登记过，变元是因为环境落在那里。
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γ
归纳
原子与常元是 refl，因为相对化不碰它们；联结词是同余。有界量词是第一个实质情形：它的见证本就落在界里，界落在层里，而层传递，故见证落在层里，归纳假设遂适用于扩展后的环境。
存在量词的情形归结为上一章的论证。向下：来自层的见证本来就是 L 中的见证，归纳假设把它转移过去。向上是闭包的情形：存在量词在 L 中为真，按定义正是闭包引理所处理的那种可满足性，于是闭包返回一个已在层之内的见证，归纳假设转而适用于这一个见证。请注意用的是哪个见证：不是 L 恰好给出的那个，而是闭包选出的那个。这正是此处不产生循环的原因，也正是那一层永远不必成为任何东西的不动点的原因。
全称量词的情形就是否定后矩阵的存在量词的情形，用反证法论证。若 L 的某个元素不满足该矩阵，那次失败便是否定后矩阵的一个见证，于是闭包会在层之内造出一个这样的见证；然而归纳假设断言层中的一切都满足该矩阵，两者矛盾。判定那个元素是否失败，正是排中律进入本次归纳之处，而且是唯一之处。
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) })
反射定理
把这次归纳与相对化的正确性复合，就把有界读法变回一次寻常的满足，只不过对象是相对化后的公式。这是便于使用的形式：右侧是 Δ₀ 的，故任意复杂度的公式已被换成一条有界公式加一个被明确指出的层。
整理成定理后，它接受一条公式和调用方要求包含在层中的任意序数，并返回一个包含该序数的层。这个额外序数不可省略：证书不会由较大层继承，所以调用方不能事后扩大层，以容纳自己已有的集合。调用方必须预先说明需要包含什么，联合步进会把这一要求一同带入构造。
这个包被封装起来，而这是本书至此最要紧的一次封装。若是透明的，它所命名的层会在每一级上一路展开到联合步进、界层引理与排中律；而凡在类型中提到该层的使用者，都会把那整次展开带进每一次转换检查，两个使用者恰恰都在类型中提到它，于是下一章根本无法完成。封装之后，那一层只是一个名字，使用者向它索取的四样东西，正是这个包已经陈述的四样。
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.κ∈β
小结
mkReflect 对任意公式以及任意必须装进去的序数，造出一层，公式在其上与它到该层的相对化一致。相对化是 Δ₀ 的，这便是从整个语言通向有界片段的途径：分离那一章因此能用有界片段来表述；它也是那一章的 Δ₀ 工具与两条以任意公式陈述的模型字段之间的最后一环。
经典的代价一如既往：排中律，用在下降处、判定可满足性处，以及此处全称情形再用一次。这里没有用到选择，也没有用到 L 的良序。