可构造层级的序列

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

阅读指南 · 依赖地图

本章用函数图描述逐次取可定义幂集所得的层，刻画该函数的部分逼近，并封装后面用来识别可构造层级初始段的图。

在这条路线上，塔是唯一一个没法照满足关系那场递归的办法内化的构造。一个图不可以点名它所定义的对象，而塔在某一层处是由该层以下的塔造出来的，故直接为塔写下的图将不得不点名它自己在诸子实参处的取值。它没有可点名的取值。

能说出口的是逼近是什么。函数 f 是层级在 a 上的一个逼近，当它恰好定义在 a 的诸成员上，且它所记录的每个取值都是「在那个实参处、由 f 自身算出的那一步」。那一步只在实参以下查阅 f，故这个条件永不查看该函数尚未记录的取值，而塔自己在 a 处的取值就是「由这样一个 f 所得的那一步」。这是一条序列刻画，而它是一个只谈 f 的一阶句子。

本章中的每个槽位都由变元表示。逼近由图中唯一的存在量词绑定，实参与取值是图的两个自由变元，整个描述不含任何具名常元，因此可以放在层级所需的位置，即持有层的那层绑定之下。下面每条读式也都在变元环境中陈述，理由与前两章相同：若在具体环境中解除充分性，环境的构造会进入满足关系，使同一陈述的检查时间从几秒增加到几分钟。

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; _⇒̇_; ∃̇_; ∀̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; 𝒟ₒ )
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; domAt; domAt-in; domAt-out; prAtL; prAtL-adequate )
open import L.Coding.Expressions {ℓ} using ( extAt; extAt-out; extAt-in; extAt-in-both )
open import L.Coding.DefinablePowerSet {ℓ} lem using ( DefAt; DefAt-in; DefAt-out )

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )

open hPropStructure 𝒮ʟ

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

后继层关系

StepAt v b f 表示 v 是 f 定义域中的后继实参，并且 f 在该处的取值是其在前驱 b 处取值的可定义幂集。Records、StepOf 与 PowOK 分别揭示该陈述的三个部分。

v 是 b 处的层 (给定 b 以下的逼近 f)，当 v 的诸成员恰是「落在 f 于 b 中某个实参处所记录的某个取值的可定义幂集之中」的那些集合。这个陈述体现于三个相邻的存在量词：那个实参 c、逼近在其处所记录的取值 w，以及该取值的可定义幂集 d。幂集必须被绑定，因为上一章给出的只是关于它的一条描述、而不是指称它的一个词项；DefAt 说的是 d 是 w 的可定义幂集，故使用它的唯一办法就是对它所描述的那个东西作量化。

整一步是一次 extAt，这是一项设计决定，并非为了省事。层是一个集合，而凡取值为集合的递归，其每一条子句说的都是同一句话：这个取值恰是满足某个条件的那些东西之集。若手写成一对包含，那个条件就要出现两次、每条包含之下各一次，于是那三个存在量词被复制一份，此后对它们的每一次改动都得在两处各做一遍，而每一种读法都得由「互非逆」的两半重新拼起来。extAt 把条件只写一次，并把两种读法作为投影给出，它的意义正在于此。

这一步带有一个旁条件，而同一条假设在两个方向上都能解除它。要满足这条描述，必须把可定义幂集作为模型的元素给出，因为对象语言的存在量词在 L 上取值；要把描述读回来，则需要使用 DefAt 的消去方向，其旁条件是「载体的诸可定义子集皆可构造」。前者蕴含后者：若 𝒟ₒ w 是 L 的元素，则由该类的传递性，它的诸成员皆可构造。因此，两个方向需要的是同一项假设 PowOK；在某一层使用它时，后继恒等式会解除这项条件。

private
  sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n))))
  sh4 i = suc (suc (suc (suc i)))

StepBody : ∀ {n} → Fin n → Fin n → Formula S (suc (suc (suc (suc n))))
StepBody b f = (var (suc (suc zero)) ∈̇ var (sh4 b))
             ∧̇ ( appAt (sh4 f) (suc (suc zero)) (suc zero)
               ∧̇ ( DefAt zero (suc zero)
                 ∧̇ (var (suc (suc (suc zero))) ∈̇ var zero) ) )

StepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
StepAt v b f = extAt v (∃̇ (∃̇ (∃̇ (StepBody b f))))

