可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。

固定宇宙层级 ℓ，并假设 lem : LEM (ℓ-suc ℓ)。这个假设为相应层级的每个命题提供判定，并始终作为下文构造的显式参数。

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

对整条公式的反射，必须为其语法中各处出现的存在子公式给出答案。本章沿公式递归构造联合封闭条件与序数梯，得到一层，使该公式在其中与整个可构造宇宙中具有相同真值。

证明是结构归纳，它需要该层具备两样东西。在无界量词处，需要上一章的闭包，针对该量词自己的矩阵。在有界量词处，需要那个界落在该层里，好让落在界内的一切也落在其中；那正是分离那一章早已会满足的常元条件。

没有哪个针对单一矩阵的极限能同时覆盖全部矩阵，因为闭包不为更大的层所继承：把层扩大，就有更多环境需要它处理。因此这架梯要联合构造：每一级的步进沿公式的结构进行，把其中每个矩阵的单矩阵步进合并起来，连同包含常元的那一层。于是极限对每个矩阵都给出回答，上一章的论证施于其中每一个即可，无须重做。

英文原文

lint-agda: keep (⊤̇ names the defining formula behind LsetS)

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅ )

open hPropView 𝒮ʟ 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σ τ = ⊤*
Answers (t ≐ u)  σ oσ τ = ⊤*
Answers (φ ∧̇ ψ)  σ oσ τ = Answers φ σ oσ τ × Answers ψ σ oσ τ
Answers (φ ∨̇ ψ)  σ oσ τ = Answers φ σ oσ τ × Answers ψ σ oσ τ
Answers (φ ⇒̇ ψ)  σ oσ τ = Answers φ σ oσ τ × Answers ψ σ oσ τ
Answers ⊥̇        σ oσ τ = ⊤*
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 σ (λ _ → ⊤*)
  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ₙ 0        = ∅
Gₙ (suc N)     = jstep (Gₙ N) (Gₙ-ord N) .fst
Gₙ-ord 0    = ∅-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) (γ : Vec S m) → Below β γ
                → ⟨ (lookup i γ) .fst ∈ Lset β ⟩
  lookupInLayer zero    (a ∷ γ) (ha , _)  = ha
  lookupInLayer (suc i) (a ∷ γ) (_  , hγ) = lookupInLayer i γ hγ

  tmInLayer : ∀ {m} (t : Term S m) (γ : Vec S m) → Below β γ
            → BoundedTm (Below′ β) t → ⟨ (⟦ t ⟧ γ) .fst ∈ 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′ β) χ
          → (γ : Vec S m) → Below β γ → (γ ⊨ χ) ≡ (γ ⊨ᴬ χ)

private
  reflect∃ : ∀ {m} (χ : Formula S (suc m)) → ClosedFor β χ
           → ((N : ℕ) → Answers χ (Gₙ N) (Gₙ-ord N) (Gₙ (suc N)))
           → BoundedFo (Below′ β) χ
           → (γ : Vec S m) → Below β γ → (γ ⊨ (∃̇ χ)) ≡ (γ ⊨ᴬ (∃̇ χ))
  reflect∃ χ cl an bd γ bγ = ⇔toPath fwd bwd
    where
    fwd : ⟨ γ ⊨ (∃̇ χ) ⟩ → ⟨ γ ⊨ᴬ (∃̇ χ) ⟩
    fwd ex = map₁
      (λ { (q , (fq∈ , satq)) →
           q , (fq∈ , subst ⟨_⟩ (reflectFo χ an bd (q ∷ γ) (fq∈ , bγ)) satq) })
      (cl γ bγ ex)
    bwd : ⟨ γ ⊨ᴬ (∃̇ χ) ⟩ → ⟨ γ ⊨ (∃̇ χ) ⟩
    bwd = 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′ β) χ
           → (γ : Vec 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 (FOL.Semantics.decideSatisfaction 𝒮ʟ id lem (x ∷ γ) χ)
      where
      decide : Dec ⟨ (x ∷ γ) ⊨ χ ⟩
             → ⟨ (x ∷ γ) ⊨ χ ⟩
      decide (yes sat) = sat
      decide (no nsat) = rec₁ (((x ∷ γ) ⊨ χ) .snd) collide
        (cl γ bγ ∣ x , (λ sat → lift (nsat sat)) ∣₁)
        where
        collide : Σ[ q ∶ S ] (⟨ q .fst ∈ Lset β ⟩ × ⟨ (q ∷ γ) ⊨ (¬̇ χ) ⟩)
                → ⟨ (x ∷ γ) ⊨ χ ⟩
        collide (q , (fq∈ , refute)) = ⊥₀-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β : ⟨ (⟦ t ⟧ γ) .fst ∈ 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β : ⟨ (⟦ t ⟧ γ) .fst ∈ Lset β ⟩
  tInβ = tmInLayer t γ bγ (bd .fst)
  fwd : ⟨ γ ⊨ (∃̇∈ t χ) ⟩ → ⟨ γ ⊨ᴬ (∃̇∈ t χ) ⟩
  fwd = map₁ (λ { (x , (x∈t , h)) → x , (x∈t , subst ⟨_⟩
    (reflectFo χ an (bd .snd) (x ∷ γ) (transβ x∈t tInβ , bγ)) h) })
  bwd : ⟨ γ ⊨ᴬ (∃̇∈ t χ) ⟩ → ⟨ γ ⊨ (∃̇∈ t χ) ⟩
  bwd = map₁ (λ { (x , (x∈t , h)) → x , (x∈t , subst ⟨_⟩
    (sym (reflectFo χ an (bd .snd) (x ∷ γ) (transβ x∈t tInβ , bγ))) h) })

反射定理

把这次归纳与相对化的正确性复合，就把有界读法变回一次寻常的满足，只不过对象是相对化后的公式。这是便于使用的形式：右侧是 Δ₀ 的，故任意复杂度的公式已被换成一条有界公式加一个被明确指出的层。

整理成定理后，它接受一条公式和调用方要求包含在层中的任意序数，并返回一个包含该序数的层。这个额外序数不可省略：证书不会由较大层继承，所以调用方不能事后扩大层，以容纳自己已有的集合。调用方必须预先说明需要包含什么，联合步进会把这一要求一同带入构造。

这个包被封装起来，而这是本书至此最要紧的一次封装。若是透明的，它所命名的层会在每一级上一路展开到联合步进、界层引理与排中律；而凡在类型中提到该层的使用者，都会把那整次展开带进每一次转换检查，两个使用者恰恰都在类型中提到它，于是下一章根本无法完成。封装之后，那一层只是一个名字，使用者向它索取的四样东西，正是这个包已经陈述的四样。

reflectRel : (γ : Vec 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 β ]
                (⟨ δ ∈ β ⟩
                 × ((γ : Vec 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 的良序。

任意公式的反射

作为元素的层

层对公式的义务

联合步骤

联合梯

归纳

反射定理

小结