---
title: "横断集合による選択"
module: L.Choice.Transversal
lang: ja
site: "Bedrock"
description: "横断集合による選択"
stage: "正準整列順序と選択公理"
reading_order: 84
canonical: https://bedrock.institute/ja/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/zh/L.Choice.Transversal.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 横断集合による選択
本章では `𝒮ʟ` の選択公理を証明する。段階有界な内部の整列順序で各セルの最小要素を分出し、得られた集合が互いに素な各セルとちょうど一点で交わることを示す。
英語原文
This chapter proves the axiom of choice at `𝒮ʟ` in the **transversal** form
used by the model record: given a set whose members
are inhabited and pairwise disjoint, merely a set meeting each member in exactly
one point.
英語原文
The argument follows the classical proof, with its most laborious step already
carried out earlier. The textbook well-orders the universe and takes the least member of every
cell. A well-order of all of `L` is a relation on a proper class, and this book
never built one; what the previous chapters built instead is a well-order of each
**stage**, uniformly, and, at every ordinal, as an element of the model. That is
enough, because a set is small. One ordinal bounds a family, its members and
their members all at once, and inside the tower at that ordinal the choosing is
an ordinary least-element search.
英語原文
So the chapter is four moves. The **bound**: the stage chapter's bounding ordinal
for the family, above the family's own stage and hence above every member of
every member of it. The **order there**: the table's relation at that ordinal, an
element of the model, with two lemmas reading membership in it against the meta
comparison in both directions. The **description**: "some member of the family
contains this set, and nothing in that member precedes it", a formula with the
order as a constant, which the model's own separation cuts a set out with. The
**count**: that set meets each member in exactly one point, existence from the
least element and uniqueness from pairwise disjointness, which is what
disjointness is for and the only place the book uses it.
英語原文
There is a fifth thing, and it is an observation rather than a move. Choice is
stated relative to a ZF model on this carrier, because the intersection it names
is that model's derived operation; and the whole of that dependence is one
transport along the intersection's specification.
```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` は一自由変数の論理式であり、点が族のある要素に属し、選んだ関係の下でその中に先行する点がないことを述べる。
英語原文
One formula, one free variable, two constants. Of a set `z` it says: some member
of the family contains `z`, and nothing in that member precedes `z` under the
order. The application atom takes the order directly as a constant. The family
is likewise named directly, since it appears only under a membership atom.
英語原文
The formula is sealed, by the standing law that a description read at constants
is sealed where it is built. Here that law is free rather than decisive: sealed
and unsealed both check in 2.3 s, and the chapter says so rather than borrowing
someone else's number. The reason is worth one line, because it says what the
earlier measurements were really about. Those descriptions carried coded syntax
inside them, and each satisfaction at a concrete environment normalized a whole
hierarchy description; this one carries four atoms and one application, so there
is nothing large to unfold. The seal stays, because it costs nothing and because
a later reader of this description should not have to re-measure.
英語原文
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.
```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)) )) ) )
```
## 横断集合
上界段階の内部で最小要素の探索が各セルから一点を選び、分出公理がそれらを集合に集め、互いに素であることから各交わりでの一意性が従う。
英語原文
The module fixes the ZF model supplying the intersection, the family, and the
family's two hypotheses. The choice-stage construction supplies the bound and
order at the family itself: `β` is an ordinal above the family's own
stage, hence above its members and their members, and above `ω` where the names
live; `W` is the well-order of the members of the tower at `β`; and
`rel` is that same order as an **element of the model**, which is what
lets it be named by a constant in the description at all.
英語原文
`Cell x` is the predicate "is a member of `x`" on those members, and
`least` applies the generic search from `L.WellOrder.Base` to it.
The same search serves finite-stage orders and name selection, and will serve
later GCH constructions; here its role is specific: it turns the stage order
into one chosen representative for each cell. This is precisely the selection
that excluded middle makes possible for the transversal.
英語原文
`pick-in` and `pick-out` are the description's two readings, and
neither is a corollary of the other: one builds a satisfaction out of a least
element, the other extracts a least element from a satisfaction, and each has to
move a set between the two ways it can be presented, as an element of `L` and as
a member of the tower at `β`. Every truncation payload is named,
`Two` and `Predecessor`, so that neither reading writes the nesting
out; the negation is the one place a truncation is eliminated into the empty
type, and it is eliminated in a named helper.
英語原文
Then the separation and the counting. `transversalSet` is the model's own
separation, at the tower at `β`, by the description. `Cut` fixes a
member of the family: the centre of the intersection is the least element, which
is in the transversal because `pick-in` says so and in the member because
being least includes being there. Uniqueness is where pairwise disjointness is
used. Another point of the intersection satisfies the description, so it is least in
**some** member of the family; it also lies in this one; so the two members meet
and are equal; so it is least in this member too, and least elements are unique
by trichotomy alone. The generic uniqueness theorem
`isPropLeastOf` closes precisely this last comparison.
```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` is the statement the frontier used to hold, moved here
verbatim and proved here: the model's choice field at `𝒮ʟ`, relative to a
ZF model on this carrier because the intersection is that model's derived
operation. `hasChoiceL` gives the proof. The root chapter applies it to the very
model it is assembling, which is why the statement quantifies over the model in
the first place.
英語原文
This line gives the Choice field used by the root theorem. Its statement
remains relative to the ZF model being assembled because intersection is the
derived operation of that model.
```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` is the description: some member of the family contains this set,
and nothing in that member precedes it. `pick-in` and `pick-out`
are its two readings against being a least element of a member.
`transversalSet` is what the model's separation cuts out with it, over the
tower at the family's bounding ordinal, and `transversal` counts the
intersection with each member: one point, existence from the least-element
search and uniqueness from pairwise disjointness. `hasChoiceL` is the
model's choice field, and with it the frontier is empty and gone.
英語原文
One measurement, and it is a law declining to bite. A description read at
constants is sealed where it is built, and that law was worth ninety-nine fold
where it was found; here it is worth nothing, 2.3 s either way, because this
description carries no coded syntax. The seal stays, and the number is recorded
so that the law keeps its true shape: it is about what a description **contains**,
not about where it is read.
## 本書が目指したもの
完成した Choice の構成列が最後のモデル・フィールドを与えるので、明示された唯一の排中律の仮定の下で構成可能宇宙は ZFC を満たす。
英語原文
This is the end of the chain, so it is worth stating plainly what has been
established. **In cubical Agda, granted one instance of the excluded middle at the
model's own truth level, the constructible universe is a model of ZFC.** Read with the
ambient-hierarchy result that the hierarchy models ZF, that is Gödel's relative consistency of
choice in semantic form: a universe satisfying ZF contains inside it a
sub-universe satisfying ZFC, so an inconsistency of ZFC would already be an
inconsistency of ZF.
英語原文
The costs are stated explicitly. The host is cubical Agda with its universe
tower, informally about as strong as ZFC plus an inaccessible; excluded middle
is a module parameter rather than an axiom, and it is the only hypothesis the
theorem carries; and the development has no postulates or holes. This chapter
supplies the Choice field that `L.Model` combines with the earlier ZF
structure.