完整的分离与替换

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

有界分离能够形成由 Δ₀ 公式定义的可构造子集，但分离模式允许任意一阶公式。本章先在一个包含待分离集合的层上反射一条指定公式，以此弥合两者之间的差距；随后把函数性关系在源集合上的所有值置于同一层，再用刚得到的完整分离收集它们，从而证明完整替换。本章证明的正是这两个公式模式字段；完整的 ZF 与 ZFC record 留待后文装配。

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

唯一的经典参数是宿主层原理 LEM。在指定的宇宙层级上，它对每个命题返回证明或反驳。它不是宿主层选择公理，也不给出从任意一族命题截断存在中选取见证的操作；它还不同于后文在集合论模型内部解释的选择公理。

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

固定 lem : LEM (ℓ-suc ℓ)。本模块的一切构造都相对于这一条宿主层假设。数学结论是可构造模型中适用于任意一阶公式的分离模式与替换模式；此处既不假设也不证明对象理论的选择公理。对排中律的依赖来自下文所用的最早层与公式反射定理：前者判定是否仅仅存在更小的合格层，后者在无界全称量词的反向判定矩阵是否成立。

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

论证需要在句法与语义之间往返。Formula S n 的元素是有 n 个变元位置、常元取自 S 的对象语言公式，con 把这样的常元放入公式。改名改变变元读取的环境位置，并带有相应的满足关系定理。相对化把每个无界量词改为由选定常元约束的量词，Δ₀-relativize 则从公式结构证明结果是有界公式。原公式与相对化公式的一致来自反射，而不是单凭这次句法变换。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( con; Formula; ∃̇∈ )
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
open import FOL.Manipulation.Relativization using ( relativize; Δ₀-relativize )
import FOL.Absoluteness

这套语言有两种结构解释。外围的累积层级结构 𝒮ᵥ 解释 V ℓ 中的所有集合；𝒮ʟ 的元素则是配有可构造性证明的集合。对指标 β，Lset β 是相应的可构造层；它的层证明给出传递性，而序数指标之间的严格隶属关系使 Lset-mono 可以把成员关系提升到更高层。对每个可构造集，stage 给出包含它的最小序数层指标，以及序数性与成员关系的证明。本章只使用后两项事实，不使用极小性本身。

import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; Lset; Lset-layer; layer-trans; Lset-mono )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )

有界分离与反射共同搭起通往任意公式的桥梁。对有界的一元公式，separateΔ₀ 构造具有所需成员的唯一可构造集。对一条任意公式 φ 和一个序数 δ，mkReflect 产生满足 δ ∈ β 的序数 β，并在条目落于 Lset β 的环境上认同 φ 与其相对化。这只是针对指定公式与参数的反射，并不声称 Lset β 是初等子模型。对于替换，FunctionalImage 给出一个序数层，容纳每个与某个 x ∈ˢ a 相关的 y；LsetS 则把该层表示成对象语言常元。

open import L.Axioms.Separation {ℓ} lem
  using ( module FunctionalImage; separateΔ₀ )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.FormulaReflection {ℓ} lem using ( mkReflect )

若干宿主层构造使语义等同成为精确的路径。⇔toPath 把命题值真值之间的双向蕴含变成路径，随后函数外延性便可从逐点路径认同两个谓词。hProp 中的索引存在经过命题截断。在替换证明中，PT.rec 只把这种存在消去到另一个命题，PT.map 则在不把见证带出命题截断的前提下变换见证。这两种操作都不会全局选定一个源。

open import Cubical.Data.Unit using ( tt* )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )

𝒮ʟ 的载体 S 由 V ℓ 中的底层集合及其可构造性证明组成。其相等与隶属关系只考察底层集合，因此 x ∈ˢ a 给出后文配合层传递性使用的外围隶属。对象语言公式以这一载体为论域，所以它们的常元与环境条目都保留了留在模型内部所需的可构造性证书。

open hPropStructure 𝒮ʟ

