存在公式到可构造层的反射

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

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

对一条存在公式以及来自某个可构造层的参数，本章构造一个更大的序数层：只要环境可构造宇宙中存在见证，该层也包含见证。迭代见证选择步骤并取序数极限，可使这一层包含该公式对其中参数所需的见证。

这一构造可以完成，其论证出自 Montague。固定一个矩阵与一个参数环境。若见证存在，就有一个包含见证的最小层，从而以一个集合大小的层控制原本涉及真类的搜索。取遍某一层中的全部参数元组，并为所得各层取一个共同上界，便得到单一层，其中包含下方层每个元组所需的见证。沿自然数迭代这一步并取并，所得极限也具有相同性质：极限中的任何有穷元组早已属于某个有穷层，而该层所需见证的层在下一层已被界住。

此处有两点与通常做法不同。通常会在选择见证时使用 L 的良序，而这里并不需要：论证所需的是典范的序数，而非典范的元素，并且序数已经由成员关系良序化。因此，可由讨论层的一章的下降论证直接取包含见证的最小层，而不指定其中究竟是哪一个见证。此外，参数从一开始就是元组。若先处理单参数情形再作推广，就要把整个构造写两遍，因为构造的每一步都不依赖参数的个数；只有在定位元组时需要考虑这一点，并把有穷多个层合并成一个。

open import Cubical.Data.Nat using ( +-comm )

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; sett; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ⋃_ )

open hPropView 𝒮ʟ using ( S )

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

取自一层的环境

参数取自层的索引集，索引元组则给出环境：层的一个元素经塔的成员关系判据成为类模型的一个元素。正是这一点使下面的界层引理得以适用：诸元组构成周遭大小的类型，因为它正是其上的向量。

一个环境落在某层之下，指它的每一项都落在其下。从这样的环境读回索引元组是逆向的操作，且同时给出等式，因为构造需要知道：它所界定的环境正是输入的那一个。等式正是用到「可构造性是命题」之处：模型的两个元素，只要底集相同就相等。

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 : ℕ} → Vec (⟪ Lset σ ⟫) k → Vec S k
LsetEnv σ oσ []       = []
LsetEnv σ oσ (m ∷ ms) = LsetElt σ oσ m ∷ LsetEnv σ oσ ms

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

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

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

作答层

固定一个矩阵，其中含一个见证变元与 k 个参数。「这个环境的某个见证落在该层里」是序数的一条性质，故讨论层的那一章的下降直接适用于它。它的前提是某个序数具有该性质，而这仅凭可满足性即得：见证是 L 的元素，而 L 的元素按定义落在某一层里。

其次，全函数性要求即便见证不存在也得有个值，而排中律给出分情形。一如讨论层的那一章，分情形由显式的辅助函数而非 with 作出，因为下面那条承重引理必须点名同一个判定值并在其上匹配。

Sat : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k) → S → hProp (ℓ-suc ℓ)
Sat ψ ρ q = (q ∷ ρ) ⊨ ψ

SatEx : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k) → hProp (ℓ-suc ℓ)
SatEx ψ ρ = ∃[ q ∶ S ] Sat ψ ρ q

satExDecision : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k)
              → Dec ⟨ SatEx ψ ρ ⟩
satExDecision ψ ρ = FOL.Semantics.decideSatisfaction 𝒮ʟ id lem ρ (∃̇ ψ)

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

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

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

decideStage : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k)
            → Dec ⟨ SatEx ψ ρ ⟩ → V ℓ
decideStage ψ ρ (yes sat) = pick ψ ρ sat .fst
decideStage ψ ρ (no _)    = ∅

pickStage : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k) → V ℓ
pickStage ψ ρ = decideStage ψ ρ (satExDecision ψ ρ)

decideStage-ord : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k)
                  (d : Dec ⟨ SatEx ψ ρ ⟩)
                → IsOrd (decideStage ψ ρ d)
decideStage-ord ψ ρ (yes sat) = pick ψ ρ sat .snd .fst
decideStage-ord ψ ρ (no _)    = ∅-ord

pickStage-ord : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k)
              → IsOrd (pickStage ψ ρ)
pickStage-ord ψ ρ = decideStage-ord ψ ρ (satExDecision ψ ρ)

最后是整个构造所倚赖的那条性质：若环境根本可满足，则它的作答层确实装着一个见证。证明必须知道判定走的是哪一支，而它问不出来，因为判定是排中律的一个值，没有东西算得出它。于是它做那件标准的事：对分支作量化，记住「该分支就是那个判定」这条等式，并沿之搬运。在假分支上，假设自我反驳。

pickWitness : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k) → ⟨ SatEx ψ ρ ⟩
            → ⟨ Wit ψ ρ (pickStage ψ ρ) ⟩
pickWitness ψ ρ sat = go (satExDecision ψ ρ) refl
  where
  go : (d : Dec ⟨ SatEx ψ ρ ⟩)
     → satExDecision ψ ρ ≡ d → ⟨ Wit ψ ρ (pickStage ψ ρ) ⟩
  go (yes s) e = subst (λ d → ⟨ Wit ψ ρ (decideStage ψ ρ d) ⟩) (sym e)
                   (pick ψ ρ s .snd .snd .fst)
  go (no ¬s) e = ⊥₀-rec (¬s sat)

