ZF と ZFC のモデル

この章を読むか、読書案内と依存マップで別のルートを選べます。

読書案内 · 依存マップ

公理を持たない構造は、ZF の各公理の証拠を与えることで集合論のモデルになります。本章ではこの道を段階を追って進めます。まず集合がいつクラスを実現するかを定め、明示的な外延性の議論から実現者の一意性を証明し、一意存在から集合を読み出す確定記述の演算子を導入し、公理を record にまとめます。最後に選択公理を加えて、ZF モデルを ZFC モデルへ拡張します。

裸の構造には、集合論の名に値するものはまだ何もありません。その所属関係が空集合を許すとは限らず、二つの要素を対にできるとも、何かの部分集合を集められるとも限りません。集合の宇宙が何を提供しなければならないかは、まさに ZF 公理の述べる通りであり、本章はそれを書き下ろします。ZF モデルとは、そのフィールドが公理を供給する構造であり、「𝒮 が ZF を満たす」とは、そのような証拠が 𝒮 で存在することを意味するにすぎません。

設定はここで一度だけ確定します。𝒮 の等号と所属は hProp ℓ に値を取るので、その主張はすべて命題です。モジュール全体が同じ宇宙レベル ℓ で動作し、公理は Type (ℓ-suc ℓ) に住みます。

モジュールのシグネチャは、調べる対象の種類を示します。𝒮 は真理値が命題である ZFStructure、すなわち hProp ℓ の上の構造です。ここから二つのことがすぐに従います。第一に、構造の等号 ≈ˢ と所属 ∈ˢ は基礎型をもつ命題を返すので、本章の所属の主張は証拠で満たせるものになります。第二に、パラメータ {ℓ} は宇宙レベルであり、全体を通して固定されます。台 S は Type ℓ に住み、S のすべての部分集合を量化する命題、つまり公理そのものは Type (ℓ-suc ℓ) に置かれます。

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

open import Base.Prelude
open import FOL.ZFStructure using ( ZFStructure; module hPropStructure )

module FOL.ZFModel {ℓ} (𝒮 : ZFStructure ℓ) where

これらの公理は事実を hProp で直接主張します。定数の解釈には意味論の章の正準なものを採ります。定数域は台そのものであり、解釈は id なので、論理式に現れる定数は、まさにその名が指す集合そのものです。

ここで公理に必要な作業用の語彙をそろえます。構文の章は Formula、所属記号 ∈̇、構成子 var と con を供給し、分出と置換は論理式を本物の入力として受け取ることになります。意味論の章はモジュール At を提供します。これは定数解釈を一つに固定し、その解釈での論理式の充足を公開します。ホストのライブラリからは、第二成分が命題である依存対のパスを帰着させる Σ≡Prop、正則性が記録する整礎性の型 WellFounded、空の型 Empty.⊥、そして選択公理で使う命題の截断 ∥_∥₁ が来ます。

open import FOL.Syntax using ( Formula; var; con; _∈̇_ )
open import FOL.Semantics 𝒮 using ( module At )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Induction.WellFounded using ( WellFounded )
import Cubical.Data.Empty as Empty

二つの open が構造と充足関係の名前をスコープに入れます。hProp 上の直接の論理演算は基礎語彙からすでに得られています。hPropStructure 𝒮 を開くと、構造の台 S、その h-集合性の証拠、真理値を返す二つの関係 ≈ˢ と ∈ˢ、さらに所属の Type 値の読み ∈ᵗ が得られます。最後に At S id を開くと、充足関係 _⊨_ が正準な定数解釈で具体化されます。そこでは定数が自分自身を指すので、論理式の自由変数の枠は、特定の集合への所属として読まれます。

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )

open hPropStructure 𝒮

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 が命題なのは、各繊維が命題だからです。hProp ℓ は hProp ℓ であり、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) には基礎型があるからです。しかし定義はすべてを真理値のまま保ちます。

_⊆ˢ_ : S → S → hProp ℓ
a ⊆ˢ b = ∀[ x ∶ S ] (x ∈ˢ a) ⇒ (x ∈ˢ b)

記号 a ⊆ˢ b は冪集合の公理と後の議論で用います。所属、等号、部分集合を同時に含む式が一意に読めるよう、ここで優先順位を定めます。

infix 20 _⊆ˢ_

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 は矛盾を導き、その証拠は空のホスト型 Empty.⊥ に落ちます。読み方に注意してください。∈ˢ は hProp ℓ の命題を返し、⟨_⟩ がその基礎型を取り、その型の inhabitant からフィールドは荒謬を導きます。これは第零の数項が要素をもたないことを述べるものであり、派生した空集合には一言も触れません。

  field
    numeral      : ℕ → S
    numeral-zero : (z : S) → ⟨ z ∈ˢ numeral zero ⟩ → Empty.⊥
    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 は截断されません。