Bedrock構成可能階層と構成可能宇宙
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ構成可能階層は空集合から始まり、定義可能冪集合を繰り返し施し、極限点では和集合を取ります。できあがる各段階は推移的で、塔は添字の所属に沿って単調です。いくつかの段階に現れる集合の全体がクラス L を与え、周囲の構造をそこへ制限した集合論的構造が伴います。
この章の仕事の大部分は、ひとつの設計判断が担います。塔の添字には独立した順序数の型ではなく集合そのものを使い、正則性公理が許す所属に沿った再帰で進めます。つまり Lset α = ⋃ { Def (Lset β) ∣ β ∈ α } です。このただ一本の等式が零・後者・極限を同時にカバーし、フォン・ノイマン順序数の上ではまさにゲーデルの塔になります。定義そのものは任意の集合を添字として受け入れ、添字が順序数であるという要求は、クラス L を定義する場所で初めて課されます。これと並行して帰納的述語 isLayer、すなわち「段階であること」が走ります。その構成子こそ塔の閉包原理であり、二つの見方は章全体で協調します。
本章は固定した宇宙レベル ℓ で累積階層 V の内部を扱います。その台 S は、外延的で整礎的な所属関係をもつ集合からなります。対応する構造では等式と所属を命題値の関係として読み、⟨ x ∈ˢ A ⟩ のような式は通常の所属証明の型を表します。以下の構成はこの環境で行います。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module L.Constructible {ℓ : Level} where open import FOL.ZFStructure using ( ZFStructure; _↾_; module hPropStructure; Transitive )
構成を進める数学的な材料は三つあります。第一に、所属に沿った整礎再帰です。階層の章の原理 ∈-induction は、∈ˢ に沿った再帰で集合上の関数を定義することを可能にし、塔そのものがまさにこれで定義されます。第二に、添字族の和集合と、その和への所属を両方向に読む二つのモデル補題です。第三に、定義可能性の章の演算子 Def A であり、内側の世界 (A, ∈) で A のパラメータによって定義される A の部分集合を集めるもので、これを段階ごとに施すことが階層を上へ伸ばす原動力になります。一階述語論理式の構文、とりわけ型 Formula は、まさにこの演算子のために構文の章から引き継がれます。
open import FOL.Syntax using ( Formula ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; ∈-induction-compute ) open import V.Model {ℓ} using ( union-family-in; union-family-out ) open import L.Definability {ℓ} using ( module DefOf ) open import Cubical.Foundations.HLevels using ( isProp× )
階層の集合は小さな族によって表現され、本章はその表現を通して要素を読みます。集合 α に対して ⟪ α ⟫ はその要素の小さな添字型であり、⟪ α ⟫↪ は添字をふたたび集合へ埋め込み、∈ₛ⟪ α ⟫↪ m は m の指す要素が α に属することを証明します。橋渡し ∈∈ₛ は階層固有の所属 ∈ と構造的な所属 ∈ˢ を双方向に結び、sett X f は X 上の f の値を要素とする集合を作ります。これらと並んで、命題的切り詰め ∥ _ ∥₁ とその導入 ∣ _ ∣₁ が「単に存在する」を与えます。切り詰められた主張の要素は、証人が存在すると主張するのであって、それを名指しはしません。
import Cubical.Data.Empty as Empty import Cubical.Data.Sum as Sum import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
基本の構成は所属の特徴づけとともに使えます。空集合には ∅-empty、非順序対には pairing-ax、二項和と添字族の和には union-ax が対応します。レベル ℓ-suc ℓ の命題が真理値を直接与え、周囲の構造 𝒮ᵥ を hPropStructure を通じて読むことで、命題の基礎型を取る記法 ⟨ _ ⟩ と構造的な所属を表す ∈ˢ が使えるようになります。本章のすべての主張はこの命題値の設定のなかで述べられます。
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅; ∅-empty; ⁅_,_⁆; pairing-ax; ⋃_; union-ax; _∪_ )
設定が整ったところで、定義可能冪集合の演算子に作業用の名前が与えられます。𝒟 A は定義可能性の章の Def A そのものであり、制限構造の上で A の有限個のパラメータによって定義される A の部分集合を集めたものです。この演算子の数学的内容、すなわちその要素がすべて A の部分集合であることや、推移的な A に対して A ⊆ 𝒟 A が成り立つことは、すでにそこで確立済みであり、ここでは本書を通して使われる短い記号を与えるだけです。
open hPropStructure 𝒮ᵥ 𝒟 : S → S 𝒟 A = DefOf.Def A
推移的集合
階層の各段階は推移的です。空集合は推移的であり、定義可能冪集合は推移性を保存し、推移的集合の和も推移的です。これらの閉性は、後で層を作る構成子に一つずつ対応します。
(𝒟 は前の章の Def に対する本書の短い記号で、この演算子に慣用される花文字に合わせたものです。)
集合 A が推移的であるとは、A の要素の要素が再び A の要素になることです。定義 isTransV は構造レベルの閉性条件 Transitive 𝒮ᵥ を「A と等しい集合のクラス」に具体化したものであり、したがって isTransV A の証明は文字どおり、y ∈ˢ x と x ∈ˢ A から y ∈ˢ A を与える関数です。宇宙に注意してください。この主張は台を量化するので ℓ-suc ℓ に存在します。推移性は命題であり、isPropIsTransV がこれを直接示します。二つの証明 p と q が与えられれば、その結論 y ∈ˢ A は構成により命題なので各点で一致し、立方の関数外延性がこの各点一致を p と q の間のパスへ組み立てます。最後の行は、空集合についての最初の閉性事実を宣言しています。
isTransV : S → Type (ℓ-suc ℓ) isTransV A = Transitive 𝒮ᵥ (λ x → x ∈ˢ A) isPropIsTransV : (A : S) → isProp (isTransV A) isPropIsTransV A p q i {x} {y} y∈x x∈A = (y ∈ˢ A) .snd (p y∈x x∈A) (q y∈x x∈A) i ∅-trans : isTransV ∅
空集合の場合は空虚に成り立ちます。x ∈ˢ ∅ から ∈∈ₛ を経て ∅ の本来の要素が取り出せ、∅-empty がそこから矛盾を導くので、y ∈ˢ A へ至る任意の含意が成り立ちます。定義可能冪集合については、前の章の二つの補題を組み合わせます。𝒟 A の要素 x は定義可能な部分集合なので、y ∈ x なら y ∈ A が強制され (Def∋⊆A)、これに推移性の仮定 Atr を適用すれば、推移的な A に対する A ⊆ 𝒟 A (A⊆Def) によって y は 𝒟 A に入ります。最後に ⋃-trans が和の原理を述べます。x の各要素が推移的ならば、x の要素の要素全体の集合 ⋃ x も推移的です。
∅-trans {x} y∈x x∈∅ = Empty.rec (∅-empty x (∈∈ₛ {a = x} {b = ∅} .fst x∈∅)) 𝒟-trans : ∀ {A} → isTransV A → isTransV (𝒟 A) 𝒟-trans {A} Atr {x} {y} y∈x x∈𝒟A = DefOf.Refine.A⊆Def A Atr y (DefOf.Def∋⊆A A x x∈𝒟A y y∈x) ⋃-trans : (x : S) → ((y : S) → ⟨ y ∈ˢ x ⟩ → isTransV y) → isTransV (⋃ x)
和の要素を見るには、まずそれが実際に要素であることを見なければなりません。仮定 u∈⋃x は周囲の階層における所属であり、∈∈ₛ の第二の向きがそれを切り詰められたファイバー形式へ変換します。そして union-ax がその所属を特徴づけます。すなわち u ∈ ⋃ x となるのは、u ∈ w なる w ∈ x が単に存在するとき、そしてそのときに限ります。命題的切り詰めは本質的です。公理は途中の w を名指しせず、その存在を主張するだけだからです。したがって証明は切り詰めの内部で写像を行い、対 w , (w∈ₛx , u∈ₛw) が与えられる分岐では、二度の ∈∈ₛ がファイバーのデータから使える仮定 w∈x と u∈w を復元します。
⋃-trans x mem {u} {v} v∈u u∈⋃x = ∈∈ₛ {a = v} {b = ⋃ x} .snd (union-ax x v .snd (PT.map (λ { (w , (w∈ₛx , u∈ₛw)) → let w∈x = ∈∈ₛ {a = w} {b = x} .snd w∈ₛx
この分岐では、仮定 mem w w∈x が w の推移性を言うので、v ∈ u と u ∈ w から v ∈ w が得られます。第一の向きの ∈∈ₛ で改めて変換すると、このデータは union-ax の正当なファイバーになり、命題的切り詰めの消去も、目標である「v の ⋃ x への所属」が命題であるため正当です。二項和はこれに続きます。A ∪ B は ⋃ ⁅ A , B ⁆ と定義されるので、∪-trans はこの対への ⋃-trans の適用であり、残る義務は対の各要素が推移的であることで、これを供給するのが局所的な主張 prem です。
u∈w = ∈∈ₛ {a = u} {b = w} .snd u∈ₛw in w , (w∈ₛx , ∈∈ₛ {a = v} {b = w} .fst (mem w w∈x v∈u u∈w)) }) (union-ax x u .fst (∈∈ₛ {a = u} {b = ⋃ x} .fst u∈⋃x)))) ∪-trans : ∀ {A B} → isTransV A → isTransV B → isTransV (A ∪ B) ∪-trans {A} {B} tA tB = ⋃-trans ⁅ A , B ⁆ prem
義務 prem が問うのは、対の各 y が推移的かどうかです。対の所属は「単に」の形で特徴づけられます。すなわち y ∈ ⁅ A , B ⁆ となるのは、y が A であるか y が B であることが単に成り立つときであり、選ばれた選言肢ではなく命題的切り詰めによって与えられます。消去の目標は命題 isTransV y であり、各分岐は y を A ないし B と同一視する等式 p を伴います。推移性は集合の等しさで不変なので、subst isTransV (sym p) が既知の証明 tA ないし tB をその等式に沿って型 isTransV y へ輸送します。
where prem : (y : S) → ⟨ y ∈ˢ ⁅ A , B ⁆ ⟩ → isTransV y prem y y∈ = PT.rec (isPropIsTransV y) (λ { (Sum.inl p) → subst isTransV (sym p) tA ; (Sum.inr p) → subst isTransV (sym p) tB })
prem の最後の行が命題的切り詰めされた所属を pairing-ax に通して場合分けを完成させ、二項の場合が終わります。族の形式 setUnion-trans は小さな添字族を一度に扱います。型 X : Type ℓ と関数 f : X → S が与えられれば、集合 sett X f の要素は値 f x であり、各 f x は仮定により推移的です。ここでも添字集合への所属は命題的切り詰めされており、証明が受け取るのは対 x , fx≡y、すなわち添字と、その値を y と同一視するパスです。
(pairing-ax A B y .fst (∈∈ₛ {a = y} {b = ⁅ A , B ⁆} .fst y∈)) setUnion-trans : (X : Type ℓ) (f : X → S) → ((x : X) → isTransV (f x)) → isTransV (⋃ (sett X f)) setUnion-trans X f hf = ⋃-trans (sett X f) (λ y → PT.rec (isPropIsTransV y)
ここでも輸送が帳簿づけを担います。subst isTransV fx≡y (hf x) は f x の推移性の証明を同一視に沿って y へ移し、isTransV y が命題であるため命題的切り詰めの消去が許されます。これで閉包原理、空集合、定義可能冪集合、そして一般・二項・添字付きの三形態の和、がそろいました。以下で証明する、すべての層が推移的であることの帰納は一行の振り分けとなり、各構成子がここで証明した対応する補題と結びます。
(λ { (x , fx≡y) → subst isTransV fx≡y (hf x) }))
順序数の述語
構成可能階層の添字として働くのはフォン・ノイマン順序数であり、整礎で外延的な宇宙の内部では、古典的な定義はわずかなものに縮みます。すなわち順序数とは、推移的な集合からなる推移的な集合です。整礎性と外延性は定義に書き込む必要がありません。階層が至る所でそれらを保証するからです。線形性は後の章で証明される古典的な定理であって、概念そのものの一部ではありません。この章ではこの述語とその命題性を記録し、順序数の理論は必要になったときに専用の章で展開されます。
したがって IsOrd A は二つの命題の積です。A が推移的であり、かつ A の各要素が推移的である、という二つです。isPropIsOrd A は、命題が積と依存関数に関して閉じていることを使い、両成分の命題性を合わせます。この証明書は isL の定義で明示的に使われ、(IsOrd α , isPropIsOrd α) が「段階の添字は順序数である」という真理値を与えます。
IsOrd : S → Type (ℓ-suc ℓ) IsOrd A = isTransV A × ((x : S) → ⟨ x ∈ˢ A ⟩ → isTransV x) isPropIsOrd : (A : S) → isProp (IsOrd A) isPropIsOrd A = isProp× (isPropIsTransV A) (isPropΠ λ x → isPropΠ λ _ → isPropIsTransV x)
層
isLayer A は塔の閉包性を五つの構成子で記録します。空集合は層であり、層に 𝒟 を適用したものも層です。和集合については、要素がすべて層である集合、二つの層、小さく添字付けられた層の族、という三つの形を受け入れます。すべての層について性質を証明するときの帰納法の場合分けは、この五つです。特に各場合は、前節で証明した推移性の補題の一つに対応します。
この述語は台を添字とする帰納的な族であり、構成子は段階の生成規則として読めます。基底の場合は、空集合が段階であること。𝒟 による閉包は、A が段階ならその定義可能冪集合も段階であることで、後者ステップに対応します。一般の和の構成子は極限ステップに対応します。x の要素がすべて、切り詰めなしに層であるなら、⋃ x も層です。二項和の構成子は、A と B の層の証明から直接 A ∪ B を扱います。各構成子は、前節の推移性の補題の一つを isTransV を isLayer に置き換えた形に対応し、この平行性こそが次の証明を即座にします。
data isLayer : S → Type (ℓ-suc ℓ) where ∅-layer : isLayer ∅ 𝒟-layer : ∀ {A} → isLayer A → isLayer (𝒟 A) union-layer : (x : S) → ((y : S) → ⟨ y ∈ˢ x ⟩ → isLayer y) → isLayer (⋃ x) union₂-layer : ∀ {A B} → isLayer A → isLayer B → isLayer (A ∪ B)
小さな添字族の構成子が全体を完成させます。型 X : Type ℓ と族 f : X → S に対し、すべての値が層なら、和 ⋃ (sett X f) も層です。極限段階は、まさにこの構成子を通して前段階の族から組み立てられます。次に帰納です。layer-trans、すなわちすべての層が推移的であることを示すには、層を帰納的な引数として受け取るので、場合はその構成子で定まります。空集合の場合はそのまま ∅-trans です。𝒟 の場合は 𝒟-trans を適用し、その前提は下の層に対する帰納仮定 layer-trans lA です。
setUnion-layer : (X : Type ℓ) (f : X → S) → ((x : X) → isLayer (f x)) → isLayer (⋃ (sett X f)) layer-trans : ∀ {A} → isLayer A → isTransV A layer-trans ∅-layer = ∅-trans layer-trans (𝒟-layer {A} lA) = 𝒟-trans {A} (layer-trans lA)
三つの和の場合も同じように直接に振り分けられます。一般の和の場合は、要素ごとの帰納仮定を ⋃-trans に渡します。この補題は x の各要素 y に対する y の推移性の証明を要求しますが、構成子の前提 mem がまさにそれを切り詰めなしで供給するため、命題的切り詰めの消去は必要ありません。二項の場合は二つの帰納仮定に対する ∪-trans です。族の場合は各点の帰納仮定を伴う setUnion-trans です。こうしてこの節は、構造的再帰だけで塔のすべての段階が推移的集合であることを確立します。本章の後半でクラス L の推移性を示す際に用いられる事実です。
layer-trans (union-layer x mem) = ⋃-trans x (λ y y∈x → layer-trans (mem y y∈x)) layer-trans (union₂-layer lA lB) = ∪-trans (layer-trans lA) (layer-trans lB) layer-trans (setUnion-layer X f hf) = setUnion-trans X f (λ x → layer-trans (hf x))
階層
いよいよ塔そのものを、所属に沿った再帰で構成します。まず二つの技術的な措置を施します。𝒟 を展開すると論理式上の大きな sett になり、再帰の仕組みそのものも到達可能性の消去子へ展開されます。露出したままだと両者がその後の変換に割り込むため、opaque によって 𝒟ₒ と塔を不透明にし、明示的に展開するブロックの内側でのみ開き、Lset-compute を塔の宣言された展開式とします。ステップは、添字 α の要素 β にわたって再帰値に 𝒟ₒ を施したものの和集合を取り、計算規則は命題としてのパスとして成り立ちます。
まず演算子を opaque ブロックの内側で 𝒟ₒ として包み直し、Def の込み入った定義が、補題が明示的に展開を求めない限り姿を現さないようにします。ステップ関数 LsetStep は添字集合 α と、α の各要素 β に対する再帰値 rec β を受け取ります。ここでの所属は、構造的な所属の命題を型として読む ∈ᵗ を通して現れます。本体は、小さな添字 m : ⟪ α ⟫ を、m の指す要素 ⟪ α ⟫↪ m での再帰値に 𝒟ₒ を施したものへ写す族を作り、その和集合を取ります。この和を添字型にわたって展開すれば、意図された読みはまさに ⋃ { 𝒟ₒ (Lset β) ∣ β ∈ α } であり、一本の等式が零・後者・極限を等しく扱います。α が空なら和は空、後者なら古典的な次のステップを繰り返し、極限ならすべての前段階を一度に集めます。
opaque 𝒟ₒ : S → S 𝒟ₒ A = 𝒟 A LsetStep : (α : S) → (∀ β → β ∈ᵗ α → S) → S LsetStep α rec = ⋃ (sett ⟪ α ⟫ (λ m → 𝒟ₒ (rec (⟪ α ⟫↪ m) (mem m))))
補助関数 mem が本体に必要な変換を供給します。添字 m の指す α の要素は ⟪ α ⟫↪ m であり、∈ₛ⟪ α ⟫↪ m がこの集合が小さな表現で α に属することを証明します。そして ∈∈ₛ がそれを、rec が期待する型としての所属 ∈ᵗ へ変換します。塔そのものはただ一度の呼び出しです。Lset はステップ関数に ∈-induction を適用したものとして定義されます。これは所属に沿った整礎再帰であり、その正当性は階層の章の正則性の定理が一度に与えます。再帰の添字は集合 α そのものであり、素の定義は添字の順序数性を要求しません。順序数性が課されるのは、この階層を使う場所においてです。
where mem : (m : ⟪ α ⟫) → ⟪ α ⟫↪ m ∈ᵗ α mem m = ∈∈ₛ {a = ⟪ α ⟫↪ m} {b = α} .snd (∈ₛ⟪ α ⟫↪ m) opaque Lset : S → S
𝒟ₒ と Lset はそれぞれ固有の opaque ブロックで包まれるため、両者の Agda の項は型検査のあいだ抽象的なままです。再帰の仕組みの内側、つまりある到達可能性の消去子で何が展開されようと、それが後の変換に漏れ出すことはありません。盲目的な展開の代わりとなるのが、宣言された計算規則です。Lset-compute は、Lset α が α と再帰値 λ β _ → Lset β にステップを適用したものに等しいことを、命題としてのパスとして述べます。これは階層の章の ∈-induction-compute をこのステップで実例化した恰好であり、この等式は定義的に成り立つとは限りません。明示的に述べておくことで、以後の証明は再帰の仕組みを開く代わりに、この一本の制御された等式で Lset α を書き換えられます。
Lset = ∈-induction LsetStep opaque unfolding Lset Lset-compute : (α : S) → Lset α ≡ LsetStep α (λ β _ → Lset β) Lset-compute = ∈-induction-compute LsetStep
塔のすべての値は層です。まず Lset-compute で一度展開し、各要素に帰納仮定を適用し、𝒟ₒ-layer で一段上げ (不透明な定義が展開されるのはまさにここだけです)、最後に setUnion-layer によって族の和が再び層であると結論します。
演算子から述語への橋渡しは一行で済みます。𝒟ₒ を展開するブロックの内側では、𝒟ₒ-layer という主張は文字どおり構成子 𝒟-layer です。𝒟ₒ A は 𝒟 A へ簡約されるからです。本章で不透明な包みの内側を見る必要があるのはここだけで、これ以後は演算子のすべての使用が抽象的なままで済みます。目標 Lset-layer は、塔がまるごと帰納的述語の内側に落ちること、すなわちすべての段階 Lset α が層であることを言います。その証明自体が、塔を定義したのと同じ原理である所属帰納の適用です。
opaque unfolding 𝒟ₒ 𝒟ₒ-layer : ∀ {A} → isLayer A → isLayer (𝒟ₒ A) 𝒟ₒ-layer = 𝒟-layer Lset-layer : (α : S) → isLayer (Lset α)
この帰納のステップ関数は α と、α の各要素 β に対して Lset β が層であることを与える帰納仮定 IH を受け取ります。Lset は不透明なので、目標 isLayer (Lset α) は構成子と直接照合できず、まず輸送されなければなりません。等式 Lset-compute α が Lset α をステップの和集合と同一視し、subst isLayer (sym (Lset-compute α)) がそのパスに沿って目標を正しい向きへ移すので、目標は isLayer (⋃ (sett ⟪ α ⟫ (λ m → 𝒟ₒ (Lset (⟪ α ⟫↪ m))))) になります。これはまさに塔のステップ関数が作った族です。
Lset-layer = ∈-induction step where step : (α : S) → (∀ β → β ∈ᵗ α → isLayer (Lset β)) → isLayer (Lset α) step α IH = subst isLayer (sym (Lset-compute α)) (setUnion-layer ⟪ α ⟫ (λ m → 𝒟ₒ (Lset (⟪ α ⟫↪ m)))
残りの義務は族の構成子に正確にはまります。setUnion-layer は族と、その各値に対する層の証明を要求します。添字 m に対する値は Lset (⟪ α ⟫↪ m) での 𝒟ₒ であり、局所的な補助 mem によって型としての所属へ変換されたうえでその要素に適用した帰納仮定 IH が isLayer (Lset (⟪ α ⟫↪ m)) を与え、𝒟ₒ-layer がそれを定義可能冪集合の一段へ引き上げます。Lset の不透明な包みは宣言された等式を通してのみ開かれ、𝒟ₒ の包みは 𝒟ₒ-layer の内側でのみ開かれるので、帰納全体が塔の意図された読みのレベルで進みます。前節と合わせれば、すべての段階は推移的な層です。
(λ m → 𝒟ₒ-layer (IH (⟪ α ⟫↪ m) (mem m)))) where mem : (m : ⟪ α ⟫) → ⟪ α ⟫↪ m ∈ᵗ α mem m = ∈∈ₛ {a = ⟪ α ⟫↪ m} {b = α} .snd (∈ₛ⟪ α ⟫↪ m)
段階の比較
塔についてさらに二つの事実があります。第一は演算子の所属に名前を与えます。𝒟ₒ A は A の定義可能部分集合の集合なので、それに属することは構成上「ある defSet φ である、と単に」であり、論理式を一つ、外延的な等式とともに示せば、集合を演算子の中へ置くのにちょうど十分です。第二は塔を一度展開し、和集合を両方向から読みます。段階とは、添字の要素にわたる前段階の 𝒟ₒ の和集合であり、したがって段階に属することは、ある前段階の 𝒟ₒ に属することに他なりません。これは二つの独立な方向として述べられます。単調性はその後、別個の構成ではなく帰結として従います。
𝒟ₒ を展開するブロックの内側では、𝒟ₒ A への所属は Def の定義的性質に帰着します。𝒟ₒ A の要素とは、A の小さな要素の上でのアリティ 1 の論理式 φ が選び出す A の部分集合であり、実際の集合はパス DefOf.defSet A φ ≡ x によって特定されます。周囲の階層での所属は命題的に切り詰められているため、主張には命題的切り詰めが冠されます。断言されるのはそのような論理式が単に存在することであって、一つが選ばれていることではありません。以下の二つの補題は、この同値をそれぞれ一方向ずつ述べるものです。ここでは導入の方向が宣言され、切り詰められた定義データを所属へ取ります。
opaque unfolding 𝒟ₒ 𝒟ₒ-intro : (A x : S) → ∥ Σ[ φ ∈ Formula ⟪ A ⟫ 1 ] (DefOf.defSet A φ ≡ x) ∥₁ → ⟨ x ∈ˢ 𝒟ₒ A ⟩
証明の本体は両方向とも恒等写像です。𝒟ₒ を展開すれば、命題的に切り詰められた定義データの要素はもともと要素であり、逆に反転の補題 𝒟ₒ-inv は所属を同じ切り詰められたデータとして返します。したがって 𝒟ₒ-intro と 𝒟ₒ-inv の対は、直前述べたインターフェイスそのものです。段階における DefOf.defSet を論理式からの写像として読み、反転によって要素の定義論理式を取り戻します。どちらも「単に存在する」のレベルで働くため、標準的な論理式が選ばれることはありません。𝒟ₒ A の要素は単に何らかの定義可能部分集合であるだけであり、この二方向が言うのはそれだけです。
𝒟ₒ-intro A x p = p 𝒟ₒ-inv : (A x : S) → ⟨ x ∈ˢ 𝒟ₒ A ⟩ → ∥ Σ[ φ ∈ Formula ⟪ A ⟫ 1 ] (DefOf.defSet A φ ≡ x) ∥₁ 𝒟ₒ-inv A x p = p
塔を後の議論で使うために、さらに二つの事実を示します。第一は演算子の所属に名前を与えます。𝒟ₒ A は A の定義可能部分集合の集合なので、それに属することは構成上「ある defSet φ である、と単に」であり、論理式を一つ、外延的な等式とともに示せば、集合を演算子の中へ置くのにちょうど十分です。第二は塔を一度展開し、和集合を両方向から読みます。段階とは、添字の要素にわたる前段階の 𝒟ₒ の和集合であり、したがって段階に属することは、ある前段階の 𝒟ₒ に属することに他なりません。これは、証明がそう使うために、二つの独立な方向として述べられます。単調性はその後、別個の構成ではなく帰結として従います。
最初の補題は、段階がその固有の定義可能冪集合に含まれるという包含です。Lset-layer β が段階 Lset β が層であることを言い、layer-trans がそれを推移的にするので、定義可能性の章の細分の評価 A⊆Def がそのまま適用され、x ∈ Lset β ⟹ x ∈ 𝒟ₒ (Lset β) が得られます。双対の 𝒟ₒ∋⊆ は、演算子が細分するだけで要素を失わないことを再確認します。𝒟ₒ A の各要素は A の部分集合なので、その要素の要素も依然 A にあります。最後に stageFam が、塔のステップの下にある族に名前を与えます。α の小さな表現の添字 m に対して、対応する段階は m の指す要素での Lset に 𝒟ₒ を施したものです。
Lset⊆𝒟ₒ : (β x : S) → ⟨ x ∈ˢ Lset β ⟩ → ⟨ x ∈ˢ 𝒟ₒ (Lset β) ⟩ Lset⊆𝒟ₒ β x = DefOf.Refine.A⊆Def (Lset β) (layer-trans (Lset-layer β)) x 𝒟ₒ∋⊆ : (A x : S) → ⟨ x ∈ˢ 𝒟ₒ A ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ A ⟩ 𝒟ₒ∋⊆ A = DefOf.Def∋⊆A A stageFam : (α : S) → ⟪ α ⟫ → S
次に、段階への所属を上から特徴づけます。Lset-in の主張は、δ が α の要素であり x が 𝒟ₒ (Lset δ) に属するなら、x はすでに Lset α に属する、ということです。証明はまず計算規則で Lset α を一度書き換え、目標を和集合 ⋃ (sett ⟪ α ⟫ (stageFam α)) への所属に変えます。そして union-family-in を呼びます。これはモデル章の補題で、添字 i と f i の要素 x を受け取り、添字付きの和の要素を返します。供給される添字は fib .fst、すなわち ⟪ α ⟫ のうち要素 δ を名指す元です。
stageFam α m = 𝒟ₒ (Lset (⟪ α ⟫↪ m)) Lset-in : (α δ x : S) → ⟨ δ ∈ˢ α ⟩ → ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩ → ⟨ x ∈ˢ Lset α ⟩ Lset-in α δ x δ∈α x∈𝒟ₒδ = subst (λ w → ⟨ x ∈ˢ w ⟩) (sym (Lset-compute α)) (union-family-in ⟪ α ⟫ (stageFam α) (fib .fst) x
名前 fib はファイバーの計算の略記です。構造的な所属 δ∈α は命題的に切り詰められていますが、∈-asFiber がそれを埋め込み ⟪ α ⟫↪ のファイバーへ変換します。つまり添字 i と ⟪ α ⟫↪ i ≡ δ というパスの対です。証明の内側ではこの同一視に沿って輸送が行われます。x∈𝒟ₒδ は Lset δ について述べていますが、union-family-in が必要とするのは stageFam α (fib .fst) の要素であり、これは 𝒟ₒ (Lset (⟪ α ⟫↪ (fib .fst))) に等しいので、subst がパス sym (fib .snd) を横断して仮定を移します。δ∈α が切り詰められたものであることはここでは問題になりません。∈-asFiber が実際にそこからファイバー表現を構成したからです。
(subst (λ δ → ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩) (sym (fib .snd)) x∈𝒟ₒδ)) where fib = ∈-asFiber {a = δ} {b = α} δ∈α Lset-out : (α x : S) → ⟨ x ∈ˢ Lset α ⟩ → ∥ Σ[ δ ∈ S ] (⟨ δ ∈ˢ α ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩) ∥₁
下向きの方向 Lset-out は命題的切り詰めを避けられず、それを率直に述べます。Lset α の要素 x は、ある前駆から単に来ています。すなわち δ ∈ α かつ x ∈ 𝒟ₒ (Lset δ) なる δ が単に存在するということです。証明はここでも計算規則で Lset α を書き換え、union-family-out を適用して、⟪ α ⟫ の添字 m でその位置の族の値に x が属することが単に成り立つことを得ます。そして切り詰めの内部で写像を行います。対 (m , hx) は、段階 ⟪ α ⟫↪ m、∈∈ₛ による α への構造的な所属、そして hx になります。結果が切り詰められた証人になるのは、和集合の公理が標準的な前駆を名指さないからにほかなりません。分岐の内側で構成した一つは局所的なデータであって、選ばれた関数ではありません。
Lset-out α x x∈Lα = PT.map (λ { (m , hx) → ⟪ α ⟫↪ m , (∈∈ₛ {a = ⟪ α ⟫↪ m} {b = α} .snd (∈ₛ⟪ α ⟫↪ m) , hx) }) (union-family-out ⟪ α ⟫ (stageFam α) x (subst (λ w → ⟨ x ∈ˢ w ⟩) (Lset-compute α) x∈Lα))
単調性はこれで、別個の構成ではなく特徴づけの短い帰結になります。β ∈ α かつ x ∈ Lset β なら、まず Lset⊆𝒟ₒ が x を 𝒟ₒ (Lset β) へ引き上げます。段階が推移的であることを使います。次に包含 β ∈ α とともに Lset-in を適用して、x を Lset α へ運びます。厳密な形に注意してください。単調性が要求するのは β が α の部分集合であることではなく要素であることであり、これは塔が要素にわたる和集合を取って伸びる仕方と一致します。
Lset-mono : {α β : S} → ⟨ β ∈ˢ α ⟩ → {x : S} → ⟨ x ∈ˢ Lset β ⟩ → ⟨ x ∈ˢ Lset α ⟩ Lset-mono {α} {β} β∈α {x} x∈Lβ = Lset-in α β x β∈α (Lset⊆𝒟ₒ β x x∈Lβ)
クラス L とその構造
集合が構成可能であるとは、塔のある順序数段階がそれを含むことです。順序数の上限を定義に意図的に書き込むのは、後の理論が段階の順序数を取り出す必要があるためであり、この形はそれを構成によって直接与えます。順序数性が課されるのはまさにこの定義の箇所であることに注意してください。塔 Lset そのものは任意の集合を添字として受け付けます。L は推移的クラスです。段階は推移的であり、証人となる順序数は動きません。
このクラスは部分型ではなく真理値です。isL x は、すべての集合 α にわたる索引付きの選言 ∃[ x ] P x として定義され、その各項は IsOrd α と x ∈ˢ Lset α の連言です。したがって添字付き選言の意味により、isL x の要素は単に、順序数 α と段階 α への x の所属の対です。構成可能集合に標準的な段階が付属することはありません。量詞は台全体にわたるため、証人はこの「単に存在する」の形でしか得られません。クラスを命題値の述語として扱うことが、まもなくそれを構造へ制限できる理由です。
isL : S → hProp (ℓ-suc ℓ) isL x = ∃[ α ∶ S ] ((IsOrd α , isPropIsOrd α) ⊓ (x ∈ˢ Lset α)) isL-trans : Transitive 𝒮ᵥ isL isL-trans {x} {y} y∈x x∈L = PT.rec (snd (isL y)) (λ { (α , (ordα , x∈Lα)) →
クラスの推移性は、段階の閉性からただちに従います。y ∈ x と isL x の要素が与えられ、命題的に切り詰められたものを命題 isL y へ消去します。証人は対 (α , ordα , x∈Lα) であり、段階 Lset α は layer-trans (Lset-layer α) により推移的集合なので、二つの仮定 y∈x と x∈Lα から y ∈ Lset α が得られます。同じ順序数 α が結論を改めて証明するので、クラスは要素の要素について閉じています。結論を ∣ _ ∣₁ で改めて切り詰めるのは、目標 isL y それ自体が切り詰められた存在式だからであって、どの選択を取り消す必要があったからではありません。
∣ α , (ordα , layer-trans (Lset-layer α) y∈x x∈Lα) ∣₁ }) x∈L
ある順序数段階に属することこそ定義そのものなので、この方向の橋は構成子そのものです。この橋に名前を与えるのは、引用しやすくするためです。
段階 α の順序数の証人 oα と所属 x∈Lα が与えられれば、証明は三つの成分、順序数、その順序数性、所属、を一つの命題的に切り詰められた対へまとめます。計算されるものは何もありません。この補題の内容は、isL x の定義にある存在式が、まさに手元のデータによって証明されるということです。信頼の向きに注意してください。この補題は α の順序数性を仮定として受け取ります。定義上の Lset は任意の集合を添字として受け付けるため、選んだ添字が本当に順序数であることは呼び出し側が知っていなければならないからです。
Lset→isL : (α : S) → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ isL x ⟩ Lset→isL α oα x x∈Lα = ∣ α , (oα , x∈Lα) ∣₁
最後に、構成可能クラスを一つの構造として捉えます。𝒮ᵥ を命題値のクラス isL に制限して得られるのが 𝒮ʟ です。その元は構成可能性の証明を伴う集合であり、等式と所属は制限を通して受け継がれます。これが後に L についての論理式を解釈する構造になります。これを ZFC のモデルと示すには、続く各章の公理ごとの議論が別に必要です。
一行で十分です。制限 _↾_ は周囲の構造とクラス isL を受け取り、isL を満たす証拠と対になった集合を要素とする構造を作ります。等号と所属は第一射影に沿って読まれるため、周囲のものと一致します。isL は hProp の真理値であり、クラスは推移的であると証明済みなので、制限された構造は同じ枠組みのなかで問題なく定義されます。まだ開いている問題、すなわち後の章の主題は、この構造が ZF と ZFC の公理を満たすかどうかです。制限そのものはそれについて何も主張しません。
𝒮ʟ : ZFStructure (ℓ-suc ℓ) 𝒮ʟ = 𝒮ᵥ ↾ isL
まとめ
塔 Lset は所属再帰で定義され、isLayer は定義可能性の演算と三種類の和集合構成に関する閉包性を記録します。層の証拠に対する構造的再帰と対応する補題から layer-trans が得られます。集合が isL に属するとは、ある順序数 α に対して Lset α に単に属することです。このクラスは推移的であり、周囲の構造をそこへ制限すると 𝒮ʟ が得られます。残る課題は、この構造が ZFC を満たすことを公理ごとに証明することです。