Reflecting an existential into a stage

分离那一章用量词已然有界的公式雕出阶段的子集，而那是够用的，因为有界公式只问阶段已经装下的东西。无界的存在量词不然：它问的是在 L 的某处是否有见证，而 L 是真类。要用这样的公式来雕，就得在一个集合之内回答一个真类大小的问题。

回答得了，而论证出自 Montague。固定一个矩阵与一个参数环境。若见证根本存在，则有一个包含见证的最小阶段，而那个阶段是对真类大小之问题的集合大小的回答。取遍某一阶段中的全部参数元组，把诸回答界住，所得便是单一阶段，它为下方那个阶段的每个元组作答。沿自然数迭代这一步并取并：极限为它自己的参数作答，因为极限中的任何有穷元组早已落在某个有穷层里，而那一层的回答在下一层被界住。

此处有两件事与通常做法不同。见证的选取正是通常召唤 L 的良序之处，而它并不需要：论证想要的是典范的序数，而非典范的元素，而序数早已被成员关系良序化。故装有见证的最小阶段被直接取用，经阶段那一章的下降，而住在那里的究竟是哪个见证，从未被决定。以及，参数自始就是元组。先写单参数情形、日后再推广，等于把整个构造写两遍，因为它的每一步都对参数有几个漠不关心；元组唯一被感受到的地方是为它定位，那里有穷多个层要合并成一个。

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Truth
open import Base.Classical using ( LEM )

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; ∃̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset-in; Lset-out
        ; Lset→isL )
open import L.Ordinal {ℓ} using ( ∅-ord; boundingOrd; bound2; setUnion-ord )
open import L.Stage {ℓ} lem using ( LeastOrd; leastOrd )

open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Data.Nat using ( _+_; +-comm )
open import Cubical.Data.Unit using ( Unit*; tt* )
import Cubical.Data.Empty as Empty
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Functions.Logic using ( ⇔toPath; ∃[∶]-syntax )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; sett; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ⋃_; union-ax )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ʟ 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 : ℕ} → ⟪ Lset σ ⟫ ^ k → S ^ k
LsetEnv σ oσ []       = []
LsetEnv σ oσ (m ∷ ms) = LsetElt σ oσ m ∷ LsetEnv σ oσ ms

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

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

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

作答的阶段

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

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

Sat : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k) → S → Ω
Sat ψ ρ q = (q ∷ ρ) ⊨ ψ

SatEx : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k) → Ω
SatEx ψ ρ = ∃[ q ∶ S ] Sat ψ ρ q

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

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

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

decideStage : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k)
            → ⟨ SatEx ψ ρ ⟩ ⊎ (⟨ SatEx ψ ρ ⟩ → Empty.⊥) → V ℓ
decideStage ψ ρ (inl sat) = pick ψ ρ sat .fst
decideStage ψ ρ (inr _)   = ∅

pickStage : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k) → V ℓ
pickStage ψ ρ = decideStage ψ ρ (lem (SatEx ψ ρ))

decideStage-ord : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k)
                  (d : ⟨ SatEx ψ ρ ⟩ ⊎ (⟨ SatEx ψ ρ ⟩ → Empty.⊥))
                → IsOrd (decideStage ψ ρ d)
decideStage-ord ψ ρ (inl sat) = pick ψ ρ sat .snd .fst
decideStage-ord ψ ρ (inr _)   = ∅-ord

pickStage-ord : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k)
              → IsOrd (pickStage ψ ρ)
pickStage-ord ψ ρ = decideStage-ord ψ ρ (lem (SatEx ψ ρ))

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

pickWitness : {k : ℕ} (ψ : Formula S (suc k)) (ρ : S ^ k) → ⟨ SatEx ψ ρ ⟩
            → ⟨ Wit ψ ρ (pickStage ψ ρ) ⟩
pickWitness ψ ρ sat = go (lem (SatEx ψ ρ)) refl
  where
  go : (d : ⟨ SatEx ψ ρ ⟩ ⊎ (⟨ SatEx ψ ρ ⟩ → Empty.⊥))
     → lem (SatEx ψ ρ) ≡ d → ⟨ Wit ψ ρ (pickStage ψ ρ) ⟩
  go (inl s) e = subst (λ d → ⟨ Wit ψ ρ (decideStage ψ ρ d) ⟩) (sym e)
                   (pick ψ ρ s .snd .snd .fst)
  go (inr ¬s) e = Empty.rec (¬s sat)

梯与其极限

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

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

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