Records : ∀ {n} → Fin n → Fin n → S ^ n → S → S → Type (ℓ-suc ℓ)
Records b f γ c w = ⟨ fst c ∈ fst (lookup b γ) ⟩
                  × ⟨ pr (fst c) (fst w) ∈ fst (lookup f γ) ⟩

StepOf : ∀ {n} → Fin n → Fin n → S ^ n → S → Type (ℓ-suc ℓ)
StepOf b f γ z = Σ[ c ∈ S ] Σ[ w ∈ S ]
                   (Records b f γ c w × ⟨ fst z ∈ 𝒟ₒ (fst w) ⟩)

PowOK : ∀ {n} → Fin n → Fin n → S ^ n → Type (ℓ-suc ℓ)
PowOK b f γ = (c w : S) → Records b f γ c w → ⟨ isL (𝒟ₒ (fst w)) ⟩

读取并构造层级步骤

StepAt-out 从已满足的步骤中提取可定义幂集条件，StepAt-in 从该条件及所需定义域数据构造满足关系。StepAt-back 以后续证明所用的形式保留提取出的条件。

读体是消去那三个存在量词之处，下面每一次 PT.rec 都明确写出自身载荷的类型。这是上一章已经采用的规则，并非文风选择：若交给推断，载荷会成为一个元变元，表示「某条公式的满足关系」，而消解器尚未确定是哪条公式；同样两行代码的检查时间便会从两秒增加到两分钟以上。

装配体则是把同样三个存在量词填上。可定义幂集由 PowOK 所提供的那个模型元素给出，它自己的编码等式在那个元素处是 refl，而 DefAt 的引入别无所需。这一步的诸读法于是就是 extAt 的诸方向：把那两半插进去；而它们有三条而非两条，StepAt-out 把这一步的一个成员读作一份载荷，StepAt-back 把一份载荷放回去，而 StepAt-in 由两个方向一并造出这一步，因为一个以外延造出的集合，必须从两侧逐成员地重新进入。读体与装配体为三者所共用，故每个投影都只有一行。

module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) where
  private
    Φ : Formula S (suc n)
    Φ = ∃̇ (∃̇ (∃̇ (StepBody b f)))

    readBody : PowOK b f γ → (z c w d : S)
             → ⟨ (d ∷ w ∷ c ∷ z ∷ γ) ⊨ StepBody b f ⟩ → StepOf b f γ z
    readBody ok z c w d (hb , (ha , (hd , hz))) =
      c , w , rec , subst (λ X → ⟨ fst z ∈ X ⟩) qd hz
      where
英文原文

Perf: env spelled out at both ends; via an abbreviation, 15 s per conversion.

      rec : Records b f γ c w
      rec = hb , subst ⟨_⟩ (appAt-adequate
        (sh4 f) (suc (suc zero)) (suc zero) (d ∷ w ∷ c ∷ z ∷ γ)) ha

      qd : fst d ≡ 𝒟ₒ (fst w)
      qd = DefAt-out w zero (suc zero) (d ∷ w ∷ c ∷ z ∷ γ)
        (λ x x∈ → isL-trans {x = 𝒟ₒ (fst w)} {y = x} x∈ (ok c w rec)) refl hd

    unfold : PowOK b f γ → (z : S)
           → ⟨ (z ∷ γ) ⊨ Φ ⟩ → ∥ StepOf b f γ z ∥₁
    unfold ok z = PT.rec squash₁ viaArg
      where
      viaPow : (c w : S)
             → Σ[ d ∈ S ] ⟨ (d ∷ w ∷ c ∷ z ∷ γ) ⊨ StepBody b f ⟩
             → ∥ StepOf b f γ z ∥₁
      viaPow c w (d , hd) = ∣ readBody ok z c w d hd ∣₁

      viaVal : (c : S)
             → Σ[ w ∈ S ] ⟨ (w ∷ c ∷ z ∷ γ) ⊨ ∃̇ (StepBody b f) ⟩
             → ∥ StepOf b f γ z ∥₁
      viaVal c (w , hw) = PT.rec squash₁ (viaPow c w) hw

      viaArg : Σ[ c ∈ S ] ⟨ (c ∷ z ∷ γ) ⊨ ∃̇ (∃̇ (StepBody b f)) ⟩
             → ∥ StepOf b f γ z ∥₁
      viaArg (c , hc) = PT.rec squash₁ (viaVal c) hc

    fill : PowOK b f γ → (z : S) → StepOf b f γ z → ⟨ (z ∷ γ) ⊨ Φ ⟩
    fill ok z (c , (w , (rec , hz))) =
      ∣ c , ∣ w , ∣ D , (rec .fst , (ha , (hdef , hz))) ∣₁ ∣₁ ∣₁
      where
