Bedrockこの章を読むか、対話型目次と依存グラフで別のルートを選べます。
対話型目次 · 依存グラフモジュールのシグネチャは、調べる対象の種類を示す。𝒮 は真理値が命題である ZFStructure、すなわち hProp ℓ の上の構造である。ここから二つのことがすぐに従う。第一に、構造の等号 ≈ˢ と所属 ∈ˢ は基礎型をもつ命題を返すので、本章の所属の主張は証拠で満たせるものになる。第二に、パラメータ {ℓ} は宇宙レベルであり、全体を通して固定される。台 S は Type ℓ に住み、S のすべての部分集合を量化する命題、つまり公理そのものは Type (ℓ-suc ℓ) に置かれる。
module FOL.ZFModel {ℓ} (𝒮 : ZFStructureₕ ℓ) where
公理を持たない構造は、ZF の各公理の証拠を与えることで集合論のモデルになる。本章ではこの道を段階を追って進める。まず集合がいつクラスを実現するかを定め、明示的な外延性の議論から実現者の一意性を証明し、一意存在から集合を読み出す確定記述の演算子を導入し、公理を record にまとめる。最後に選択公理を加えて、ZF モデルを ZFC モデルへ拡張する。
裸の構造には、集合論の名に値するものはまだ何もない。その所属関係が空集合を許すとは限らず、二つの要素を対にできるとも、何かの部分集合を集められるとも限らない。集合の宇宙が何を提供しなければならないかは、まさに ZF 公理の述べる通りであり、本章はそれを書き下ろす。ZF モデルとは、そのフィールドが公理を供給する構造であり、「𝒮 が ZF を満たす」とは、そのような証拠が 𝒮 で存在することを意味するにすぎない。
設定はここで一度だけ確定する。𝒮 の等号と所属は hProp ℓ に値を取るので、その主張はすべて命題である。モジュール全体が同じ宇宙レベル ℓ で動作し、公理は Type (ℓ-suc ℓ) に住む。
これらの公理は事実を hProp で直接主張する。定数の解釈には意味論の章の正準なものを採る。定数域は台そのものであり、解釈は id なので、論理式に現れる定数は、まさにその名が指す集合そのものである。
ここで公理に必要な作業用の語彙をそろえる。構文の章は Formula、所属記号 ∈̇、構成子 var と con を供給し、分出と置換は論理式を本物の入力として受け取ることになる。意味論の章はモジュール At を提供する。これは定数解釈を一つに固定し、その解釈での論理式の充足を公開する。ホストのライブラリからは、第二成分が命題である依存対のパスを帰着させる Σ≡Prop、正則性が記録する整礎性の型 WellFounded、空の型 ⊥*、そして選択公理で使う命題の截断 ∥_∥₁ が来る。
open import Cubical.Induction.WellFounded using ( WellFounded )
二つの open が構造と充足関係の名前をスコープに入れる。hProp 上の直接の論理演算は基礎語彙からすでに得られている。hPropView 𝒮 を開くと、構造の台 S、その h-集合性の証拠、真理値を返す二つの関係 ≈ˢ と ∈ˢ、さらに所属の Type 値の読み ∈ᵗ が得られる。最後に At S id を開くと、充足関係 _⊨_ が正準な定数解釈で具体化される。そこでは定数が自分自身を指すので、論理式の自由変数の枠は、特定の集合への所属として読まれる。
open hPropView 𝒮
open At S id using ( _⊨_ )
クラスを集合として実現する
これから出てくる公理はほとんどすべて同じ形をしている。ある集合が存在して、その要素がちょうどかくかくしかじかである。まず「かくかくしかじか」をはっきりさせよう。クラスとは台の上の命題値の述語 S → hProp ℓ のことである。所属を語ることはできるが、それを集める集合があるとは限らない。(クラスはすでに別の姿で現れている。構造の章の制限 𝒮 ↾ M は、まさにこのような M に沿って切り取る操作であった。) 本節では、集合がいつクラスを実現するかを定義し、実現そのものが命題であることを見て、両者を一つにまとめる。
実現の定義は意図的に各点ごとの形をしている。IsSetOf Q b は、台のすべての要素 x について、命題 x ∈ˢ b が hProp ℓ の要素としてクラスの値 Q x に等しいときに成る。ここに公式も構文も簡約もなく、比較は真理値の直接的な等式である。この型は S 全体を量化するため Type (ℓ-suc ℓ) に住み、公理そのものの住処と一致する。
IsSetOf : (S → hProp ℓ) → S → Type (ℓ-suc ℓ)
IsSetOf Q b = (x : S) → (x ∈ˢ b) ≡ Q x
isPropIsSetOf : (Q : S → hProp ℓ) (b : S) → isProp (IsSetOf Q b)
isPropIsSetOf Q b = isPropΠ (λ x → isSetHProp _ _)
SetOf : (S → hProp ℓ) → Type (ℓ-suc ℓ)
実現がより重いデータではなく命題であることを、ここで確かめる。関数型 (x : S) → (x ∈ˢ b) ≡ Q x が命題なのは、この型族の各値が命題だからである。isSetHProp は hProp ℓ が h-集合であることを述べるので、その任意の二要素の間のパス型は命題になる。isPropΠ がこの各点の事実を関数型全体へ持ち上げる。したがって SetOf Q、つまり候補の集合 b と証拠 IsSetOf Q b の依存対は、第二成分が命題である対のままである。この事実は後で繰り返し使われる。
SetOf Q = Σ[ b ∶ S ] IsSetOf Q b
一つのクラスに実現者はいくつあり得るであろうか。外延性 (同じ要素をもつ集合は等しい。これは record の最初のフィールドになる) の下では、答えは高々一つであり、しかも強い構造的な意味でそうである。どれか一つの実現者が、実現者全体の型を可縮にする。この補題が外延性を明示的な入力として受け取るのは、それを提供する record がまだ定義されていないからである。
クラス Q の実現者 (b , sp) が与えられると、収縮は他の任意の実現者 (b' , sp') をそれへのパスに写す。第一成分のパスは、外延性を λ x → sp x ∙ sym (sp' x) に適用したものである。各 x で二つの仕様はそれぞれ x ∈ˢ b ≡ Q x と x ∈ˢ b' ≡ Q x を与え、第一のパスと第二の逆向きを合成すれば x ∈ˢ b ≡ x ∈ˢ b' が得られ、外延性はまさにこれを b ≡ b' に変える。第二成分は Σ≡Prop で片付ける。isPropIsSetOf が任意の二つの実現者の仕様の相等を示すので、これが正当である。引数の形に注意してほしい。クラス Q と一つの実現者が明示的な入力であり、結論は文字通り、型 SetOf Q がその実現者を中心として可縮であることである。
setOf-unique : ({a b : S} → ((x : S) → (x ∈ˢ a) ≡ (x ∈ˢ b)) → a ≡ b)
→ (Q : S → hProp ℓ) → SetOf Q → isContr (SetOf Q)
setOf-unique ext Q (b , sp) = (b , sp) , λ { (b' , sp') →
Σ≡Prop (isPropIsSetOf Q) (ext (λ x → sp x ∙ sym (sp' x))) }
確定記述の演算子
isContr はホストの一意存在である。中心と、すべての要素をその中心へ収縮させるデータを組にしたものである。したがって isContr (SetOf Q) は「Q なるものからなる集合がちょうど一つ存在する」と読め、中心がそのまま正準な証拠を供給する。以降の存在公理はすべてこの形を取り、その見返りはすぐに現れる。一意存在があれば、「条件を満たすあの集合」は射影になる。収縮の中心がすでにデータであるため、別の古典的な記述公理は要らない。
演算子 ℩ は SetOf Q の収縮の証拠を受け取り、その中心の第一成分、つまり S の要素を返す。isContr A は中心と収縮を組にしたものなので、c .fst が中心であり、もう一度射影すれば集合そのものに届く。古典的な扱いならここで記述公理を持ち出すところであるが、ここでは一意存在から証拠への移行が純粋なデータの取り出しである。以下の公理が截断された存在ではなく isContr で述べられているのは、まさにこのためである。
℩ : {Q : S → hProp ℓ} → isContr (SetOf Q) → S
℩ c = c .fst .fst
取り出した集合の要素が何であるかを読み戻す手段がなければ、その集合は役に立たない。この読み戻しもまた射影である。℩-spec c は中心が担う仕様、すなわち収縮の第一成分の第二成分である。両者を合わせると、Q なるものからなる一意な集合が存在し、℩ はその集合を証書 x ∈ˢ (℩ c) ≡ Q x とともに手渡す、となる。以降の派生演算はいずれも、公理のフィールドに ℩ を適用し、℩-spec を仕様として引用するだけで構成される。
℩-spec : {Q : S → hProp ℓ} (c : isContr (SetOf Q)) → IsSetOf Q (℩ c)
℩-spec c = c .fst .snd
部分集合
語彙を完成させるために、派生関係がもう一つ必要である。a ⊆ˢ b は、a の各要素が b にも属することを表す。これは外延性が比較する関係を、定理の仮定ではなく真理値として読んだものである。集合を返すこれからの公理と違って hProp ℓ に住み、ホストの関数型ではなく hProp 上の直接の全称量化子で述べられる。冪集合のフィールドも、選択公理の選択集合の形も、これを用いて述べられる。
定義は hProp 上の直接の全称量化子 ∀[ x ] P x を用いて、台のすべての x にわたる含意 x ∈ˢ a ⇒ x ∈ˢ b を連言する。hProp ℓ の中に留まることが重要である。結果は構造の真理値であり、他の結合子と比較・結合できる。メタレベルの関数型にはそれができない。Type 値の含意も使える。hProp の (x ∈ˢ a) ⇒ (x ∈ˢ b) には基礎型があるからである。しかし定義はすべてを真理値のまま保つ。
infix 20 _⊆ˢ_
_⊆ˢ_ : S → S → hProp ℓ
a ⊆ˢ b = ∀[ x ∶ S ] (x ∈ˢ a) ⇒ (x ∈ˢ b)
記号 a ⊆ˢ b は冪集合の公理と後の議論で用いる。所属、等号、部分集合を同時に含む式が一意に読めるよう、ここで優先順位を定める。
record としての ZF 公理
ここが本章の中心である。フィールドは三種に分けられる。第一は外延性と存在の公理、すなわち空集合、対、和集合、分出、置換、冪集合で、いずれも直前に用意した一意存在の形を取り、それぞれ ℩ を通して集合を得る (無限は後に加わる)。第二は二つの論理式のスキーマである。分出と置換は Formula S 1 または Formula S 2 を受け取り、意味論の章の充足関係で解釈するので、一階論理の諸章で作られた言語がここで実際の仕事をする。ここでの制限は明示的である。これらのフィールドが量化するのは符号化された一階論理式であり、任意のホスト述語 S → hProp ℓ ではない。したがって各実例は対象言語の構文を伴い、充足関係によって解釈される。第三は正則性である。Type 値の所属関係の整礎性として、ホストのライブラリの WellFounded _∈ᵗ_ で記録する。次の節で、なぜこの公理だけがメタレベルで述べられ、他が構造の内部に住むのかを説明する。
この record は、命題値の構造に公理が要求する保証を加えたものである。フィールドが S 全体を量化するため、record 自身は Type (ℓ-suc ℓ) に住む。最初の二つのフィールドは一意存在の形ではない。外延性は、所属の真理値が各点で一致することからパス a ≡ b を得る含意であり、setOf-unique を成立させた仮定そのものである。正則性は WellFounded _∈ᵗ_、つまり Type 値の所属関係の整礎性である。これは各要素に Acc のデータを与え、所属に沿った再帰と帰納を可能にする。残りのフィールドはそれぞれ、あるクラス Q に対して isContr (SetOf Q) を主張する。
record isZFModel : Type (ℓ-suc ℓ) where
field
extensional : {a b : S} → ((x : S) → (x ∈ˢ a) ≡ (x ∈ˢ b)) → a ≡ b
regularity : WellFounded _∈ᵗ_
hasEmpty : isContr (SetOf (λ _ → ⊥))
それぞれのクラスを自然言語に読み戻すと、教科書の言明がそのまま現れる。⊥ を実現するものはないので、空集合とは恒偽のクラスを実現する一意な集合である。a と b の対は、「a と構造的に等しいか b と構造的に等しい」というクラスを実現し、hProp 上の直接の選言 ⊔ で結ばれる。a の和集合は、「a のある要素 y に属する」という形の x のクラスを実現し、⊓ で連言し、∃[ x ] P x で存在的に集める。分出は最初の論理式を受け取るフィールドで、a の要素のうち φ を満たすものをちょうど残す。クラスは「a への所属」と「論理式 φ が一要素の環境 x ∷ [] で充足されること」の連言であり、この環境の唯一の項が Formula S 1 の唯一の自由変数の枠を埋める。
hasPair : (a b : S) → isContr (SetOf (λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b)))
hasUnion : (a : S) → isContr (SetOf (λ x → ∃[ y ∶ S ] (y ∈ˢ a) ⊓ (x ∈ˢ y)))
hasSeparation : (a : S) (φ : Formula S 1)
→ isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)))
hasReplacement : (a : S) (φ : Formula S 2)
置換は最も長いフィールドで、それ自身の仮定を一つ持つ。受け取るのは Formula S 2 であり、その二つの自由変数の枠は環境 y ∷ x ∷ [] の順で読まれる。まず出力の値、次に入力である。仮定は、φ が a の上で関数的であること、つまり a の各要素 x に対して φ を満たす y がちょうど一つあることである。このちょうど一つは、そのような y の型の isContr として表される。この仮定の下で、フィールドは像の一意存在、すなわち a のある要素と関係 φ に立つ y 全体の集合を主張する。何を主張しないかにも注意してほしい。関数性の仮定がなければ、このフィールドは何も主張しない。これは、古典的な扱いで置換公理が関数的な論理式に限られることと対応している。最後に、a の冪集合は部分集合のクラスを実現し、前節の派生関係 ⊆ˢ を用いる。
→ ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∶ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩))
→ isContr (SetOf (λ y → ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ)))
hasPower : (a : S) → isContr (SetOf (λ x → x ⊆ˢ a))
それぞれの λ を自然言語に読み戻すと、おなじみの言明が並ぶ。⊥ を実現するものはないので、hasEmpty が空集合である。対の要素は a または b と等しいものであり、和集合の要素は要素の要素である。分出は a の要素のうち φ を満たすものを残す (環境 x ∷ [] が唯一の自由変数を埋める)。置換はまず φ が a の上で関数的であること、つまり isContr の意味で一入力一出力であることを求め、それから出力を集める。冪集合の要素は部分集合である。
正則性公理をメタレベルに置く理由
他の公理はいずれも対象言語か単純な所属で語るが、正則性公理だけはホストの整礎性の概念に頼る。古典的な理由は、外部の整礎性を表現する一階の文は存在しないことである。古典的モデル理論のコンパクト性定理により、ちょうど整礎な構造で成り立つ文は、無限降下の ∈-列をもつ構造でも成り立つ。拡張された理論 (新しい定数の列 $a_{n+1} \in a_n$) の各有限断片はモデルを持つからである。本書はこの議論を語るが、これに依存せず、コンパクト性も展開しない。実用的な理由は型 WellFounded _∈ᵗ_ そのものに見える。整礎性を明示的なデータとして持てば、所属に沿った再帰と帰納が使える。代償は、この条件が一階の論理式からは見えなくなることである。その損失がどのほど重要かについて、本章は以下で証明する範囲を超えて何も主張しない。
公理から得られる演算
いまや ℩ がそれぞれの一意存在を演算に変え、℩-spec がそれを仕様に変える。以下の仕様はすべて文字通り一つの射影である。対の和集合が二項の和集合を与え、二項の和集合から後者 a ⁺ = a ∪ {a} が得られる (a と自分自身の対が一元集合である)。これは一つの集合から次の集合へ進むフォン・ノイマンの一歩であり、無限公理が後に使う一歩である。
record の中では、各フィールドに ℩ を適用することで演算が得られる。空集合は ℩ hasEmpty であり、対の演算 pair a b は、具体的な a と b における対の証拠に ℩ を適用する。どの適用も正当である。フィールドが isContr (SetOf _) を提供し、それがちょうど ℩ の入力型だからである。仕様 pair-spec はまったく新しい証明ではなく、同じフィールドで ℩-spec を引用したものである。その主張は実現の主張そのまま、すなわちすべての x について x ∈ˢ pair a b が選言 (x ≈ˢ a) ⊔ (x ≈ˢ b) に等しいことである。
∅ : S
∅ = ℩ hasEmpty
pair : S → S → S
pair a b = ℩ (hasPair a b)
pair-spec : ∀ a b → IsSetOf (λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b)) (pair a b)
和集合の演算 ⋃ a は a の和の証拠を取り出し、二項の和集合はそれから定義される。a ∪ b は対 pair a b の和集合であり、その要素は a の要素と b の要素の全体にほかならない。二項の和集合に別の公理は使わず、対と和の合成として得られる。定義の向きに注意してほしい。∪ は対に ⋃ を適用して作られるのであり、その逆ではない。
pair-spec a b = ℩-spec (hasPair a b)
⋃ : S → S
⋃ a = ℩ (hasUnion a)
_∪_ : S → S → S
a ∪ b = ⋃ (pair a b)
分出は、論理式そのものを引数とする演算になる。separate a φ は a と論理式 φ における分出の証拠に ℩ を適用するので、得られる集合は対象言語の構文の一部に依存する。その仕様もやはり ℩-spec をそのまま引用し、すべての x について x ∈ˢ separate a φ ≡ (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ) を与える。所属とは、a への属することと φ の充足の連言である。冪集合の演算 𝒫 a は冪集合の証拠を取り出す。それが実現するクラスを通して読めば、その要素は a の部分集合ちょうどである。
separate : (a : S) → Formula S 1 → S
separate a φ = ℩ (hasSeparation a φ)
separate-spec : ∀ a φ → IsSetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)) (separate a φ)
separate-spec a φ = ℩-spec (hasSeparation a φ)
𝒫 : S → S
末尾の空行はこの演算のブロックを閉じる。続く節はこれらの上に築かれ、まず新しい公理を何も使わずに共通部分を導出する。
𝒫 a = ℩ (hasPower a)
分出から導かれる共通部分
二項の共通部分は意図的にフィールドにしない。二つの記号からなる論理式 var zero ∈̇ con b は「その変数が b の要素である」と述べる。これを a における separate に渡せば、公理が a ∩ b を返す。その仕様は分出の仕様そのままであり、⊨ の定義節によってこの論理式の充足が x ∈ˢ b として計算されるからである。これは一般のパターンの実例である。論理式で名指せるホストの述語は、分出によって集合にできる。
定義は構文を適用した一行である。a ∩ b は、内容が原子式の所属主張 var zero ∈̇ con b だけである論理式に沿って a を分出する。定数 b は解釈 id の下で自分自身を指すので、環境 x ∷ [] でこの論理式を充足することは、充足関係の定義節によって真理値 x ∈ˢ b へと計算される。したがって仕様定理は、この特定の論理式での分出の仕様をそのまま引用したものであり、共通部分への所属は連言 x ∈ˢ a ⊓ x ∈ˢ b である。新しい公理も存在の新しい証明も要らない。二つの記号からなる論理式が、分出が実現できるホストの述語をすでに名指しているのである。
_∩_ : S → S → S
a ∩ b = separate a (var zero ∈̇ con b)
∩-spec : ∀ a b x → (x ∈ˢ (a ∩ b)) ≡ ((x ∈ˢ a) ⊓ (x ∈ˢ b))
∩-spec a b x = separate-spec a (var zero ∈̇ con b) x
無限
残る公理は一つ、真に無限な集合の存在を強制するものである。数項とはフォン・ノイマンの自然数、すなわち ∅、∅ ⁺、(∅ ⁺) ⁺、… のことである。record はこの列そのものをフィールドとして受け取り、生の所属と等号で述べた二つの命題的等式で固定する。第零の数項は要素をひとつももたず、後者の数項の要素はちょうど直前の数項とその要素である。外延性により、この二つの等式からそれぞれ numeral zero ≡ ∅ と numeral (suc n) ≡ numeral n ⁺ が正確に得られるので、列を直接定義するのとちょうど同じ強さである。得られるのは自由度である。等式は派生した ∅ をまったく言及しないため、具体的なモデルは台の上で計算に最も都合のよい形で列を提示し、確定記述の演算子を一切展開せずに等式を満たせる。
数項の列は関数 numeral : ℕ → S であり、ホストの自然数による添字付けが明示的なデータになっている。零の場合は否定の条件である。Type 値の所属 z ∈ˢ numeral zero の任意の inhabitant は矛盾を導き、その証拠は空のホスト型 ⊥* に落ちる。読み方に注意してほしい。∈ˢ は hProp ℓ の命題を返し、⟨_⟩ がその基礎型を取り、その型の inhabitant からフィールドは荒謬を導く。これは第零の数項が要素をもたないことを述べるものであり、派生した空集合には一言も触れない。
field
numeral : ℕ → S
numeral-zero : (z : S) → ⟨ z ∈ˢ numeral zero ⟩ → ⊥₀
numeral-suc : (n : ℕ) (z : S)
→ (⟨ z ∈ˢ numeral (suc n) ⟩ → ⟨ (z ∈ˢ numeral n) ⊔ (z ≈ˢ numeral n) ⟩)
後者の場合は二つの含意の組で、どちらも截断を含まない命題の読みの中にある。第一は、numeral (suc n) の要素 z が numeral n の要素であるか、それと構造的に等しいことを述べ、選言には hProp 上の ⊔ である。第二は、直前の数項のそのような要素、およびそれと等しいものが、後者の要素であることを述べる。両方向を合わせると、後者の数項の要素はちょうど直前の数項とその要素であり、これがまさにフォン・ノイマンの一歩で、∈ˢ と ≈ˢ だけで述べられている。
× (⟨ (z ∈ˢ numeral n) ⊔ (z ≈ˢ numeral n) ⟩ → ⟨ z ∈ˢ numeral (suc n) ⟩)
isNumeral が定めるクラスは、ある数項と等しい対象からなる。添字のデータが最下層の宇宙にあるため、量化は作業レベルへ lift された ℕ 上を走る。ここで採用する無限公理は、この正確なクラスが集合であると述べる。したがって ω は双方向に特徴づけられる。すべての数項がそこに属し、そのすべての要素はある数項と等しくなる。
クラス isNumeral は hProp で直接書かれた存在式である。∃[ x ] P x は台の型の上で量化し、命題の族 x ≈ˢ numeral (lower n) を選言する。∃[ x ] P x を適用するには台の型が Type ℓ である必要があるが、ℕ は Type ℓ-zero に住む。そこで Lift {ℓ-zero} {ℓ} ℕ が作業レベルへ持ち上げ、lower が普通の添字を取り戻して numeral に渡す。これは宇宙レベルの調整であって数学的な変更ではない。lift された型はまったく同じ要素を持つ。フィールド hasInfinity は、おなじみの形で、このクラスを実現する集合の一意存在を主張する。
isNumeral : S → hProp ℓ
isNumeral x = ∃[ n ∶ Lift {ℓ-zero} {ℓ} ℕ ] x ≈ˢ numeral (lower n)
field
hasInfinity : isContr (SetOf isNumeral)
ω : S
他の一意存在と同様に、ω は ℩ が hasInfinity から取り出す中心である。実現されるクラスが isNumeral そのものであるため、仕様 ℩-spec は ω のすべての要素がある数項と等しいことを述べる。この強い形を自然数の集合として直接使えるのはこのためであり、数項が埋め込まれる単なる集合ではない。
ω = ℩ hasInfinity
最初の定理
外延性は存在の機構全体を一度に引き上げる。setOf-unique により、実現者をもつクラスではその実現者が一意の実現者であり、実現者の型はそれを中心として可縮である。したがって本章の派生集合は、どれも一意性を伴う。
ZFC：選択公理による拡張
選択公理は選択集合の形で採る。集合 a の要素が空でなく互いに素であるとき、a の各要素とちょうど一点で交わる集合が存在する、というものである。この形は所属と派生した共通部分だけで述べられる。他の定式化との同値性はモデル内部の数学であり、必要になるまで先送りする。命題の截断 ∥_∥₁ は、空でないこと、共有点の証拠、選択集合の存在をそれぞれ包む。したがって公理は存在を主張するが、証拠を大域的に選ばない。これを基礎の record のフィールドにせず独立した拡張として保つことで、ZF が証明することと選択公理が追加することの区別が保たれる。
ZFC の record は繰り返すのではなく拡張する。最初のフィールドは ZF モデル全体であり、続く open ... public の行がそのすべてのフィールドを再エクスポートする。したがって ZF モデルに対して証明されたことは、一字違わず ZFC モデルにも当てはまる。record が自らの新しいフィールドを宣言するのはこの開きの後だけであり、追加された公理は基礎理論からきれいに分離される。
record isZFCModel : Type (ℓ-suc ℓ) where
field
zf : isZFModel
open isZFModel zf public
field
hasChoice の二つの仮定は、a が空でなく互いに素な集合の族であることを、ここで使える読み方で述べる。空でないことは截断されている。a の各要素 x に対してその中に y が単に存在する、つまり ∥ Σ[ y ∶ S ] ⟨ y ∈ˢ x ⟩ ∥₁ であり、選ばれた証拠はない。互いに素なことも截断されている。a の二つの要素 x と y が点 z を単に共有するなら、x ≡ y は截断なしで成る。素であるという前提の形に注意してほしい。その結論はホストのパスであり、共有点の証拠の截断こそが、截断されない相等に材料を供しているのである。
hasChoice :
(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 が単に存在し、a の各要素 x に対して共通部分 c ∩ x がちょうど一つの要素をもつ。これはその要素の型の isContr で表される。内側の isContr は截断ではない。各 x について c ∩ x の要素を一つ与え、他のそのような要素がすべてそれに等しいことを示す。外側の截断は適切な c の存在にかかるため、公理は特定の選択集合を指定しない。
→ ∥ Σ[ c ∶ S ] ((x : S) → ⟨ x ∈ˢ a ⟩
→ isContr (Σ[ z ∶ S ] ⟨ z ∈ˢ (c ∩ x) ⟩)) ∥₁
まとめ
ZF モデルは三種のフィールドをもつ record である。実現者を一意にする外延性。空集合、対、和集合、分出、置換、冪集合の一意存在のフィールドで、分出と置換は本書自身の論理式に限る。そして正則性は、所属のホストの整礎性としてメタレベルで述べられ、所属に沿った再帰と帰納が使える。℩ はフィールドを演算に変え、その仕様は射影である。二項の和集合と後者は合成であり、共通部分は分出と、充足が直接計算される二つの記号の論理式から得られた。無限は数項の列、すなわち生の所属の等式で固定される関数 ℕ → S として入り、強い形は ω を要素がすべて数項である集合にする。isZFCModel はその上に選択公理を加える。空でないことと共有点の証拠は截断され、結論も截断されるが、各共通部分についての isContr は截断されない。