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