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

交互式目录 · 依赖图

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

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

本章证明 𝒮ʟ 的选择公理：在循阶的内部良序下，从每一格分离出最小元素，并证明所得集合与每个两两不交的格恰交于一点。

本章证明选择公理在 𝒮ʟ 处的实例，采用模型 record 的横截形式：给定一个元素非空且两两不交的集合，则仅仅存在一个集合，与原集合的每个元素恰交于一点。

论证与经典证法相同，只是其中最费力的那一步已经在此前完成：教科书把宇宙良序化，再取每一格中最小的元素。L 整体的良序是真类上的关系，本书从未构造过它；前几章构造出来的，是每个层上的良序，且是一致地构造的，并在每个序数处都作为模型的一个元素。这就够了，因为集合是小的：单个序数就能同时界住一个族、它的元素与它们的元素，而在该序数处的塔之内，选取不过是一次普通的极小元搜索。

于是本章只有四步。上界：层一章为该族给出的上界序数高于该族自身的层，因而高于它每个元素的每个元素。那里的序：取该序数处表中的关系，它是模型的一个元素，另有两条引理把对它的成员关系与元层面的比较双向读通。那条描述：「该族的某个元素含有这个集合，且那个元素中没有任何东西排在它之前」，这是以那个序为常元的公式，本章的模型据它用分离得到一个集合。计数：该集合与每个元素恰交于一点，存在性来自极小元，唯一性来自两两不交；这正是两两不交假设的用途，也是全书唯一用到它的地方。

本章除四步之外还有一句观察。选择是相对于此载体上的一个 ZF 模型陈述的，因为它所点名的交是该模型的派生运算；而这份依赖的全部内容，就是沿交的规格作一次改写。

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

open hPropView 𝒮ʟ

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

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

那条描述

Pick 是一条单自由变元公式，断言该点属于族的某个元素，且在选定关系下，该元素中没有点排在它之前。

一条公式，一个自由变元，两个常元。它对一个集合 z 说：该族的某个元素含有 z，且那个元素中没有任何东西在那个序下排在 z 之前。应用原子直接把那个序当作常元。族也直接点名，因为它只出现在一条成员关系原子之下。

该公式仍在构造之处封装，因为常元上的描述原则上应在定义处保持不透明。不过，这一选择在本章不影响检查时间：封装与不封装都需 2.3 秒。原因是此前较慢的描述内部含有已编码语法，在具体环境中求满足关系会正规化完整的层级描述；这里的公式只包含四个原子和一次应用，没有大型定义可展开。封装仍予保留，以维持统一接口，并避免后续使用者重新评估这一边界。

英文原文

Perf: sealed by the standing law (a description read at constants), though measured here at 2.3 s either way: this description names no coded syntax.

opaque
  Pick : S → S → Formula S 1
  Pick c r =
    ∃̇ ( (var zero ∈̇ con c)
      ∧̇ ( (var (suc zero) ∈̇ var zero)
        ∧̇ (¬̇ ∃̇ ( (var zero ∈̇ var (suc zero))
               ∧̇ appC r zero (suc (suc zero)) )) ) )

横截集

在上界层之内，极小元搜索为每一格选出一点；分离把这些点收集成集，而不交性证明每次相交中的唯一性。

本模块固定下供应交运算的那个 ZF 模型、那个族，以及该族的两条假设。选择构造的层部分在该族自身处供应上界与序：β 是一个高于该族自身层的序数，从而高于它的元素及其元素，也高于诸名字所住的 ω；W 是 β 处塔的诸元素上的良序；而 rel 就是同一个序作为模型的一个元素，正是这一点才使它能在描述中被一个常元点名。

Cell x 是那些元素之上「是 x 的元素」这条谓词，而 least 把 L.WellOrder.Base 的泛型搜索施于它。同一搜索此前已用于有穷层序与名字选取，后面还用于 GCH 构造；它在此处的具体职责，是把层序变成每一格的一个选定代表。这正是借助排中律才能为横截集完成的选取。

pick-in 与 pick-out 是那条描述的两条读式，而两者互不为对方的推论：一条由极小元造出一个满足关系，另一条由满足关系取出一个极小元，且各自都要把一个集合在它可被呈现的两种形态之间转换，即作为 L 的元素与作为 β 处塔的元素。两个截断载荷分别名为 Two 与 Predecessor，于是两条读式都不必把嵌套写开；否定式是唯一一处把截断消去到空类型的地方，而它是在一个具名辅助件里消去的。

