BedrockL における冪集合
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ構成可能集合 a の L 内部での冪集合は、何を集めるべきでしょうか。モデルの量化子はその台S 上を動くので、必要な要素は、内部の包含 x ⊆ˢ a を満たす構成可能なモデル要素x です。周囲の階層は基底の集合 A = fst a の冪集合を作れますが、その所属条件は V ℓ 全体にわたり、構成可能性を要求しません。したがって、その周囲の冪集合は添字を供給できますが、L の冪集合としてそのまま返すことはできません。
証明は三段階で進みます。まず周囲の冪集合からすべての候補の小さな表示を得ます。次に、構成可能な候補を表示する添字を残し、それらの段階を一つの順序数 β で抑えます。最後に Lset β の内部で分出を行い、a に内部的に含まれるモデル要素だけを集めます。ホスト側の構成が上界を与え、最終的な集合そのものは構成可能モデル内で作られます。
{-# OPTIONS --cubical --safe --guardedness #-}
構成には二種類の小ささが必要です。命題リサイズは、モデルの真理値のレベルにある命題を、小さな添字のレベルにある同値な命題へ置き換えます。非可述性のパッケージはさらに、小さな命題のための小さな分類子を与え、周囲の階層で冪集合を作れるようにします。どちらも排中律から導かれますが、解決する大きさの問題は異なります。命題リサイズは構成可能性を小さな添字型に収め、分類子はその添字を供給する周囲の冪集合を構成します。
open import Base.Prelude open import Base.Classical using ( LEM; lem→resizing; lem→ΩResizing )
宇宙レベル ℓ と、ただ一つの仮定 lem : LEM (ℓ-suc ℓ) を固定します。目標のモデルフィールドは、L の各 a に対して、a に内部的に含まれるモデル要素をちょうど要素とするモデル要素が一意に存在する、と述べます。一意性はホスト型 isContr にまとめられます。対象理論での内容は冪集合公理であり、その一意性は外延性から従います。同じ一つの lem が、命題リサイズ、周囲の冪集合のための小さな分類子、正準な段階の関数、完全な分出で用いる反映という四つの経路を通って証明に入ります。別の古典的仮定は加わりません。
module L.Axioms.Power {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
証明では三つの水準を区別します。ホスト型は添字と証明を組織します。周囲の構造 𝒮ᵥ の要素は累積階層のすべての集合です。制限された構造 𝒮ʟ の要素は、周囲の集合とその構成可能性の証拠との対です。論理式の言語は、𝒮ʟ の内部で包含を表すための有界全称量化子を備えています。したがって周囲の構造は部分集合の候補を列挙でき、対象理論の冪集合公理は制限された構造の中で証明されます。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; ∀̇∈ ) import FOL.Absoluteness import FOL.ZFModel open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
周囲の階層は、A の周囲でのすべての部分集合を含む集合 𝒫V A と、その所属の仕様を与えます。構成可能階層は段階 Lset α とその厳密な単調性を与えます。すなわち α ∈ β なら、前の段階への所属を後の段階へ持ち上げられます。各構成可能な候補には、段階の関数が、その候補を含む段階の正準な順序数添字を与えます。上界補題は、この小さな順序数添字の族を一つの順序数の真に下へ収めます。段階の関数は最小性も証明しますが、本章で使うのは順序数性と段階への所属だけです。
open import V.Model {ℓ} using ( module Power ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono ) open import L.Ordinal {ℓ} using ( boundingOrd ) open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
順序数の上界 β が得られると、LsetS β oβ は、考えている内部部分集合をすべて含むと分かっているモデル要素になります。したがって、残る数学的操作は、包含を表す一変数論理式による分出です。一般定理 hasSeparationL は任意の論理式を受け取ります。反映する段階を見つけ、その段階で論理式を有界な相対化に置き換え、有界な分出を適用します。ここでの論理式はすでに Δ₀ ですが、この呼び出しは実際にこの一般的な経路を通ります。そのため、この有界な場合にも、論理式の反映とパラメータの段階の構成は、同じ lem の実際の使用です。
open import L.Axioms.Basic {ℓ} using ( LsetS ) open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
階層の各集合は小さな表現を持ちます。添字型 ⟪P⟫ と、その要素を呈示する埋め込み ⟪P⟫↪ です。P への所属は、この埋め込みのファイバーの命題的切り詰めとして定義されます。写像が埋め込みなので各ファイバーはすでに命題であり、∈-asFiber は選択公理を使わずに添字とそれを特定するパスを復元できます。同値の二方向は、リサイズされた命題と元の命題との間の往復にも使われます。最後には命題外延性が、二方向の含意を真理値の間のパスへ変えます。
open import Cubical.Foundations.Equiv using ( _≃_; invEq; equivFun ) open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈-asFiber; ⟪_⟫; ⟪_⟫↪ )
𝒮ʟ を開くと、以下で修飾なしに書く台 S と所属関係は構成可能モデルのものになります。S の要素は、構成可能な集合とその構成可能性の証拠との対であり、fst は証拠を忘れて周囲の集合を返します。パラメータ ℓ は ⟪P⟫ のような小さな表現型のレベルを支配し、V ℓ、台 S、二つの構造の真理値は ℓ-suc ℓ に住みます。したがって後の小ささの議論は添字型についてのものであり、モデルの台についてのものではありません。
open hPropStructure 𝒮ʟ
二つのモデルのインターフェースは、同じ記法を持ちながら量化域の異なる二つの部分集合関係を与えます。ModelL の x ⊆ˢ a は S 上で量化するため、構成可能な要素だけを調べます。ModelV の対応する関係は V ℓ のすべての集合上で量化します。任意の左辺に対しては後者の方が強い条件です。左辺自身が構成可能なら、L の推移性によってその周囲での各要素を S の要素にでき、内部の包含から周囲の包含への、以下で必要となる正確な橋が得られます。
module ModelL = FOL.ZFModel 𝒮ʟ open ModelL using ( SetOf; _⊆ˢ_ ) module ModelV = FOL.ZFModel 𝒮ᵥ
ここでの記法 _⊨_ は、台 S 上の論理式を制限された構造 𝒮ʟ で評価する内側の充足関係です。定数はそれが名指すモデル要素を表し、制限された所属関係は、その第一射影を周囲の階層で読みます。同じモジュールは外側の読み方も与えますが、本章では絶対性定理を適用しません。ここで使う充足の主張は、有界な包含論理式のモデル内部での直接の意味だけです。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
周囲の冪集合の構成には、lem→ΩResizing lem から得られる小さな分類子を与えます。ここで使うのは ΩResizing から導かれる分類子だけです。特性関数を小さな真理値コードの型への関数として表し、それに対応する階層の集合を作ります。isL の命題リサイズは別の操作であり、この具体化には入りません。二つの役割を分けることで、後の小さな添字の構成が明確になります。
module Pow = Power (lem→ΩResizing lem)
包含条件を論理式にする
a : S に対して、論理式 subFo a は候補 x のための自由な枠を一つ持ち、
「すべての y ∈ x について y ∈ a」
と読みます。二つの var zero は異なる文脈にあります。有界全称量化子の外側では候補 x を表し、その本体では新しく束縛された要素 y を表します。定数域がモデルの台なので、con a は a を直接名指せます。環境 x ∷ [] では、有界全称の意味論はそのまま x ⊆ˢ a に簡約されます。これは内部の包含であり、y は構成可能モデルの要素だけを動きます。この論理式は Δ₀ ですが、後の証明では一般の分出インターフェースに渡されます。
subFo : S → Formula S 1 subFo a = ∀̇∈ (var zero) (var zero ∈̇ con a)
構成可能な部分集合を抑える
a : S を固定します。その第一射影 A は、構成可能性の証拠を忘れて、同じ集合を周囲の階層で見たものです。集合 P = Pow.𝒫V A は、周囲での完全な冪集合の仕様を満たします。P への所属に必要なのは周囲の意味で A に含まれることだけであり、構成可能性の仮定はありません。したがって、構成可能でない周囲の部分集合があれば、それも P に属します。また、この構成から P 自身の構成可能性は得られません。証明が使うのは小さな表示 ⟪P⟫ だけであり、後でその添字を構成可能性によって選び出します。P はモデルで最終的に返される冪集合ではありません。
module Bound (a : S) where private A P : V ℓ A = fst a P = Pow.𝒫V A
周囲の集合 v に対する構成可能性 isL v は、レベル ℓ-suc ℓ の命題です。具体的には、v を含む順序数段階が存在するという主張の命題的切り詰めです。この命題は、レベル ℓ の型の第二成分に置くには大きすぎます。そこで rsz は、小さな命題 Q : hProp ℓ と、その基礎型と isL v との同値を与えます。変わるのは真理値の宇宙レベルだけです。命題的切り詰めを除去することも、順序数段階を選ぶこともありません。
rsz : (v : V ℓ) → Σ[ Q ∈ hProp ℓ ] (⟨ isL v ⟩ ≃ ⟨ Q ⟩)
rsz v = lem→resizing lem (isL v)
ホスト型 Ix は、周囲の冪集合のうち構成可能な要素をちょうど添字づけます。その要素は、A の周囲での部分集合を呈示する添字 m : ⟪P⟫ と、呈示された集合についてリサイズされた構成可能性命題の証明との対です。両成分が小さいため Ix : Type ℓ となり、順序数の上界補題がその上で量化できます。Ix はホスト側の添字型にすぎません。L の要素でも、対象言語の論理式で定義されたクラスでもなく、最終的な冪集合にもなりません。
Ix : Type ℓ Ix = Σ[ m ∈ ⟪ P ⟫ ] ⟨ rsz (⟪ P ⟫↪ m) .fst ⟩
i : Ix の段階を得るため、まず元の構成可能性命題を復元します。リサイズの同値の逆写像は、i.snd を小さな命題から isL (⟪P⟫↪ i.fst) へ戻します。得られる主張は依然として、ある順序数段階が呈示された集合を含むという命題的切り詰めにとどまります。したがって unres は宇宙レベルの変更を逆にするだけで、切り詰めから証人を取り出しません。確定した段階の添字を得るための追加の仕事は、次の定義が行います。
private unres : (i : Ix) → ⟨ isL (⟪ P ⟫↪ (i .fst)) ⟩ unres i = invEq (rsz (⟪ P ⟫↪ (i .fst)) .snd) (i .snd)
関数 stg は Ix の各項に正準な段階の添字を割り当てます。これは、呈示された集合が Lset σ に属するような最小の順序数 σ です。この古典的な段階は命題リサイズとは別です。内部で stage は整礎的な降下を行い、より小さな証人が存在するかを排中律で判定します。命題的切り詰めを除去する先は LeastOrd だけであり、その型が命題であることは順序数の三分律と残りの証拠の一意性から示されます。したがって確定した順序数添字は得られますが、任意の切り詰められた証人からデータを取り出す一般則は得られません。本章で使うのは stage-ord と stage-mem だけで、最小性は使いません。
stg : Ix → V ℓ stg i = stage (⟪ P ⟫↪ (i .fst)) (unres i)
ここで stg : Ix → V ℓ は実際に小さな族となり、stage-ord が各値は順序数であることを示します。補題 boundingOrd は、順序数 β と、各 stg i が β に属するという証明を明示的なデータとして返します。この構成はホスト理論で、与えられた順序数の後続を取り、続いてそれらの和集合を取ることで行われます。L の内部で置換を適用するのではなく、本章では置換のフィールドを一度も使いません。この厳密な上界は、後で Lset-mono が要求する形そのものです。
b = boundingOrd Ix stg (λ i → stage-ord (⟪ P ⟫↪ (i .fst)) (unres i))
上界データの第一射影を β と名づけます。これはホスト側の構成で得られた周囲の階層の集合であり、次の証明が順序数であることを示します。後でモデル要素としてまとめられるのは段階 Lset β、すなわち LsetS β oβ であり、β 自身をモデルに入れる必要はありません。また β は、a 自身の段階だけではなく、A の周囲での構成可能なすべての部分集合の段階に依存します。このように候補の族全体に依存する上界で冪集合公理には十分なので、凝縮による精密な評価は必要ありません。
β : V ℓ β = b .fst
証明 oβ は、上界が順序数であることを記録します。b.snd のもう一つの成分は後で b.snd.snd i として使われ、各 i : Ix に対して stg i ∈ β を述べます。これは順序数添字の厳密な所属です。stage-mem : presented-set ∈ Lset (stg i) が与えられると、Lset-mono はまさにこの所属を用いて、呈示された集合を Lset β へ持ち上げます。順序数性とこの厳密な上界性が、以下で β について必要となる二つの事実です。
oβ : IsOrd β oβ = b .snd .fst
補題 below は上界の本質的な被覆性を述べます。x : S が a に内部的に含まれるなら、その底となる周囲の集合 fst x は Lset β に属します。証明ではまず、fst x を P の要素を呈示する適切な添字 i : Ix と同一視します。stage-mem により候補は Lset (stg i) に属し、stg i ∈ β に沿って Lset-mono を使えば、この所属を Lset β へ持ち上げられます。最後の subst は、呈示のパスに沿って結果を fst x へ運びます。以下の局所定義が、この特定の i の存在と必要な性質を示します。
below : (x : S) → ⟨ x ⊆ˢ a ⟩ → ⟨ fst x ∈ Lset β ⟩ below x x⊆a = subst (λ w → ⟨ w ∈ Lset β ⟩) pa (Lset-mono {α = β} {β = stg i} (b .snd .snd i) (stage-mem _ (unres i))) where
添字を得るため、まず内部の包含を周囲の包含へ変えます。周囲での任意の要素 v ∈ fst x に対し、構成可能性の推移性は x.snd から isL v を導きます。そこでモデル要素 (v , proof) に x⊆a を適用すると v ∈ A が得られます。したがって fst x は周囲で A の部分集合であり、Pow.power-spec の逆方向がこの包含を fst x ∈ P に変えます。P への所属は表現のファイバーの命題的切り詰めですが、表現写像は埋め込みなので、そのファイバー自体が命題です。よって ∈-asFiber は実際の表現添字と、その像を fst x と同一視するパス pa を返せます。これは一意性によって許される切り詰めの除去であり、選択公理の適用ではありません。
vsub : ⟨ ModelV._⊆ˢ_ (fst x) A ⟩ vsub v v∈ = x⊆a (v , isL-trans {x = fst x} {y = v} v∈ (x .snd)) v∈ fib = ∈-asFiber {a = fst x} {b = P} (subst ⟨_⟩ (sym (Pow.power-spec A (fst x))) vsub) pa : ⟪ P ⟫↪ (fib .fst) ≡ fst x
パス pa によって、復元した表現添字を Ix の要素へ完成できます。第一成分は fib.fst です。第二成分については、sym pa に沿って x.snd : isL (fst x) をその添字が呈示する集合の構成可能性へ運び、リサイズ同値の順写像でこの命題をレベル ℓ に符号化します。したがって i は x と同じ底集合を持つ候補を実際に添字づけ、その段階は β で抑えられた族の一つです。stage-mem、b.snd.snd i、Lset-mono を組み合わせ、最後に pa に沿って運ぶと、below の結論が得られます。
pa = fib .snd i : Ix i = fib .fst , equivFun (rsz (⟪ P ⟫↪ (fib .fst)) .snd) (subst (λ w → ⟨ isL w ⟩) (sym pa) (x .snd))
冪集合フィールド
hasPowerL の型は、証明すべきモデル論的な主張をそのまま述べています。すべてのx : S において所属述語が x ⊆ˢ a であるような実現者 p : S からなる型が可縮であることを要求します。この段階で、周囲の集合 P は役目を終えています。Bound.β a を構成するための添字の族を供給しましたが、結論には現れません。
hasSeparationL をモデル要素 LsetS (Bound.β a) (Bound.oβ a) に適用すると、まず、x がこの段階に属し、かつ subFo a を満たすという、見かけ上より強い述語に対する可縮な SetOf が得られます。残る仕事は、この述語が内部の包含に等しいと示すことだけです。局所的な等式 Q≡ がその同一視を与え、外側の subst が可縮なパッケージを冪集合のフィールドが要求する述語へ輸送します。
hasPowerL : (a : S) → isContr (SetOf (λ x → x ⊆ˢ a)) hasPowerL a = subst (λ Q → isContr (SetOf Q)) Q≡ (hasSeparationL (LsetS (Bound.β a) (Bound.oβ a)) (subFo a)) where
残る等式は、分出によって切り出されたクラスと、冪集合フィールドが要求するクラスを比較します。左辺は、x が上界となる段階に属し、かつ subFo a を満たすと述べます。後半の充足命題は、内部の包含 x ⊆ˢ a に簡約されます。したがって順方向の証明は、段階への所属を表す成分を捨てます。逆方向では、x ⊆ˢ a に Bound.below を適用してその成分を補います。命題外延性は二方向の含意を各 x におけるパスへ変え、関数外延性はそれらのパスを述語の等式 Q≡ にまとめます。最外側の subst は、この等式に沿って、分出が与えた実現者の可縮な型を輸送します。Q≡ 自体は集合の外延性を使いません。分出がまとめた一意性の中ですでに使われています。
したがって hasPowerL a は、対象理論の冪集合公理を正確なモデル論的形式で証明します。これは要素 p : S からなる可縮な型を与え、すべての x : S について、所属命題 x ∈ˢ p が内部の主張 x ⊆ˢ a と同値であることを示します。p も候補となる各 x も、構成可能モデルの台の上で量化されています。前に用いた周囲の階層の冪集合は、候補の小さな添字を与えるだけであり、ここで得られる集合ではありません。ただ一つの仮定 LEM (ℓ-suc ℓ) は、命題リサイズ、小さな分類器、命題的切り詰めを施した構成可能性からの標準的な段階の選択、そして完全分出が用いる反映を通じて、この構成に届きます。
Q≡ : (λ x → (x ∈ˢ LsetS (Bound.β a) (Bound.oβ a)) ⊓ ((x ∷ []) ⊨ subFo a)) ≡ (λ x → x ⊆ˢ a) Q≡ = funExt (λ x → ⇔toPath (λ { (_ , x⊆a) → x⊆a }) (λ x⊆a → Bound.below a x x⊆a , x⊆a))
まとめ
この構成には、明確に異なる三つの役割があります。周囲の冪集合が小さな表示を供給し、ホスト理論がその構成可能な要素の段階を抑え、内部の分出がその上界から求める集合を切り出します。L.Model は hasPowerL を L⊨ZF の hasPower フィールドに組み込み、その後レコードが内部演算 𝒫 を定義します。後の GCH の議論は、この演算と仕様 ℩-spec (hasPower κ) を使って所属と内部の包含の間を往復します。補助的な周囲の Pow.𝒫V を使うことはありません。
論理的な依存関係も具体的です。唯一の仮定 LEM (ℓ-suc ℓ) が、小さな分類子、命題リサイズ、正準な段階の構成、および完全な分出のための論理式の反映を支えます。この証明では、選択、置換のフィールド、凝縮のいずれも使いません。