英文原文

Perf: env spelled out at both ends; via an abbreviation, 15 s per conversion.

      D : S
      D = 𝒟ₒ (fst w) , ok c w rec

      ha : ⟨ (D ∷ w ∷ c ∷ z ∷ γ) ⊨ appAt (sh4 f) (suc (suc zero)) (suc zero) ⟩
      ha = subst ⟨_⟩ (sym (appAt-adequate
        (sh4 f) (suc (suc zero)) (suc zero) (D ∷ w ∷ c ∷ z ∷ γ))) (rec .snd)

      hdef : ⟨ (D ∷ w ∷ c ∷ z ∷ γ) ⊨ DefAt zero (suc zero) ⟩
      hdef = DefAt-in w zero (suc zero) (D ∷ w ∷ c ∷ z ∷ γ) refl refl

  StepAt-out : ⟨ γ ⊨ StepAt v b f ⟩ → PowOK b f γ
             → (z : S) → ⟨ fst z ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ z ∥₁
  StepAt-out h ok z z∈ = unfold ok z (extAt-out v Φ γ h z z∈)

  StepAt-back : ⟨ γ ⊨ StepAt v b f ⟩ → PowOK b f γ
              → (z : S) → StepOf b f γ z → ⟨ fst z ∈ fst (lookup v γ) ⟩
  StepAt-back h ok z s = extAt-in v Φ γ h z (fill ok z s)

  StepAt-in : PowOK b f γ
            → ((z : S) → ⟨ fst z ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ z ∥₁)
            → ((z : S) → StepOf b f γ z → ⟨ fst z ∈ fst (lookup v γ) ⟩)
            → ⟨ γ ⊨ StepAt v b f ⟩
  StepAt-in ok into back = extAt-in-both v Φ γ
    (λ z z∈ → PT.rec (snd ((z ∷ γ) ⊨ Φ)) (fill ok z) (into z z∈))
    (λ z h → PT.rec (snd (fst z ∈ fst (lookup v γ))) (back z) (unfold ok z h))

层级序列的逼近

ApproxAt f a 描述一个定义域为序数 a 的函数：它具有指定初值，且每个后继处的取值都由 StepAt 关联。GraphAt 以存在量词封装这类函数，其读取引理则揭示定义域、取值与步骤方程。

两个合取项，没有第三个。f 定义在 a 上，且 f 所记录的每个取值都是「在那个实参处、由 f 自身算出的那一步」。第二个合取项无须加上「实参落在 a 中」这一限制：第一个合取项已经在两个方向上把定义域限制为 a，故凡记录了东西的实参都是 a 的成员，再说一遍只会把句子拉长。

这一对是一条隶属等价，而这比看上去更要紧。若反过来陈述为「对 a 中的每个实参，仅仅存在一个取值是那里的那一步」，这句话就容许 f 在正确的对之外还带有多余的对，故它并不确定 f，那条存在性断言不是命题，而针对它的归纳需要一条内部的函数外延性引理，才能从两个逼近得到一个。作为等价，动机是命题，而那条引理根本无须写下。

此处刻意没有单值性合取项。它断言不出第二个合取项尚未给出的任何东西：若在同一个实参处记录了两个取值，则两者都是那个实参处的那一步，而那一步是一条集合等式，同成员的两个集合相等。若加上它，等于拿三个置于满足关系之下的全称量词去换一条推论。

这三个投影就是使用这些定义的人要问的三个问题：有条目的实参在定义域中、定义域中的实参有条目、被记录的取值是一步。把引入放在此处而不放在调用处，理由与每一条读式相同：它解除一次充分性，而那必须在变元环境上做。

private
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)

