---
title: "以横截集实现选择"
module: L.Choice.Transversal
lang: zh
site: "Bedrock"
description: "以横截集实现选择"
stage: "典范良序与选择公理"
reading_order: 84
canonical: https://bedrock.institute/zh/L.Choice.Transversal.html
html: L.Choice.Transversal.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/Transversal.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.ZFModel, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Axioms.Basic, L.Choice.FirstIntersectionStage, L.Choice.StageOrders, L.Choice.InternalWellOrder, L.Coding.Model, L.WellOrder.Base]
routes: [choice-completion]
translations: [https://bedrock.institute/en/L.Choice.Transversal.md, https://bedrock.institute/ja/L.Choice.Transversal.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 以横截集实现选择

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

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

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

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

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

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; _∧̇_; ¬̇_; ∃̇_ )
import FOL.ZFModel
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset→isL )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Choice.FirstIntersectionStage {ℓ} lem using ( bound-below₂ )
open import L.Choice.StageOrders {ℓ} lem using ( Mem; relOf )
open import L.Choice.InternalWellOrder {ℓ} lem using ( module Bound )
open import L.Coding.Model {ℓ} using ( appC; appC-adequate )
open import L.WellOrder.Base {ℓ-suc ℓ}
  using ( SWO; IsLeast; isPropLeastOf; leastOf )

open import Cubical.Data.Sigma using ( Σ≡Prop )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )

open hPropStructure 𝒮ʟ

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 秒。原因是此前较慢的描述内部含有已编码语法，在具体环境中求满足关系会正规化完整的层级描述；这里的公式只包含四个原子和一次应用，没有大型定义可展开。封装仍予保留，以维持统一接口，并避免后续使用者重新评估这一边界。

<details class="localized-fallback" lang="en">
<summary lang="zh">英文原文</summary>

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.

</details>

```agda
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` 完成最后这步比较。

```agda
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 (fst a) (snd a)

  β : 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 = fst m , Lset→isL β oβ (fst m) (snd m)

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

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

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

    least : (x : S) → ⟨ x ∈ˢ a ⟩ → Σ[ m ∈ Mem (Lset β) ] IsLeast W (Cell x) m
    least x x∈a = leastOf W lem (Cell x) (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 ℓ} Empty.⊥))

    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 → Empty.⊥
      noPredecessor (w , (w∈x , hap)) = mini (fst w , hw) w∈x lt
        where
        hw : ⟨ fst w ∈ Lset β ⟩
        hw = bound-below₂ (fst a) (snd a) (fst x) (fst w) w∈x x∈a
        hpr : ⟨ pr (fst w) (fst z) ∈ fst rel ⟩
        hpr = subst ⟨_⟩ (appC-adequate rel zero (suc (suc zero)) (w ∷ x ∷ z ∷ [])) hap
        lt : relOf W (fst w , hw) (fst z , hz)
        lt = B.orderL-rep (fst w , hw) (fst z , hz) hpr

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

    pick-out : (z : S) → ⟨ (z ∷ []) ⊨ Pick a rel ⟩ → Out z
    pick-out z = PT.rec PT.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 : ⟨ fst z ∈ Lset β ⟩
        hz = bound-below₂ (fst a) (snd a) (fst x) (fst z) z∈x x∈a

        mini : (b : Mem (Lset β)) → ⟨ Cell x b ⟩
             → relOf W b (fst z , hz) → Empty.⊥
        mini b b∈x lt = lower (neg ∣ elt b , (b∈x , hap) ∣₁)
          where
          hpr : ⟨ pr (fst b) (fst z) ∈ fst rel ⟩
          hpr = B.orderL-fill b (fst z , 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) → ⟨ fst z ∈ 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 = snd (subst ⟨_⟩ (csp z) h)

  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₀ (snd m) (pick-in x x∈a z₀ (snd m , lm))) (fst lm)

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

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

          lz' : IsLeast W (Cell x) (fst z , hz)
          lz' = subst (λ y → IsLeast W (Cell y) (fst z , 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 → snd (w ∈ˢ (transversalSet ∩ x)))
        (Σ≡Prop (λ v → snd (isL v)) (same z h)))

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

## 定理

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

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

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

```agda
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 结构装配起来。