对宿主层谓词 Q : S → hProp (ℓ-suc ℓ)，SetOf Q 是如下配对的类型：一个模型元素 b，以及逐点路径 (x ∈ˢ b) ≡ Q x。因此，isContr (SetOf Q) 表达强的唯一存在：其中心给出一个实际的实现集合，其收缩则把每个其他实现者与该中心认同。即使 Q 由对象语言公式的满足关系构成，它仍是宿主层函数。从中心作投影只是取出已有数据，不使用摹状原理。

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )

绝对性构造为同一套句法给出 𝒮ᵥ 中的外围读法与 𝒮ʟ 中的内层读法；这里把内层关系 _⊨ᵐ_ 政名为 _⊨_。因此，γ ⊨ φ 本身是一个宿主层命题，断言对象语言公式 φ 在有限环境 γ 下于可构造结构中为真；不能把它混同于把任意宿主层谓词代入句法。

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

为了比较后文使用的两种变元次序，这里在 𝒮ʟ 上实例化改名语义，并以恒等函数解释常元。Ren.Agrees 逐点断言：经改名的变元位置与另一环境中的对应位置读出同一条目。一旦给出这种一致，Ren.⊨-rename 就把改名公式的满足关系与原公式在重排环境中的满足关系认同起来。

module Ren = Sat 𝒮ʟ id

两件小工具

第一条局部引理记录底层集合上的传递性。若 x ∈ y 且 y ∈ Lset β，则 x ∈ Lset β，因为每个可构造层都是传递集。这里的变元属于 V ℓ；该引理并不构造 x 的可构造性证明。后文使用它时，x : S 已经自带这份证明，而 transIn 只补出反射所需的层成员关系。

private
  transIn : (β : V ℓ) {x y : V ℓ} → ⟨ x ∈ y ⟩ → ⟨ y ∈ Lset β ⟩ → ⟨ x ∈ Lset β ⟩
  transIn β = layer-trans (Lset-layer β)

替换对同一条二元公式使用两种环境次序。在模型的陈述中，(y ∷ x ∷ []) ⊨ φ 把像 y 放在零号槽，把源 x 放在一号槽。存在量词绑定源之后，其主体却在 (x ∷ y ∷ []) 中求值，新绑定的源位于零号槽。函数 swap 恰好交换 Fin 2 的这两个位置，并不反转数学关系。

  swap : Fin 2 → Fin 2
  swap zero    = suc zero
  swap (suc _) = zero

把公式改名用于 swap，便得到 swapFo。若 φ 预期像在零号位置、源在一号位置，那么 swapFo φ 就可以在源居首的环境中求值。这只是自由位置的句法重排；其语义依据另由改名正确性给出。

  swapFo : Formula S 2 → Formula S 2
  swapFo = renameFo swap

对具体元素 x 与 z，两个环境在这次换位下逐点一致。在零号位置，swap 从 x ∷ z ∷ [] 读出第二项 z；在一号位置则读出 x。因此，两条所需路径都直接计算为 refl，这就完整证明了二元环境所需的 Ren.Agrees。

  swapAgrees : (x z : S) → Ren.Agrees swap (x ∷ z ∷ []) (z ∷ x ∷ [])
  swapAgrees x z zero       = refl
  swapAgrees x z (suc zero) = refl

改名正确性现在给出替换所需的精确语义转换：(x ∷ z ∷ []) ⊨ swapFo φ 与 (z ∷ x ∷ []) ⊨ φ 是同一个命题。把 x 读作源、z 读作像时，左边是有界存在量词产生的次序，右边是模型要求的像在前次序。这条路径可借通常的运输双向使用。

  ⊨-swap : (φ : Formula S 2) (x z : S)
         → ((x ∷ z ∷ []) ⊨ swapFo φ) ≡ ((z ∷ x ∷ []) ⊨ φ)
  ⊨-swap φ x z = Ren.⊨-rename swap φ (x ∷ z ∷ []) (z ∷ x ∷ []) (swapAgrees x z)