ClosedFor : (β : V ℓ) {k : ℕ} (ψ : Formula S (suc k)) → Type (ℓ-suc ℓ)
ClosedFor β {k} ψ = (ρ : 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 zero    = 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 = ∈∈ₛ {a = G n} {b = top} .snd
    (union-ax (sett (Lift {ℓ-zero} {ℓ} ℕ) fam) (G n) .snd
      ∣ G (suc n)
      , ( ∈∈ₛ {a = G (suc n)} {b = sett (Lift {ℓ-zero} {ℓ} ℕ) fam} .fst
            ∣ lift (suc n) , refl ∣₁
        , ∈∈ₛ {a = G n} {b = G (suc n)} .fst (G-up n) ) ∣₁)

闭包论证要它的参数落在某一级上，而不只是落在极限之下。对单个参数，两次反演把它送到那里：极限中的序数属于被取并的集合之一，因而属于某一级；而极限之阶段中的集合，按塔的刻画，属于某个更小序数之阶段上的算子，故把那个序数定位、再走「进去」，就把该集合放进了那一级的阶段。

对元组，为各项找到的诸级必须合并，而「够得着」引理合并其中两个：自级 n 与级 m，二者都够得着级 suc (n + m)，一个直接够到，另一个交换加法之后够到。沿元组递归把它们全部合并，而单调性把靠前的诸项抬上去。

  δ∈top→fin : (δ : V ℓ) → ⟨ δ ∈ top ⟩ → ∥ (Σ[ N ∈ ℕ ] ⟨ δ ∈ G N ⟩) ∥₁
  δ∈top→fin δ δ∈ = PT.rec squash₁
    (λ { (v , (v∈ₛsett , δ∈ₛv)) → PT.map
        (λ { (i , Gi≡v) → lower i
           , ∈∈ₛ {a = δ} {b = G (lower i)} .snd
               (subst (λ w → ⟨ δ ∈ₛ w ⟩) (sym Gi≡v) δ∈ₛv) })
        (∈∈ₛ {a = v} {b = sett (Lift {ℓ-zero} {ℓ} ℕ) fam} .snd v∈ₛsett) })
    (union-ax (sett (Lift {ℓ-zero} {ℓ} ℕ) fam) δ .fst
      (∈∈ₛ {a = δ} {b = top} .fst δ∈))

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

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

闭包

一架梯对某矩阵作答，指凡由某级索引出的环境，其作答阶段都落在下一级上。关于梯是怎么造的，闭包论证用到的仅此一条假设，而下一节与下一章各以自己的方式供给它。

有了它，极限对该矩阵闭合。把环境定位到某一级，并在那里为它命名：它是那一级之阶段的某个索引元组的像，至多相差一个等式，而读取引理连同元组一并交还了它。它的作答阶段落在下一级上，故住在作答阶段里的东西便住在那一级的阶段里，因而落在极限之下；两次单调性，再把那个等式搬回去。

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

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

于是有了后续诸章将要消费的定理。对落在极限之下的环境，类模型满足那个存在量词，恰当极限之阶段中有一个见证。正向是闭包，反向是忘掉见证住在哪里。

正向不需要翻译的一步，因为两侧本已是同一个命题：存在量词的语义是沿载体的截断和，而 SatEx 当初就是照这个定义的。故定理是闭包换了个说法，而在语法与元层之间往返，分文未付。

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

    reflect : (ρ : 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 : ⟪ Lset σ ⟫ ^ k)
                                 → ⟨ pickStage ψ (LsetEnv σ oσ ms) ∈ β ⟩))
  Fbnd σ oσ = boundingOrd (⟪ 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

    σ∈Fstep : (σ : V ℓ) (oσ : IsOrd σ) → ⟨ σ ∈ Fstep σ oσ ⟩
    σ∈Fstep σ oσ =
      bound2 (Fbnd σ oσ .fst) σ (Fbnd σ oσ .snd .fst) oσ .snd .snd .snd

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

  βₙ : ℕ → V ℓ
  βₙ-ord : (n : ℕ) → IsOrd (βₙ n)
  βₙ zero        = ∅
  βₙ (suc n)     = Fstep (βₙ n) (βₙ-ord n)
  βₙ-ord zero    = ∅-ord
  βₙ-ord (suc n) = Fstep-ord (βₙ n) (βₙ-ord n)

  βₙ-step : (n : ℕ) → ⟨ βₙ n ∈ βₙ (suc n) ⟩
  βₙ-step n = σ∈Fstep (βₙ n) (βₙ-ord n)

  module L = Ladder βₙ βₙ-ord βₙ-step

  βω : V ℓ
  βω = L.top

  βω-ord : IsOrd βω
  βω-ord = L.top-ord

  answers : (n : ℕ) (ms : ⟪ Lset (βₙ n) ⟫ ^ k)
          → ⟨ pickStage ψ (LsetEnv (βₙ n) (βₙ-ord n) ms) ∈ βₙ (suc n) ⟩
  answers n = pickLand (βₙ n) (βₙ-ord n)

  closed : ClosedFor βω ψ
  closed = L.closure ψ answers

  reflect : (ρ : S ^ k) → Below βω ρ → (ρ ⊨ (∃̇ ψ)) ≡ Wit ψ ρ βω
  reflect = L.reflect ψ answers

小结

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

这个构造用了两次排中律，一次判定可满足性，一次在下降之内，而选择公理一次也没用。这正是取最小阶段而非最小见证的用意：序数自带良序，而此处没有任何东西需要索取 L 的良序。

交付的是一个量词，参数任意多。任意公式有许多量词，因而有许多矩阵，而没有哪个单矩阵极限能同时服务全部；下一章将造一架梯，其步进一举闭合它们全部，并因此白得上面的一切，无须重跑其中任何一步。