随后进行分离与计数。transversalSet 是模型中的分离，依照该描述施于 β 处的塔。Cut 固定族中的一个元素：交的收缩中心就是相应极小元；由 pick-in，它属于横截集，而极小性本身保证它属于该元素。唯一性在这里使用两两不交：交中的另一点满足描述，因而是族中某个元素的极小元，同时又属于当前元素；两个元素因此相交并相等，所以该点也是当前元素的极小元。极小元由三歧唯一，泛型定理 isPropLeastOf 完成最后这步比较。

module Trans (zf : isZFModel) (a : S)
             (inh : (x : S) → ⟨ x ∈ˢ a ⟩ → ∥ Σ[ y ∶ S ] ⟨ y ∈ˢ x ⟩ ∥₁)
             (disj : (x y : S) → ⟨ x ∈ˢ a ⟩ → ⟨ y ∈ˢ a ⟩
                   → ∥ Σ[ z ∶ S ] (⟨ z ∈ˢ x ⟩ × ⟨ z ∈ˢ y ⟩) ∥₁ → x ≡ y)
             where

open ModelL.isZFModel zf using ( separate; separate-spec; _∩_; ∩-spec )
private module B = Bound (a .fst) (a .snd)

β : V ℓ
β = B.boundOrd

oβ : IsOrd β
oβ = B.boundOrd-ord

W : SWO (Mem (Lset β))
W = B.boundOrder

rel : S
rel = B.orderL

elt : Mem (Lset β) → S
elt m = m .fst , Lset→isL β oβ (m .fst) (m .snd)

Cell : S → Mem (Lset β) → hProp (ℓ-suc ℓ)
Cell x m = m .fst ∈ x .fst

CellFormula : S → Formula S 1
CellFormula x = var zero ∈̇ con x

definedCell : (x : S)
            → FOL.Semantics.FormulaPredicate 𝒮ʟ (Mem (Lset β)) S id (Cell x)
definedCell x = FOL.Semantics.presented 1 (CellFormula x)
  (λ m → elt m ∷ []) (λ m → refl)

Least : S → S → Type (ℓ-suc ℓ)
Least x z = Σ[ h ∶ ⟨ z .fst ∈ Lset β ⟩ ] IsLeast W (Cell x) (z .fst , h)

private
  members : (x : S) → ⟨ x ∈ˢ a ⟩ → ∥ Σ[ m ∶ Mem (Lset β) ] ⟨ Cell x m ⟩ ∥₁
  members x x∈a = map₁ atMember (inh x x∈a)
    where
    atMember : Σ[ y ∶ S ] ⟨ y ∈ˢ x ⟩ → Σ[ m ∶ Mem (Lset β) ] ⟨ Cell x m ⟩
    atMember (y , y∈x) =
      (y .fst , bound-below₂ (a .fst) (a .snd) (x .fst) (y .fst) y∈x x∈a) , y∈x

  least : (x : S) → ⟨ x ∈ˢ a ⟩ → Σ[ m ∶ Mem (Lset β) ] IsLeast W (Cell x) m
  least x x∈a = leastOfFormula W (definedCell x) lem (members x x∈a)

  Predecessor : S → S → S → Type (ℓ-suc ℓ)
  Predecessor x z w = ⟨ w ∈ˢ x ⟩
                    × ⟨ (w ∷ x ∷ z ∷ []) ⊨ appC rel zero (suc (suc zero)) ⟩

  Two : S → S → Type (ℓ-suc ℓ)
  Two x z = ⟨ x ∈ˢ a ⟩
          × (⟨ z ∈ˢ x ⟩
            × (∥ Σ[ w ∶ S ] Predecessor x z w ∥₁
               → Lift {j = ℓ-suc ℓ} ⊥₀))

  Out : S → Type (ℓ-suc ℓ)
  Out z = ∥ Σ[ x ∶ S ] (⟨ x ∈ˢ a ⟩ × Least x z) ∥₁