分离

完整分离量化每条一元对象语言公式 φ : Formula S 1，不带有界性假设。其目标说：存在唯一的模型集合，其成员恰是既属于 a 又满足 φ 的元素 x。证明先把有界分离用于相对化后的公式，再沿 sym Q≡ 运输实现者的整个可缩类型。因此，唯一性来自 separateΔ₀，无需在反射之后重新证明。

hasSeparationL : (a : S) (φ : Formula S 1)
               → isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)))
hasSeparationL a φ =
  subst (λ Q → isContr (SetOf Q)) (sym Q≡)
    (separateΔ₀ a (relativize c φ) (Δ₀-relativize c φ))

先把参数 a 放到将要使用反射的层之下。其底层集合的最早层指标是 sa，stage-ord 证明该指标为序数。以 sa 为输入对 φ 应用 mkReflect，得到序数 β、严格隶属关系 sa ∈ β，以及对每个落在 Lset β 中的环境，φ 与其相对化的满足命题之间的路径。此时把 sa 传入构造十分关键：反射层从一开始就被构造成包含该指标，而不是事后再扩张。

  where
  sa  = stage (fst a) (a .snd)
  R   = mkReflect φ sa (stage-ord (fst a) (a .snd))
  β   = R .fst
  oβ  = R .snd .fst

指标 β、底层集合 Lset β 与模型元素 c 是三个不同的对象。利用证明 oβ : IsOrd β，项 LsetS β oβ 由该层及其可构造性证明构成元素 c : S。这恰是 relativize 所需的形式：新量词的界是对象语言常元，因此该层必须在模型内部表示，不能只作为外围集合使用。

  c   = LsetS β oβ

现在可把参数放入反射层。stage-mem 给出 fst a ∈ Lset sa，而反射数据给出严格的序数隶属 sa ∈ β。可构造层级的单调性把二者合成，得到 fa∈β : fst a ∈ Lset β。这并未把 a 与序数认同：sa 和 β 是指标，fst a 才是被放入更高层的集合。

  fa∈β : ⟨ fst a ∈ Lset β ⟩
  fa∈β = Lset-mono {α = β} {β = sa} (R .snd .snd .fst)
           (stage-mem (fst a) (a .snd))

反射只适用于条目落在 Lset β 中的环境，因此分离谓词中的成员合取项不可缺少。给定 x ∈ˢ a，传递性把该事实与 fa∈β 合起来，得到 fst x ∈ Lset β；tt* 则给出单元素环境空尾部的平凡条件。于是，R 的反射分量给出 bridge，即 φ 在 x 处的满足关系与其相对化的满足关系之间的路径。对于 a 外的任意 x : S，这里不作比较。

  bridge : (x : S) → ⟨ x ∈ˢ a ⟩
         → ((x ∷ []) ⊨ φ) ≡ ((x ∷ []) ⊨ relativize c φ)
  bridge x x∈a = R .snd .snd .snd (x ∷ []) (transIn β x∈a fa∈β , tt*)

最后要比较两个宿主层谓词。在每个方向上，共同的成员证明 x ∈ˢ a 都被原样保留，只有满足关系的证明沿 bridge 或其逆向运输。⇔toPath 把这两个映射变成 x 处两个命题值之间的路径，funExt 再把逐点路径合成为 Q≡。这只是谓词的相等；此处既不消去存在的命题截断，也不对候选集合作外延性论证。

  Q≡ : (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ))
     ≡ (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ relativize c φ))
  Q≡ = funExt (λ x → ⇔toPath
    (λ { (x∈a , h) → x∈a , subst ⟨_⟩ (bridge x x∈a) h })
    (λ { (x∈a , h) → x∈a , subst ⟨_⟩ (sym (bridge x x∈a)) h }))

诸像所在的层

