BedrockChoice, and the frontier emptied
最后一笔债。登记簿仍在索取的，是选择公理在 𝒮ʟ 处的实例，且取模型 record 陈述它时所用的横截形式：给定一个集合，其成员非空且两两不交，则仅仅存在一个与它每个成员恰交于一点的集合。
论证的形状就是经典的那个，只是那昂贵的一步早已付讫。教科书把宇宙良序化，再取每一格中最小的成员。L 整体的良序是真类上的关系，本书从未造过一个；前几章造出来的，是每个阶段上的良序，一致地造出，且在每个序数处都作为模型的一个元素。这就够了，因为集合是小的。单个序数一举界住一个族、它的成员与它们的成员，而在那个序数处的塔之内，选取不过是一次普通的极小元搜索。
于是本章只有四步。上界：阶段那一章为该族给出的界层序数，在该族自身的阶段之上，从而在它每个成员的每个成员之上。那里的序：表在那个序数处的关系，作为模型的一个元素，配两条引理把对它的隶属与元层面的比较双向读通。那条描述：「该族的某个成员含有这个集合，且那个成员中没有任何东西排在它之前」，一条以那个序为常量的公式，模型自家的分离据以雕出一个集合。计数：那个集合与每个成员恰交于一点，存在性来自极小元，唯一性来自两两不交，而这正是不交性的用途，也是全书唯一用到它的地方。
还有第五样东西，但它是一句观察、不是一步。选择相对于此载体上的一个 ZF 模型陈述，因为它所点名的交是那个模型的派生运算；而这份依赖的全部，不过是沿交的规格的一次搬运。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth 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.Stage {ℓ} lem using ( bound-below₂ ) open import L.Choice.Step {ℓ} lem using ( Mem; relOf ) open import L.Choice.Order {ℓ} lem using ( module Bound ) open import L.Coding.Model {ℓ} using ( appAt; appAt-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 TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ module ModelL = FOL.ZFModel 𝒮ʟ open ModelL using ( isZFModel ) module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
那条描述
一条公式，一个自由变元，两个常量。它对一个集合 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 ≐ con r) ∧̇ (¬̇ ∃̇ ( (var zero ∈̇ var (suc (suc zero))) ∧̇ appAt (suc zero) zero (suc (suc (suc zero))) )) ) ) )
横截集
本模块固定下供应交运算的那个 ZF 模型、那个族，以及该族的两条假设。上界与序径直取自上一章施于该族自身之处：β 是一个高于该族自身阶段的序数，从而高于它的成员及其成员，也高于诸名字所住的 ω；W 是 β 处塔的诸成员上的良序；而 rel 就是同一个序作为模型的一个元素，正是这一点才使它能在描述中被一个常量点名。
Cell x 是那些成员之上「是 x 的成员」这条谓词，而 least 是良序那一章的搜索施于它。那场搜索自写下之日起就一直在等：L.WellOrder.Base 交付时点名了恰一个消费方，而手上一个也没有；这里就是那个消费方。这也正是排中律换来一次真正的选取、而非一次比较的地方，而那一章当初说这笔代价就是为此而花的。
pick-in 与 pick-out 是那条描述的两条读式，而两者互不为推论：一条由极小元造出一个满足关系，另一条由满足关系取出一个极小元，且各自都要把一个集合在它可被呈现的两种形态之间搬动，即作为 L 的元素与作为 β 处塔的成员。每个截断载荷都有名字，从 Two 到 Four，于是两条读式都不必把嵌套写开；否定式是唯一一处把截断消去到空类型的地方，而它是在一个具名辅助件里消去的。
随后是分离与计数。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) Four : S → S → S → S → Type (ℓ-suc ℓ) Four x z r w = ⟨ w ∈ˢ x ⟩ × ⟨ (w ∷ r ∷ x ∷ z ∷ []) ⊨ appAt (suc zero) zero (suc (suc (suc zero))) ⟩ Three : S → S → S → Type (ℓ-suc ℓ) Three x z r = (fst r ≡ fst rel) × (∥ Σ[ w ∈ S ] Four x z r w ∥₁ → Empty.⊥) Two : S → S → Type (ℓ-suc ℓ) Two x z = ⟨ x ∈ˢ a ⟩ × (⟨ z ∈ˢ x ⟩ × ∥ Σ[ r ∈ S ] Three x z r ∥₁) 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 , ∣ rel , (refl , neg) ∣₁)) ∣₁ where atFour : Σ[ w ∈ S ] Four x z rel w → Empty.⊥ atFour (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 ⟨_⟩ (appAt-adequate (suc zero) zero (suc (suc (suc zero))) (w ∷ rel ∷ 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 ] Four x z rel w ∥₁ → Empty.⊥ neg = PT.rec Empty.isProp⊥ atFour pick-out : (z : S) → ⟨ (z ∷ []) ⊨ Pick a rel ⟩ → Out z pick-out z = PT.rec PT.squash₁ atTwo where atThree : (x : S) → ⟨ x ∈ˢ a ⟩ → ⟨ z ∈ˢ x ⟩ → (r : S) → Three x z r → Out z atThree x x∈a z∈x r (qr , 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 = neg ∣ elt b , (b∈x , hap) ∣₁ where hpr : ⟨ pr (fst b) (fst z) ∈ fst r ⟩ hpr = subst (λ s → ⟨ pr (fst b) (fst z) ∈ s ⟩) (sym qr) (B.orderL-fill b (fst z , hz) lt) hap : ⟨ (elt b ∷ r ∷ x ∷ z ∷ []) ⊨ appAt (suc zero) zero (suc (suc (suc zero))) ⟩ hap = subst ⟨_⟩ (sym (appAt-adequate (suc zero) zero (suc (suc (suc zero))) (elt b ∷ r ∷ x ∷ z ∷ []))) hpr atTwo : Σ[ x ∈ S ] Two x z → Out z atTwo (x , (x∈a , (z∈x , h))) = PT.rec PT.squash₁ (λ { (r , h3) → atThree x x∈a z∈x r h3 }) h 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
定理
ChoiceStatement 就是前沿曾经持有的那条陈述，原样移到此处，且不再是一笔债：模型的选择字段在 𝒮ʟ 处的样子，相对于此载体上的一个 ZF 模型而言，因为那个交是那个模型的派生运算。hasChoiceL 证出它。根章把它施于正在装配的那个模型自身，而这正是这条陈述一开始就要对模型作全称的原因。
有了这一行，登记簿便空了，于是 L.Frontier 被删除，根章的第二个参数也随之删除。这正是那件装置立身的承诺：字段一经证明即被删除，而账清之日 record 随之消失。
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 是那条描述：该族的某个成员含有这个集合，且那个成员中没有任何东西排在它之前。pick-in 与 pick-out 是它对着「是某个成员的极小元」的两条读式。transversalSet 是模型的分离据它在该族的界层序数处的塔之上雕出的东西，而 transversal 数清它与每个成员之交：恰一点，存在性来自那场极小元搜索，唯一性来自两两不交。hasChoiceL 就是模型的选择字段，有了它，前沿即告清空并被删除。
一次实测，且是一条定律偏偏没有咬人。读在常元上的描述要在被造出之处封印，而这条定律在被发现之处值九十九倍；在此处它一文不值，封印与否都是 2.3 秒，因为这条描述不携带任何已编码的语法。封印仍然保留，而那个数字被记下来，好让这条定律保持它真正的形状：它关乎一条描述装着什么，而不关乎它被读在哪里。
本书是为了什么
这是这条链的终点，故值得把立住的东西平白说一遍。在 cubical Agda 之内，给定模型自身真值层级上的一份排中律，可构造宇宙是 ZFC 的模型。与第三部 (环境层级满足 ZF) 合读，这就是哥德尔的选择公理相对一致性的语义形式：满足 ZF 的宇宙内部含有一个满足 ZFC 的子宇宙，故 ZFC 的任何矛盾都早已是 ZF 的矛盾。
每一分价格都印在标签上。宿主是带宇宙塔的 cubical Agda，其强度非形式地约当于 ZFC 加一个不可达基数；排中律是模块参数而非公理，且是这条定理携带的唯一假设；而本开发中处处没有公设、没有洞，且自本章起，也没有尚未证明之陈述的登记簿。本书开篇先陈述了自己还证不出的主定理，并以一个 record 为这份诚实付账，其字段就是那些未清的论断。那个 record 空了。剩下的是一条定理。