opaque
  unfolding Pick

  pick-in : (x : S) → ⟨ x ∈ˢ a ⟩ → (z : S) → Least x z
          → ⟨ (z ∷ []) ⊨ Pick a rel ⟩
  pick-in x x∈a z (hz , (z∈x , mini)) =
    ∣ x , (x∈a , (z∈x , neg)) ∣₁
    where
    noPredecessor : Σ[ w ∶ S ] Predecessor x z w → ⊥₀
    noPredecessor (w , (w∈x , hap)) = mini (w .fst , hw) w∈x lt
      where
      hw : ⟨ w .fst ∈ Lset β ⟩
      hw = bound-below₂ (a .fst) (a .snd) (x .fst) (w .fst) w∈x x∈a
      hpr : ⟨ pr (w .fst) (z .fst) ∈ rel .fst ⟩
      hpr = subst ⟨_⟩ (appC-adequate rel zero (suc (suc zero)) (w ∷ x ∷ z ∷ [])) hap
      lt : relOf W (w .fst , hw) (z .fst , hz)
      lt = B.orderL-rep (w .fst , hw) (z .fst , hz) hpr

    neg : ∥ Σ[ w ∶ S ] Predecessor x z w ∥₁
        → Lift {j = ℓ-suc ℓ} ⊥₀
    neg q = lift (rec₁ isProp⊥ noPredecessor q)

  pick-out : (z : S) → ⟨ (z ∷ []) ⊨ Pick a rel ⟩ → Out z
  pick-out z = rec₁ squash₁ atTwo
    where
    atTwo : Σ[ x ∶ S ] Two x z → Out z
    atTwo (x , (x∈a , (z∈x , neg))) =
      ∣ x , (x∈a , (hz , (z∈x , mini))) ∣₁
      where
      hz : ⟨ z .fst ∈ Lset β ⟩
      hz = bound-below₂ (a .fst) (a .snd) (x .fst) (z .fst) z∈x x∈a

      mini : (b : Mem (Lset β)) → ⟨ Cell x b ⟩
           → relOf W b (z .fst , hz) → ⊥₀
      mini b b∈x lt = lower (neg ∣ elt b , (b∈x , hap) ∣₁)
        where
        hpr : ⟨ pr (b .fst) (z .fst) ∈ rel .fst ⟩
        hpr = B.orderL-fill b (z .fst , hz) lt
        hap : ⟨ (elt b ∷ x ∷ z ∷ []) ⊨ appC rel zero (suc (suc zero)) ⟩
        hap = subst ⟨_⟩
          (sym (appC-adequate rel zero (suc (suc zero)) (elt b ∷ x ∷ z ∷ []))) hpr

transversalSet : S
transversalSet = separate (LsetS β oβ) (Pick a rel)

private
  csp : (z : S) → (z ∈ˢ transversalSet)
                ≡ ((z ∈ˢ LsetS β oβ) ⊓ ((z ∷ []) ⊨ Pick a rel))
  csp = separate-spec (LsetS β oβ) (Pick a rel)

  inC : (z : S) → ⟨ z .fst ∈ Lset β ⟩ → ⟨ (z ∷ []) ⊨ Pick a rel ⟩
      → ⟨ z ∈ˢ transversalSet ⟩
  inC z hL hp = subst ⟨_⟩ (sym (csp z)) (hL , hp)

  outC : (z : S) → ⟨ z ∈ˢ transversalSet ⟩ → ⟨ (z ∷ []) ⊨ Pick a rel ⟩
  outC z h = (subst ⟨_⟩ (csp z) h) .snd

module Cut (x : S) (x∈a : ⟨ x ∈ˢ a ⟩) where