对每个 x ∈ˢ a，假设都使相关值的依值和 Σ y , (y ∷ x ∷ []) ⊨ φ 可缩。其中心给出一个值，收缩则把每个相关值与该中心认同，所以这一步不使用宿主层选择公理。FunctionalImage 遍历小表示 ⟪ fst a ⟫；它为每个小指标所表示成员的中心取最早层，再由 boundingOrd 用一个序数 βimg 界住所有这些层。给定任意成员 x ∈ˢ a，∈-asFiber 返回一个小指标，以及该指标的表示值与 x 的底层集合相等的路径。沿此路径可把关系搬到该指标所表示的源，再由可缩性把所选中心与每个相关的 y 认同，并沿这一相等搬运公共层界。这一构造中的最早层操作仍依赖 lem，但不使用选择公理。

module Images (a : S) (φ : Formula S 2)
              (fc : (x : S) → ⟨ x ∈ˢ a ⟩
                  → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩)) where
  open FunctionalImage a (λ x y → (y ∷ x ∷ []) ⊨ φ) fc public

替换

hasReplacementL 的假设使 a 的每个成员之上的值纤维可缩，而其结论使实现像谓词的模型集合所成之类型可缩。这是两种不同的唯一性：前者为每个源给出唯一的值，后者给出恰好收集所有这些值的唯一集合。像谓词中的源存在经过命题截断，只记录源的存在而不暴露一个选定的源。opaque 边界只改变 Agda 的定义性化归，既不改变这个陈述，也不增添假设。

opaque
  hasReplacementL : (a : S) (φ : Formula S 2)
                → ((x : S) → ⟨ x ∈ˢ a ⟩
                     → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩))
                → isContr (SetOf (λ y → ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ)))

替换证明现在已有恰好两项所需材料。由逐点可缩纤维，Images 给出一个序数层，容纳与 a 的成员相关的每个值。在该层上把完整分离用于一元公式 imageFo，便得到实现 BoundedImage 的集合所成的可缩类型。下文证明的路径 Q≡ 将这一谓词认同于不带层条件的像谓词 Image；因此沿 sym Q≡ 运输，就得到所要求的可缩类型 SetOf Image。这正是任意公式 φ 的完整替换，而不是对前一章有界替换定理的调用。

稍后，L.Model 把 hasSeparationL 与 hasReplacementL 用作 L⊨ZF 十二个字段中的两个。只有在这份 ZF record 装配完成之后，hasChoiceL L⊨ZF 才给出组成 L⊨ZFC 所需的对象理论选择字段。此处 lem : LEM (ℓ-suc ℓ) 是经典的宿主层假设，fc 则是定理明列的逐点唯一存在假设。从 fc 已经携带的中心作投影不需要宿主层选择公理；后文的选择字段是所得结论，并非本证明的前提。

  hasReplacementL a φ fc =
    subst (λ Q → isContr (SetOf Q)) (sym Q≡)
      (hasSeparationL (LsetS βimg βimg-ord) imageFo)
    where
    open Images a φ fc

替换所要求的谓词直接采用模型公理中的变元次序。候选者 y 属于 Image，当且仅当存在某个 x ∈ˢ a，使 φ 在环境 y ∷ x ∷ [] 中成立，其中像在前，源在后。hProp 中的索引存在采用命题截断：它保留适当的源存在这一事实，却忘去具体使用了哪个源。因此，SetOf Image 的可缩性表示恰有一个模型集合以这些像为成员，并不表示像集本身只有一个成员。

    Image : S → hProp (ℓ-suc ℓ)
    Image y = ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ)

要用分离得到同一条件，须先把它表达成一元对象语言公式。在 imageFo 中，有界存在量词遍历常元 a 的成员；引入源见证 x 后，公式体在环境 x ∷ y ∷ [] 中求值。由于 φ 预期的是 y ∷ x ∷ []，公式体取为 swapFo φ，而 ⊨-swap 证明这次位置交换保持原来要表达的关系。只有新添的这一个存在量词受 a 约束；φ 仍可含无界量词，所以 imageFo 未必是 Δ₀ 公式，必须由完整分离处理。

    imageFo : Formula S 1
    imageFo = ∃̇∈ (con a) (swapFo φ)

