Bedrock以横截集实现选择
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图本章证明 𝒮ʟ 的选择公理：在循阶的内部良序下，从每一格分离出最小成员，并证明所得集合与每个两两不交的格恰交于一点。
本章证明选择公理在 𝒮ʟ 处的实例，采用模型 record 的横截形式：给定一个成员非空且两两不交的集合，则仅仅存在一个集合，与原集合的每个成员恰交于一点。
论证与经典证法相同，只是其中最费力的那一步已经在此前完成：教科书把宇宙良序化，再取每一格中最小的成员。L 整体的良序是真类上的关系，本书从未构造过它；前几章构造出来的，是每个层上的良序，且是一致地构造的，并在每个序数处都作为模型的一个元素。这就够了，因为集合是小的：单个序数就能同时界住一个族、它的成员与它们的成员，而在该序数处的塔之内，选取不过是一次普通的极小元搜索。
于是本章只有四步。上界：层一章为该族给出的上界序数高于该族自身的层，因而高于它每个成员的每个成员。那里的序：取该序数处表中的关系，它是模型的一个元素，另有两条引理把对它的隶属与元层面的比较双向读通。那条描述：「该族的某个成员含有这个集合，且那个成员中没有任何东西排在它之前」，这是以那个序为常元的公式，本章的模型据它用分离得到一个集合。计数：该集合与每个成员恰交于一点，存在性来自极小元，唯一性来自两两不交；这正是两两不交假设的用途，也是全书唯一用到它的地方。
本章除四步之外还有一句观察。选择是相对于此载体上的一个 ZF 模型陈述的，因为它所点名的交是该模型的派生运算；而这份依赖的全部内容，就是沿交的规格作一次改写。
{-# 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 秒。原因是此前较慢的描述内部含有已编码语法，在具体环境中求满足关系会正规化完整的层级描述；这里的公式只包含四个原子和一次应用，没有大型定义可展开。封装仍予保留，以维持统一接口，并避免后续使用者重新评估这一边界。
英文原文
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 (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 模型陈述，因为交是该模型的派生运算。
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 结构装配起来。