private
  m : Mem (Lset β)
  m = least x x∈a .fst

  lm : IsLeast W (Cell x) m
  lm = least x x∈a .snd

  z₀ : S
  z₀ = elt m

  inMeet : (z : S) → ⟨ z ∈ˢ transversalSet ⟩ → ⟨ z ∈ˢ x ⟩
         → ⟨ z ∈ˢ (transversalSet ∩ x) ⟩
  inMeet z hc hx = subst ⟨_⟩ (sym (∩-spec transversalSet x z)) (hc , hx)

  outMeet : (z : S) → ⟨ z ∈ˢ (transversalSet ∩ x) ⟩
          → ⟨ z ∈ˢ transversalSet ⟩ × ⟨ z ∈ˢ x ⟩
  outMeet z h = subst ⟨_⟩ (∩-spec transversalSet x z) h

  centre : Σ[ z ∶ S ] ⟨ z ∈ˢ (transversalSet ∩ x) ⟩
  centre = z₀ , inMeet z₀
    (inC z₀ (m .snd) (pick-in x x∈a z₀ (m .snd , lm))) (lm .fst)

  same : (z : S) → ⟨ z ∈ˢ (transversalSet ∩ x) ⟩ → z .fst ≡ m .fst
  same z h = rec₁ (setIsSet (z .fst) (m .fst)) atOut
               (pick-out z (outC z ((outMeet z h) .fst)))
    where
    z∈x : ⟨ z ∈ˢ x ⟩
    z∈x = (outMeet z h) .snd

    atOut : Σ[ x' ∶ S ] (⟨ x' ∈ˢ a ⟩ × Least x' z) → z .fst ≡ m .fst
    atOut (x' , (x'∈a , (hz , lz))) =
      cong (λ p → (p .fst) .fst)
        (isPropLeastOf W (Cell x) ((z .fst , hz) , lz') (m , lm))
      where
      x≡x' : x ≡ x'
      x≡x' = disj x x' x∈a x'∈a ∣ z , (z∈x , lz .fst) ∣₁

      lz' : IsLeast W (Cell x) (z .fst , hz)
      lz' = subst (λ y → IsLeast W (Cell y) (z .fst , hz)) (sym x≡x') lz

meetsOnce : isContr (Σ[ z ∶ S ] ⟨ z ∈ˢ (transversalSet ∩ x) ⟩)
meetsOnce = centre , atPoint
  where
  atPoint : (p : Σ[ z ∶ S ] ⟨ z ∈ˢ (transversalSet ∩ x) ⟩) → centre ≡ p
  atPoint (z , h) = sym (Σ≡Prop
    (λ w → (w ∈ˢ (transversalSet ∩ x)) .snd)
    (Σ≡Prop (λ v → (isL v) .snd) (same z h)))

transversal : (x : S) → ⟨ x ∈ˢ a ⟩
            → isContr (Σ[ z ∶ S ] ⟨ z ∈ˢ (transversalSet ∩ x) ⟩)
transversal = Cut.meetsOnce

定理

最后的封装把横截集构造转成 𝒮ʟ 上 ZF 模型 record 所要求的选择字段。

ChoiceStatement 就是前沿先前持有的那条陈述，原样移到此处，并在此处被证出：模型的选择字段在 𝒮ʟ 处的样子，是相对于此载体上的一个 ZF 模型而言的，因为那个交是该模型的派生运算。hasChoiceL 给出证明。根章把它施于正在装配的那个模型自身，这正是这条陈述一开始就要对模型作全称的原因。

这一行给出根定理所用的选择字段。它仍相对于正在装配的 ZF 模型陈述，因为交是该模型的派生运算。

ChoiceStatement : isZFModel → Type (ℓ-suc ℓ)
ChoiceStatement zf =
  (a : S)
  → ((x : S) → ⟨ x ∈ˢ a ⟩ → ∥ Σ[ y ∶ S ] ⟨ y ∈ˢ x ⟩ ∥₁)
  → ((x y : S) → ⟨ x ∈ˢ a ⟩ → ⟨ y ∈ˢ a ⟩
       → ∥ Σ[ z ∶ S ] (⟨ z ∈ˢ x ⟩ × ⟨ z ∈ˢ y ⟩) ∥₁ → x ≡ y)
  → ∥ Σ[ c ∶ S ] ((x : S) → ⟨ x ∈ˢ a ⟩
       → isContr (Σ[ z ∶ S ] ⟨ z ∈ˢ (c ∩ x) ⟩)) ∥₁
  where open ModelL.isZFModel zf using ( _∩_ )

hasChoiceL : (zf : isZFModel) → ChoiceStatement zf
hasChoiceL zf a inh disj = ∣ T.transversalSet , T.transversal ∣₁
  where module T = Trans zf a inh disj

小结

Pick、循阶的层序与分离共同造出横截集；它与每个元素恰交于一点，这一性质给出 hasChoiceL。

Pick 是那条描述：该族的某个元素含有这个集合，且那个元素中没有任何东西排在它之前。pick-in 与 pick-out 是它相对于「是某个元素的极小元」的两个方向的读式。transversalSet 是模型以它为据、用分离在该族上界序数处的塔上得到的集合；transversal 则算出它与每个元素之交：恰为一点，存在性来自那场极小元搜索，唯一性来自两两不交。hasChoiceL 就是模型的选择字段；有了它，前沿即告清空并被移除。

一次实测，结果是这条定律在此处没有发挥作用。读在常元上的描述要在被造出之处封印，这条定律在其被发现之处带来了九十九倍的差别；在此处则全无影响：封印与否都是 2.3 秒，因为这条描述不携带任何已编码的语法。封印仍然保留，那个数字也仍被记下，好让这条定律保持它本来的内容：它关乎一条描述包含什么，而不关乎它在哪里被读。

本书是为了什么

完成的 Choice 构造链补上了最后缺少的模型字段，故在唯一明示的排中律假设下，可构造宇宙满足 ZFC。

这是 Choice 构造链的终点，故值得把已确立的结论平白说一遍。在 cubical Agda 之内，给定模型自身真值层级上的一份排中律，可构造宇宙是 ZFC 的模型。与环境层级满足 ZF 的结果合读，这就是哥德尔的选择公理相对一致性的语义形式：满足 ZF 的宇宙内部含有一个满足 ZFC 的子宇宙，故 ZFC 的任何矛盾都早已是 ZF 的矛盾。

这里把代价明确写出。宿主是带宇宙塔的 cubical Agda，其强度非形式地约当于 ZFC 加一个不可达基数；排中律是模块参数而非公理，且是这条定理携带的唯一假设；本开发中处处没有公设、没有留空。本章给出选择公理字段，L.Model 再把它与此前的 ZF 结构装配起来。