完整分离施于表示公共层的模型集合之内，所以它实现的谓词含有两个条件。第一项把 y 放入 Lset βimg，第二项断言 y 满足 imageFo。第一个合取项是分离所带来的论域条件，并不表示公式的每个量词都有界。对真正的像值而言，这一条件是多余的，因为 range∈βimg 已把所有像值放进公共层。余下的证明说明，添加或去掉这项层条件都不改变像谓词的外延。

    BoundedImage : S → hProp (ℓ-suc ℓ)
    BoundedImage y = (y ∈ˢ LsetS βimg βimg-ord) ⊓ ((y ∷ []) ⊨ imageFo)

相等 Q≡ 由逐点论证得到。对每个候选者 y，into y 与 out y 给出 Image y 和 BoundedImage y 之间的两个方向；⇔toPath 把它们化为命题值之间的路径，funExt 再把这些逐点路径合成谓词的相等。正向从经过命题截断的源开始。此处 PT.rec 可以考察这样的见证，因为它的目标是 BoundedImage y 的底层命题，snd (BoundedImage y) 正是对此的证明。见证只在这个命题目标内部使用，不能作为未截断的数据返回。

    Q≡ : Image ≡ BoundedImage
    Q≡ = funExt (λ y → ⇔toPath (into y) (out y))
      where
      into : (y : S) → ⟨ Image y ⟩ → ⟨ BoundedImage y ⟩
      into y = PT.rec (snd (BoundedImage y)) λ { (x , (x∈a , h)) →

在这次合法的命题消去内部，设源为 x，并有证明 x ∈ˢ a 与 (y ∷ x ∷ []) ⊨ φ。值域定理 range∈βimg 把 y 放入公共层，从而给出第一个合取项。对于第二个合取项，同一个 x 被重新包入命题截断。沿路径 ⊨-swap φ x y 的反向运输，把 φ 在 y ∷ x ∷ [] 中的满足变为 swapFo φ 在 x ∷ y ∷ [] 中的满足，后者恰是 imageFo 的公式体。因此，这个分支构造出 BoundedImage y 的两个部分，却没有从命题截断中取出一个源作为结果。

        range∈βimg x x∈a y h
        , ∣ x , (x∈a , subst ⟨_⟩ (sym (⊨-swap φ x y)) h) ∣₁ }

反向蕴含直接丢弃层成员关系这一分量。imageFo 的满足已经在命题截断之下包含一个源 x、它属于 a 的证明，以及 swapFo φ 在 x ∷ y ∷ [] 中成立的证明。PT.map 把同一个源及其成员证明保留在命题截断内部，同时沿 ⊨-swap φ x y 运输，把最后一项变为 φ 在 y ∷ x ∷ [] 中的满足；所得正是 Image y。它与正向蕴含共同证明 Q≡，而定义等式开头的运输则把完整分离得到的集合变为完整替换所要求的唯一集合。这次比较没有选出任何见证。

      out : (y : S) → ⟨ BoundedImage y ⟩ → ⟨ Image y ⟩
      out y (_ , h) = PT.map (λ { (x , (x∈a , h')) →
        x , (x∈a , subst ⟨_⟩ (⊨-swap φ x y) h') }) h

小结

完整分离与完整替换来自两次归约。先在包含源集合的层内环境上反射指定公式，把它的真假化为其 Δ₀ 相对化公式的真假；有界分离随即给出完整分离。逐点可缩的值纤维、源集合的小表示与序数定界再把每个相关值置于同一层，完整分离于是能够收集像并给出完整替换。两项结果都保留唯一的经典参数 LEM (ℓ-suc ℓ)，且不使用宿主层选择公理。后文会用它们填入 L⊨ZF 的分离与替换字段；本章本身不装配完整的 ZF 或 ZFC record。