module RecShape (Step : ∀ {n} → Fin n → Fin n → Fin n → Formula S n) where

  Domain₀ : S → V ℓ → Type (ℓ-suc ℓ)
  Domain₀ h B = (c z : S) → ⟨ pr (fst c) (fst z) ∈ fst h ⟩ → ⟨ fst c ∈ B ⟩

  ApproxAt : ∀ {n} → Fin n → Fin n → Formula S n
  ApproxAt f a = domAt f a
               ∧̇ ∀̇ (∀̇ ( appAt (sh2 f) (suc zero) zero
                       ⇒̇ Step zero (suc zero) (sh2 f) ))

  GraphAt : ∀ {n} → Fin n → Fin n → Formula S n
  GraphAt w b = ∃̇ (ApproxAt zero (suc b) ∧̇ Step (suc w) (suc b) zero)

  module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) where
    ApproxAt-dom : ⟨ γ ⊨ ApproxAt f a ⟩ → Domain₀ (lookup f γ) (fst (lookup a γ))
    ApproxAt-dom h = domAt-out f a γ (h .fst)

    ApproxAt-value : ⟨ γ ⊨ ApproxAt f a ⟩ → (c : S)
                   → ⟨ fst c ∈ fst (lookup a γ) ⟩
                   → ∥ (Σ[ z ∈ S ] ⟨ pr (fst c) (fst z) ∈ fst (lookup f γ) ⟩) ∥₁
    ApproxAt-value h = domAt-in f a γ (h .fst)

    ApproxAt-step : ⟨ γ ⊨ ApproxAt f a ⟩ → (c z : S)
                  → ⟨ pr (fst c) (fst z) ∈ fst (lookup f γ) ⟩
                  → ⟨ (z ∷ c ∷ γ) ⊨ Step zero (suc zero) (sh2 f) ⟩
    ApproxAt-step h c z p = h .snd c z
      (subst ⟨_⟩ (sym (appAt-adequate (sh2 f) (suc zero) zero (z ∷ c ∷ γ))) p)

    ApproxAt-in : ⟨ γ ⊨ domAt f a ⟩
                → ((c z : S) → ⟨ pr (fst c) (fst z) ∈ fst (lookup f γ) ⟩
                   → ⟨ (z ∷ c ∷ γ) ⊨ Step zero (suc zero) (sh2 f) ⟩)
                → ⟨ γ ⊨ ApproxAt f a ⟩
    ApproxAt-in hd hs = hd , λ c z p → hs c z
      (subst ⟨_⟩ (appAt-adequate (sh2 f) (suc zero) zero (z ∷ c ∷ γ)) p)

  module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where
    GraphOf : Type (ℓ-suc ℓ)
    GraphOf = Σ[ f ∈ S ] ( ⟨ (f ∷ γ) ⊨ ApproxAt zero (suc b) ⟩
                         × ⟨ (f ∷ γ) ⊨ Step (suc w) (suc b) zero ⟩ )

    Graph-in : (f : S) → ⟨ (f ∷ γ) ⊨ ApproxAt zero (suc b) ⟩
             → ⟨ (f ∷ γ) ⊨ Step (suc w) (suc b) zero ⟩ → ⟨ γ ⊨ GraphAt w b ⟩
    Graph-in f ha hs = ∣ f , (ha , hs) ∣₁

    Graph-out : ⟨ γ ⊨ GraphAt w b ⟩ → ∥ GraphOf ∥₁
    Graph-out h = h

  PairGraphAt : ∀ {n} → Fin n → Fin n → Formula S n
  PairGraphAt e c = ∃̇ (prAtL (suc e) (suc c) zero ∧̇ GraphAt zero (suc c))

  module _ {n : ℕ} (e c : Fin n) (γ : S ^ n)
           (φ : Formula S n) (qφ : φ ≡ PairGraphAt e c) where
    PairOf : Type (ℓ-suc ℓ)
    PairOf = Σ[ z ∈ S ] ( (fst (lookup e γ) ≡ pr (fst (lookup c γ)) (fst z))
                        × ⟨ (z ∷ γ) ⊨ GraphAt zero (suc c) ⟩ )

    PairGraph-in : (z : S) → fst (lookup e γ) ≡ pr (fst (lookup c γ)) (fst z)
                 → ⟨ (z ∷ γ) ⊨ GraphAt zero (suc c) ⟩ → ⟨ γ ⊨ φ ⟩
    PairGraph-in z q hg = subst (λ ψ → ⟨ γ ⊨ ψ ⟩) (sym qφ)
      ∣ z , (subst ⟨_⟩
        (sym (prAtL-adequate (suc e) (suc c) zero (z ∷ γ))) q , hg) ∣₁

    PairGraph-out : ⟨ γ ⊨ φ ⟩ → ∥ PairOf ∥₁
    PairGraph-out h = PT.map
      (λ { (z , (hq , hg)) →
        z , (subst ⟨_⟩ (prAtL-adequate (suc e) (suc c) zero (z ∷ γ)) hq , hg) })
      (subst (λ ψ → ⟨ γ ⊨ ψ ⟩) qφ h)