梯与其极限

论证真正需要的不是某座特定的塔，而是一架梯：由自然数索引的、上升的序数链。它的极限是并，且是序数，因为序数族之并是序数；每一级都属于极限，因为它属于自己的后继，而后继是被取并的集合之一；而这条链向前够得着，一级属于此后每个严格更晚的级，只需把一步与更晚那级的传递性复合。

把「够得着」的间隔写成显式的加项而非诉诸序关系，正是使两级仅凭加法即可合并的原因。这要紧，因为合并诸级是参数元组所付的唯一代价，而不必为此额外买一套算术。

把梯与塔分开值得费些心思，因为下一章需要一架造法不同的梯：其单步一举闭合一条公式的全部矩阵。以下一切都是关于梯来证的，于是那一章只须造它的梯，便可得到这套论证，而不必重跑一遍。

ClosedFor : (β : V ℓ) {k : ℕ} (ψ : Formula S (suc k)) → Type (ℓ-suc ℓ)
ClosedFor β {k} ψ = (ρ : Vec 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     = 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 = union-family-in (Lift {ℓ-zero} {ℓ} ℕ) fam (lift (suc n)) (G n) (G-up n)

δ∈top→fin : (δ : V ℓ) → ⟨ δ ∈ top ⟩ → ∥ (Σ[ N ∶ ℕ ] ⟨ δ ∈ G N ⟩) ∥₁
δ∈top→fin δ δ∈ = map₁ (λ { (i , h) → lower i , h })
  (union-family-out (Lift {ℓ-zero} {ℓ} ℕ) fam δ δ∈)

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

localize : {j : ℕ} (ρ : Vec S j) → Below top ρ → ∥ (Σ[ N ∶ ℕ ] Below (G N) ρ) ∥₁
localize []      _        = ∣ zero , tt* ∣₁
localize (p ∷ ρ) (h , hs) = rec₁ squash₁
  (λ { (N , h') → map₁ (merge N h') (localize ρ hs) })
  (localize₁ (p .fst) h)
  where
  merge : (N : ℕ) → ⟨ p .fst ∈ 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 ℓ)
     → ⟨ q .fst ∈ Lset σ ⟩ → ⟨ σ ∈ τ ⟩ → ⟨ τ ∈ top ⟩ → ⟨ q .fst ∈ Lset top ⟩
land q σ τ fq∈σ σ∈τ τ∈top =
  Lset-mono {α = top} {β = τ} τ∈top (Lset-mono {α = τ} {β = σ} σ∈τ fq∈σ)

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

closure : ClosedFor top ψ
closure ρ below sat = rec₁ squash₁ atRung (localize ρ below)
  where
  atRung : Σ[ N ∶ ℕ ] Below (G N) ρ → ⟨ Wit ψ ρ top ⟩
  atRung (N , belowN) = map₁ found (pickWitness ψ ρₘ satₘ)
    where
    idx = indexEnv (G N) (G-ord N) ρ belowN
    ρₘ : Vec 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 ] (⟨ q .fst ∈ Lset (pickStage ψ ρₘ) ⟩ × ⟨ Sat ψ ρₘ q ⟩)
          → Σ[ q ∶ S ] (⟨ q .fst ∈ 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 )

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

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

单个母式的步骤

最后是那一步。层的索引集是周遭大小的类型，其上的元组也是，故界层引理适用：取自同一层的全部环境，其作答层有公共上界。把那个上界与该层本身合并，就得到步进，它因而既包含自己的自变量而使迭代得以攀升，又包含自变量的诸环境的每个回答，而后者恰是那条作答假设。

步进被封印。展开来，它是由排中律所造的界再造出的界，而闭包论证反复在诸级上匹配；透明的定义会把那整座塔推进每一次转换检查。三条性质各开封一次，其中最后一条是唯一用到传递性之处，故从回答经上界进入步进的这条链封在印内，调用方只见其结论。

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

Fbnd : (σ : V ℓ) (oσ : IsOrd σ)
     → Σ[ β ∶ V ℓ ] (IsOrd β × ((ms : Vec (⟪ Lset σ ⟫) k)
                               → ⟨ pickStage ψ (LsetEnv σ oσ ms) ∈ β ⟩))
Fbnd σ oσ = boundingOrd (Vec (⟪ 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

  pickLand : (σ : V ℓ) (oσ : IsOrd σ) (ms : Vec (⟪ 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)

小结

一架梯是上升的序数链；它对某矩阵作答，指每一级的环境，其作答层都落在下一级上；而当它作答时，它的极限对该矩阵闭合，reflect 把这一点重述为存在量词的反射。Single 造出单矩阵的步进，办法是界住一层的诸回答，再与该层合并。

这个构造用了两次排中律，一次判定可满足性，一次在下降之内，而选择公理一次也没用。这正是取最小层而非最小见证的用意：序数自带良序，而此处无须用到 L 的良序。

本章的成果是一个量词，可带任意多个参数。任意公式可以含有许多量词，因而有许多矩阵，而没有哪个针对单一矩阵的极限能同时覆盖全部；下一章将构造一架梯，其一次步进同时闭合所有矩阵，并随之直接得到上面的一切，无须对其中任何一步重做论证。