open RecShape StepAt public renaming ( GraphAt to LsetGraphAt
                                     ; Graph-in to LsetGraph-in
                                     ; Graph-out to LsetGraph-out )

层级逼近之图

PairGraphAt 识别由序数实参与逼近在该处所赋取值组成的有序对。最后的图公式恰好汇集这些有序对，把逐点逼近变成表示层级序列的集合。

在逼近上有一个存在量词，其下是本章为之而写的两个合取项：f 是那个实参上的一个逼近，而那个取值是「在那个实参处、由 f 算出的那一步」。取值排在第一位，实参排在第二位，这正是模型的替换字段读一个图时所用的顺序；LsetGraph 就是把这两个分量填好之后的那个句子。

逼近被绑定，而且必须如此。一个图不可以点名它所定义的对象；且仅当某物已知是 L 的元素时，它才可以断言该物存在，因为满足关系是在模型处读的。逼近正是这样：它是由较低的诸实参经替换收集起来的对之集，而不是它所描述的那座塔。消费方提供一个逼近，而图只断言存在一个。

两种读法各只一行，因为被满足的存在量词就是一个截断的 sigma，被满足的合取就是一个对。它们带来的不是证明，而是那个名字与那个分量：GraphOf 把载荷的类型写了出来，不交给推断；两种读法都占据一个变元环境的变元位，故消费方是去实例化它们，而不是与它们作转换。

命名是本节的全部代价，这个数字值得留存，因为对它的第一次诊断是错的。若把图以它那个闭句别名来称呼，同样两行占掉了本章 130 秒中的 98 秒。当初被怪罪的是那两个分量，而它们是清白的：下一章一次隔离测量把「读式落在完全具体的位上」量到十五毫秒，把「同一条读式对着一个别名」量到五十一秒。真正耗时的是「判定别名的满足关系与它展开式的满足关系相等」，而 Agda 解决它的办法，是把一个内部装着整条可定义幂集描述的满足关系正规化。落在变元位上，诸读式根本不会遇到这个问题，而那个闭句只差一次展开。

小结

所得集合编码图记录直到某个序数界为止的逐次可构造层，其中步骤关系已经由后续内部描述所需的可定义幂集公式表达。

LsetGraph 是对象语言中「取值是实参处的层」这个句子，写下来时不点名任何层、任何塔、任何序数。StepAt 是一次 extAt 罩住三个相邻的存在量词，即那个实参、在其处所记录的取值，以及它的可定义幂集；ApproxAt 是两个合取项，即定义域与那条步进条件，再无其他。

此处没有任何东西被证两遍。可定义幂集以「落在一位上的描述」的形式来自上一章，并按既有形式直接使用；函数机器从 appAt 与 domAt 上读出；而那一步的两种读法就是 extAt 自己的那两个。本章所贡献的是形状：一个查阅逼近而非查阅塔的图，而那是一个图被允许拥有的唯一形状。

有两条裁定被记录在读者与之相遇之处。那一步是一条隶属等价，而非一个单向的收集，这使即将到来的那场归纳的动机保持为命题，并把一条内部的函数外延性引理整个从证明路线中省去。此外，没有单值性合取项，因为步进条件已经唯一确定了「在一个实参处记录的每个取值」，故单值性是一条推论，不是一条假设。

一次测量，而紧随本章的下一章更正了它的诊断。本章曾经花掉的每一秒，都是「同一样东西的两种写法」之间的一次转换，而 Agda 每一次都以「把一个内部装着整条可定义幂集描述的满足关系正规化」来应对：两条读法对着图的那个闭句别名而取，98 秒；每一处「假设把环境写开，而应用把它藏在一个缩写背后」，各 15 秒。具体位不涉及那个机制，几乎不耗时。写成两侧是同一个表达式之后，本章在两秒之内、而不是 130 秒检查完毕，数学分毫未改。前几章据以写下的那条规矩，即充分性在变元实参处解除，对一条陈述成立，与它对一次代换成立完全一样。