Bedrock後続基数を冪集合へ単射する
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップL の内部での Cantor の定理は、𝒫 κ から κ への内部的に符号化された単射を排除します。この章では、κ の後続基数 δ と、別に与えられた比較 InjL (𝒫 κ) δ から、逆向きの比較 InjL δ (𝒫 κ) を構成します。ここで InjL a b は、a から b への単射を符号化する L のグラフが存在することの命題的切り詰めです。証明では、δ 上の順序数の順序を与えられた単射に沿って 𝒫 κ へ引き戻し、その順序を順序数 μ へ崩壊して、Cantor の障害から μ が δ に属しえないことを示します。
{-# OPTIONS --cubical --safe --guardedness #-}
古典的推論は、明示的なパラメータ lem を通して導入されます。順序数の三分法が証明中の目に見える場合分けを与え、ここで用いる分出定理と符号化された単射に関する結果も、同じ仮定のもとで具体化されています。したがって、この章の古典的な依存は一箇所に明記されています。
open import Base.Prelude open import Base.Classical using ( LEM )
排中律の仮定は ℓ-suc ℓ のレベルに置かれます。集合と符号化されたグラフに関する必要な命題が、このレベルに属するためです。したがって、以下の古典的な比較はすべて、この一つのパラメータに遡れます。
module L.GCH.SuccessorIntoPowerSet {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
対角部分集合と後で用いる引き戻し順序は、ともに L の集合でなければなりません。そこで、構成可能モデルで解釈される一階の論理式によって両者を記述します。ここで用意される構文は、所属・連言・否定と、これらの関係を表すために必要な有界または非有界の存在証人を表現できます。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _∧̇_; ¬̇_; ∃̇_; ∃̇∈ ) import FOL.ZFModel import FOL.Absoluteness
引き戻し順序の整礎性は、その下降の各段階を周囲の累積階層における所属の一段階へ移し、そこで正則性を適用して証明します。続いて、構成可能な順序数についての事実により、順序数の下への所属から比較に必要な順序数構造を得ます。
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV ) open import V.Coding {ℓ} using ( pr ) open import L.Constructible {ℓ} using ( 𝒮ʟ; IsOrd; isL; isL-trans; isTransV; isPropIsTransV ) open import L.Ordinal {ℓ} using ( mem-ord )
内部の大きさの比較には二つの層があります。InjCode F a b は特定の構成可能なグラフとその単射の法則を保持しますが、InjL a b はそのような符号が存在するという命題的切り詰めだけを保持します。後続基数の最小性、符号化された包含、単射の合成により、大域的なグラフを取り出さずにこれらの比較を組み合わせられます。
open import L.Ordinal.Linear {ℓ} lem using ( Tri; ord-tri ) open import L.Axioms.Full {ℓ} lem using ( hasSeparationL ) open import L.Cardinal {ℓ} lem using ( InjCode; InjL; SuccCardL ) open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate; inclusion-coded; injl-trans; module Relation ) open import L.Coding.Model {ℓ} using ( svAt-out; domAt-in )
先の二つの結果が最終的な比較を支えます。後続基数 δ より真に小さい順序数はすべて、その基数 κ へ単射します。また、符号化された整列順序は構成可能な順序数へ崩壊でき、崩壊像への符号化写像と、そこから戻る符号化写像が得られます。第三の材料 InjL (𝒫 κ) δ は、この章の条件付き定理の仮定であり、後続基数の記録だけからは従いません。
open import L.Coding.Injection {ℓ} lem using ( injAt-out ) open import L.GCH.BelowSuccessorCardinal {ℓ} lem using ( below-succ-injects ) open import L.GCH.Assembly {ℓ} lem using ( SuccIntoPower ) open import L.DefinableInjection {ℓ} lem using ( module Inj ) open import L.GCH.OrderType {ℓ} lem using ( Holds; module Code )
以下では、第二成分が証明である依存対をいくつか同一視します。その証明成分は命題なので、底の集合の等しさだけで十分です。得られた同一視に沿って、所属やグラフについての事実を輸送できます。
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop ) open import Cubical.Data.Sum using ( _⊎_; inl; inr ) open import Cubical.Foundations.Prelude using ( subst2 ) open import Cubical.Foundations.HLevels using ( isProp× ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
到達可能性の記録は、引き戻した順序に対する整礎再帰を表します。命題的切り詰めは、この章全体で単なる存在を表し、そこからの消去先は常に、空の型や別の InjL の主張のような命題です。
import Cubical.Induction.WellFounded as WF open WF using ( Acc; acc; WellFounded ) import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
正則性と推移性を適用するとき、底の集合の所属は周囲の階層で読みます。この周囲の関係は、構成可能性の証明と組にされた要素どうしの所属とは区別しなければなりません。
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
周囲の集合を SV.S と書きます。順序数の底の集合どうしの逐点包含のように、累積階層そのものの対象を動く主張で、この台を用います。
module SV = hPropStructure 𝒮ᵥ using ( S )
集合とその構成可能性の証明との組を SL.S と書きます。内部の冪集合、後続基数の述語、符号化された単射の関係は、いずれもこの台の要素を引数に取ります。
module SL = hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )
L 上の ZF 構造が、その内部の冪集合を定めます。その仕様は、𝒫 κ への所属を内部の部分集合関係と同一視し、そこでの量化は構成可能モデルの要素を動きます。
module ModelL = FOL.ZFModel 𝒮ʟ using ( isZFModel; module isZFModel; ℩-spec )
対象言語の論理式は、構成可能な集合からなる環境で評価されます。絶対性が、その充足の主張と証明で用いる台の水準の述語とを結ぶ意味論的な読みを与えます。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ ) open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
SL.S の要素は、底の集合と構成可能性の証明からなります。構成可能性は命題なので、底の集合の等しさを SL.S における等しさへ持ち上げられ、証明どうしの等しさを別に選ぶ必要はありません。
S≡ : {x y : SL.S} → fst x ≡ fst y → x ≡ y S≡ = Σ≡Prop (λ v → snd (isL v))
内部部分集合はモデルの冪集合に属する
最初の構成は、点ごとの内部包含をモデルの冪集合への所属へ変えます。これは任意の構成可能集合 κ と y に適用できます。y の構成可能な要素がすべて κ に属するなら、y は κ の内部部分集合であり、したがって 𝒫 κ に属します。
into-power : (zf : ModelL.isZFModel) (κ y : SL.S) → ((z : SL.S) → ⟨ fst z ∈ˢ fst y ⟩ → ⟨ fst z ∈ˢ fst κ ⟩) → ⟨ fst y ∈ˢ fst (ModelL.isZFModel.𝒫 zf κ) ⟩ into-power zf κ y sub =
冪集合の仕様は、y が 𝒫 κ に属することと、点ごとの内部部分集合条件とが同値であると述べます。この同値性に沿って書き換えると、目標はちょうど与えられた包含の証明になります。
subst ⟨_⟩ (sym (ModelL.℩-spec (hasPower κ) y)) sub where open ModelL.isZFModel zf using ( hasPower )
L の内部での Cantor の対角線論法
ここで任意の構成可能集合 κ を固定し、そのモデル内の冪集合について内部の Cantor の障害を証明します。この部分では、κ が基数であることも無限であることも仮定しません。
module Cantor (zf : ModelL.isZFModel) (κ : SL.S) where
対角線論法を通して、𝒫 κ は固定した L 上の ZF モデルが与える冪集合を意味します。したがって、その要素は、まさにこのモデルの内部で認識される部分集合です。
open ModelL.isZFModel zf using ( 𝒫 )
対角の議論は、明示的に与えられた一つのグラフ F とその符号について展開されます。後の主張はすべて、この固定されたグラフに関するものです。
module Diag (F : SL.S) (code : InjCode F (𝒫 κ) κ) where
グラフの環境は、グラフと、それが全域的である冪集合とを対にします。
γF : SL.S ^ 2 γF = F ∷ 𝒫 κ ∷ []
符号の値域の条項は、グラフに記録されたすべての値が κ に属することを言います。
ranF : (x y : SL.S) → Holds F x y → ⟨ fst y ∈ fst κ ⟩ ranF = code .snd .snd .snd
全域性の条項は、𝒫 κ の各要素が F による何らかの値をもつことを述べます。値の証人は命題的切り詰めの内側に留まるので、ここでは存在だけが得られ、大域的に値を選ぶことはありません。
valF : (x : SL.S) → ⟨ fst x ∈ fst (𝒫 κ) ⟩ → ∥ Σ[ y ∈ SL.S ] Holds F x y ∥₁ valF = domAt-in zero (suc zero) γF (code .snd .fst)
単射性の条項は、値から入力を復元します。同じ記録された値をもつ二つの要素は、底の集合が等しくなります。
injF : (y x x' : SL.S) → Holds F x y → Holds F x' y → fst x ≡ fst x' injF = injAt-out zero γF (code .snd .snd .fst)
対角の述語は、単に、冪集合のある要素 A で、記録された値が ξ に等しく、しかも ξ が A に属さないものが存在する、と言います。存在は切り詰められており、そのような集合は選ばれません。
Diagonal : SL.S → Type (ℓ-suc ℓ) Diagonal ξ = ∥ Σ[ A ∈ SL.S ] ( ⟨ fst A ∈ fst (𝒫 κ) ⟩ × Holds F A ξ × (⟨ fst ξ ∈ fst A ⟩ → Empty.⊥) ) ∥₁
適用のアトムの充足は、適用の符号化の妥当性により、文字どおり、台の水準でのグラフの成立です。
private a1 : (ξ A : SL.S) → ⟨ (A ∷ ξ ∷ []) ⊨ appC F zero (suc zero) ⟩ ≡ Holds F A ξ a1 ξ A = cong ⟨_⟩ (appC-adequate F zero (suc zero) (A ∷ ξ ∷ []))
対角条件を定める論理式は、𝒫 κ の中から、F が対 (A, ξ) を記録し、かつ ξ が A に属さないような集合 A を探します。有界量化は、その証人が κ の内部部分集合であることを正確に記録します。続いて κ 上で分出を適用し、この条件を満たす ξ∈κ 全体の集合を作ります。
opaque φD : Formula SL.S 1 φD = ∃̇∈ (con (𝒫 κ)) (appC F zero (suc zero) ∧̇ ¬̇ (var (suc zero) ∈̇ var zero))
適用の符号化の妥当性により、F を A に適用する論理式のアトムは、意味論的な主張 Holds F A ξ と同一視されます。この等式によって、以下の二方向で対角論理式と符号化されたグラフを相互に読み替えられます。
φD-out : (ξ : SL.S) → ⟨ (ξ ∷ []) ⊨ φD ⟩ → Diagonal ξ φD-out ξ = PT.map (λ { (A , (mA , (h , n))) → A , mA , transport (a1 ξ A) h , (λ k → lower (n k)) })
逆に、A ∈ 𝒫 κ、グラフについての事実 Holds F A ξ、および ξ ∉ A の証明が与えられれば、対角論理式を充足できます。これらのデータは、論理式の有界存在量化に伴う命題的切り詰めの中にまとめられます。
φD-in : (ξ A : SL.S) → ⟨ fst A ∈ fst (𝒫 κ) ⟩ → Holds F A ξ → (⟨ fst ξ ∈ fst A ⟩ → Empty.⊥) → ⟨ (ξ ∷ []) ⊨ φD ⟩ φD-in ξ A mA h n = ∣ A , (mA , (transport (sym (a1 ξ A)) h , (λ k → lift (n k)))) ∣₁
対角の集合は、この有界の論理式によって κ から分出されます。
D₀ : SL.S D₀ = fst (fst (hasSeparationL κ φD))
その所属の仕様は、分出自身の読みです。対角の集合に属するとは、κ に属し、かつ対角の論理式を充足することの連言です。
D₀-spec : (ξ : SL.S) → (ξ SL.∈ˢ D₀) ≡ ((ξ SL.∈ˢ κ) ⊓ ((ξ ∷ []) ⊨ φD)) D₀-spec = snd (fst (hasSeparationL κ φD))
対角の集合は内部の冪集合の要素です。逐点の読みが、そのすべてのモデルの要素が κ に属することを証明します。
D₀∈𝒫κ : ⟨ fst D₀ ∈ fst (𝒫 κ) ⟩ D₀∈𝒫κ = into-power zf κ D₀ (λ z h → fst (subst ⟨_⟩ (D₀-spec z) h))
矛盾を導くため、グラフが対角集合 D₀ にある値 ξ を割り当てると仮定します。値域の条項から ξ ∈ κ が得られ、D₀ の定義から ξ ∈ D₀ と ξ ∉ D₀ の両方が強制されます。
absurd : Σ[ ξ ∈ SL.S ] Holds F D₀ ξ → Empty.⊥ absurd (ξ , h₀) = out inside where
ξ ∈ D₀ と仮定します。対角論理式は、命題的切り詰めのもとで、F が A を ξ へ送り、かつ ξ ∉ A となる集合 A ∈ 𝒫 κ を与えます。F は D₀ も ξ へ送るので、単射性により A と D₀ の底の集合が同一視されます。仮定した所属を A へ輸送すると、ξ ∉ A と矛盾します。
out : ⟨ fst ξ ∈ fst D₀ ⟩ → Empty.⊥ out hm = PT.rec Empty.isProp⊥ (λ { (A , _ , hA , n) → n (subst (λ w → ⟨ fst ξ ∈ w ⟩) (injF ξ D₀ A h₀ hA) hm) }) (φD-out ξ (snd (subst ⟨_⟩ (D₀-spec ξ) hm)))
逆向きでは、先ほどの反証をデータとして用います。値域の条項から ξ ∈ κ が得られます。A = D₀ と取り、F が D₀ を ξ へ送ることと、前段で証明した ξ ∉ D₀ を使えば、対角論理式を証せます。したがって分出の仕様から ξ ∈ D₀ が得られ、これにその反証を適用して矛盾を得ます。
inside : ⟨ fst ξ ∈ fst D₀ ⟩ inside = subst ⟨_⟩ (sym (D₀-spec ξ)) (ranF D₀ ξ h₀ , φD-in ξ D₀ D₀∈𝒫κ h₀ out)
この二つの半分が、冪集合から κ への内部の符号化された単射をすべて反証します。単射はグラフへ消去され、グラフの対角の集合における値が矛盾へ消去されます。目標が空の型なので、どちらの消去も正当です。
no-inj : InjL (𝒫 κ) κ → Empty.⊥ no-inj = PT.rec Empty.isProp⊥ step where step : Σ[ F ∈ SL.S ] InjCode F (𝒫 κ) κ → Empty.⊥ step (F , code) = PT.rec Empty.isProp⊥ D.absurd (D.valF D.D₀ D.D₀∈𝒫κ)
選んだグラフ F に対して、対角構成は内部部分集合 D₀ と、そこに値を割り当てることが不可能であるという証明を与えます。それでも全域性は値を割り当てるので、このグラフについて矛盾が完成します。
where module D = Diag F code
冪集合を整列してその順序型を比較する
逆向きの比較を構成するため、κ の後続基数 δ と、仮定された単射 𝒫 κ ↪ δ を符号化する特定のグラフ G を固定します。このグラフは命題的切り詰めから得られる局所的な分岐の中でだけ利用でき、最終結果は再び InjL の主張になります。
module Build (zf : ModelL.isZFModel) (κ δ : SL.S) (sc : SuccCardL δ κ) (G : SL.S) (code : InjCode G (ModelL.isZFModel.𝒫 zf κ) δ) where
ここで始域となる 𝒫 κ も、固定した ZF モデルが定める内部の冪集合です。この構成で、それを底の集合の周囲の冪集合に置き換えることはありません。
open ModelL.isZFModel zf using ( 𝒫 )
後続の順序数性は、その記録の最初の成分です。
ordδ : IsOrd (fst δ) ordδ = sc .fst
冪集合が、比較の源として名付けられます。
P : SL.S P = 𝒫 κ
グラフの環境は、グラフと冪集合を対にします。
γG : SL.S ^ 2 γG = G ∷ P ∷ []
符号の値域の条項は、すべての値が後続の中に着地することを言います。
ranG : (x y : SL.S) → Holds G x y → ⟨ fst y ∈ fst δ ⟩ ranG = code .snd .snd .snd
一価性は一つの固定した入力についての性質です。G が G(x)=y と G(x)=y' の両方を記録するなら、y と y' の底の集合は等しくなります。この一意性により、x の可能な値からなる型が命題になります。
svG : (x y y' : SL.S) → Holds G x y → Holds G x y' → fst y ≡ fst y' svG = svAt-out zero γG (code .fst)
全域性は、各 x ∈ P に対して命題的に切り詰められた値の証人を与えます。この時点では、値はまだ選ばれていません。すぐ後で一価性から可能な値のファイバーが命題であることを示し、この切り詰めから消去して局所的に値を読み出します。
valG : (x : SL.S) → ⟨ fst x ∈ fst P ⟩ → ∥ Σ[ y ∈ SL.S ] Holds G x y ∥₁ valG = domAt-in zero (suc zero) γG (code .snd .fst)
符号化された単射 G の単射性の条項は、値から始域の要素を復元します。二つの始域の要素が同じ記録値をもつなら、それらの底の集合は等しくなります。
injG : (y x x' : SL.S) → Holds G x y → Holds G x' y → fst x ≡ fst x' injG = injAt-out zero γG (code .snd .snd .fst)
入力 x を固定すると、G のグラフが与える任意の二つの値は、一価性によって等しくなります。構成可能性の証明は命題なので、基礎にある値の等しさは証人全体の等しさへ持ち上がります。したがって、可能な値からなるファイバー自身が命題です。
isPropVal : (x : SL.S) → isProp (Σ[ y ∈ SL.S ] Holds G x y) isPropVal x (y , h) (y' , h') = Σ≡Prop (λ w → snd (pr (fst x) (fst w) ∈ fst G)) (S≡ (svG x y y' h h'))
定義域の条項が最初に与える G の値は、命題的切り詰めの内側にあります。直前に示した一意性によって行き先のファイバーは命題値になるので、切り詰めを除去し、その一意な値を以後の構成で使えます。この段階で用いるのは一意性であり、一般の選択原理ではありません。
val : (x : SL.S) → ⟨ fst x ∈ fst P ⟩ → Σ[ y ∈ SL.S ] Holds G x y val x m = PT.rec (isPropVal x) (λ z → z) (valG x m)
a が b に先行するとは、両者が P に属し、G(a)=x、G(b)=y、x∈y を満たすグラフの値 x と y が命題的切り詰めのもとで存在することだと定めます。命題的切り詰めは、適切な像が存在することだけを記録し、証人の選択は保持しません。
Read : SL.S → SL.S → Type (ℓ-suc ℓ) Read a b = ∥ Σ[ x ∈ SL.S ] Σ[ y ∈ SL.S ] ( ⟨ fst a ∈ fst P ⟩ × ⟨ fst b ∈ fst P ⟩ × Holds G a x × Holds G b y × ⟨ fst x ∈ fst y ⟩ ) ∥₁
この関係を対象言語で表すため、環境は A、B と、その像の候補 x、y を、G の二つの適用から読める位置に置きます。これにより、一つの論理式で G(A)=x、G(B)=y、x∈y を同時に述べられます。
private env5 : SL.S → SL.S → SL.S → SL.S → SL.S → SL.S ^ 5 env5 p A B x y = y ∷ x ∷ B ∷ A ∷ p ∷ []
最初の妥当性の等式は、符号化された適用をグラフの主張 Holds G A x と同一視します。これは、対象言語の論理式と、符号化されたグラフが A を x へ送るという主張を結ぶ橋です。
b1 : (p A B x y : SL.S) → ⟨ env5 p A B x y ⊨ appC G (suc (suc (suc zero))) (suc zero) ⟩ ≡ Holds G A x b1 p A B x y = cong ⟨_⟩ (appC-adequate G (suc (suc (suc zero))) (suc zero) (env5 p A B x y))
二つ目の妥当性の等式は、B と y について同じ変換を行います。二つの等式を合わせることで、引き戻した関係を、論理式の充足からも、G のグラフについての通常の主張からも証明できます。
b2 : (p A B x y : SL.S)
→ ⟨ env5 p A B x y ⊨ appC G (suc (suc zero)) zero ⟩ ≡ Holds G B y
b2 p A B x y = cong ⟨_⟩
(appC-adequate G (suc (suc zero)) zero (env5 p A B x y))
定義する論理式は、まず二つの端点を内部冪集合に制限し、続いてそれらの像となる二つのモデル要素を量化します。二つの適用のアトムと、像の間の所属比較を合わせることで、P 上の関係の一階的な記述が得られ、関係の構成はその記述を L の集合として表します。
private opaque φR : Formula SL.S 3 φR = (var (suc zero) ∈̇ con P) ∧̇ ((var zero ∈̇ con P) ∧̇ ∃̇ (∃̇ (appC G (suc (suc (suc zero))) (suc zero)
二つの存在束縛の内側で、残りの条項は、二つの証人がそれぞれ端点の G による像であり、最初の像が二つ目の像に属することを述べます。これはまさに、δ 上の所属順序を G に沿って引き戻したものです。
∧̇ (appC G (suc (suc zero)) zero ∧̇ (var (suc zero) ∈̇ var zero)))))
論理式を外向きに読むと、まず二つの像の証人が命題的切り詰めのもとに保たれます。次に、二つの妥当性の等式が符号化された適用をグラフの事実へ変え、Read の意味論的データ、すなわち端点の所属、二つの値、その間の所属比較をちょうど与えます。
read : (a b p : SL.S) → ⟨ (b ∷ a ∷ p ∷ []) ⊨ φR ⟩ → Read a b read a b p (ma , mb , h) = PT.rec squash₁ (λ { (x , hx) → PT.map (λ { (y , ha , hb , hxy) → x , y , ma , mb , transport (b1 p a b x y) ha , transport (b2 p a b x y) hb , hxy }) hx }) h
内向きの読み出しは、逆向きの妥当性の等式に沿って、それぞれのホスト側の事実を運び戻し、存在量化子と適用の枠を満たして、論理式の充足を再構築します。
fill : (a b p : SL.S) → Read a b → ⟨ (b ∷ a ∷ p ∷ []) ⊨ φR ⟩ fill a b p = PT.rec (snd ((b ∷ a ∷ p ∷ []) ⊨ φR)) (λ { (x , y , ma , mb , ha , hb , hxy) → ma , mb , ∣ x , ∣ y , transport (sym (b1 p a b x y)) ha , transport (sym (b2 p a b x y)) hb , hxy ∣₁ ∣₁ })
有界関係の構成は、この定義可能な述語を L にある実際の関係集合へ変えます。上で示した二方向の読み替えにより、符号化された関係への所属は、Read が表す命題的に切り詰められた内容とちょうど一致します。
module Pullback = Relation P P φR (λ a b → Read a b , squash₁) read fill
逆向きに読むときは、二つの妥当性の等式によって、グラフの事実 Holds G A x と Holds G B y を適用のアトムへ戻します。続いて x と y を二つの存在量化の証人としてまとめると、定義論理式の充足が再構成されます。
R : SL.S R = Pullback.rel
R の一つの関係項から、引き戻しを定義する命題的に切り詰められたデータを読み戻せます。すなわち、二つの端点は冪集合に属し、それぞれ G による像をもち、最初の像は二つ目の像に属します。
R-out : (a b : SL.S) → Holds R a b → Read a b R-out = Pullback.pair-out
内向きの読み出しは、二つの端点の所属、G の像の二つの事実、そして像の間の所属から、関係の項目を作ります。
R-in : (a b x y : SL.S) → ⟨ fst a ∈ fst P ⟩ → ⟨ fst b ∈ fst P ⟩ → Holds G a x → Holds G b y → ⟨ fst x ∈ fst y ⟩ → Holds R a b R-in a b x y ma mb ha hb hxy = Pullback.into a b ma mb ∣ x , y , ma , mb , ha , hb , hxy ∣₁
符号化された関係の各項目では、二つの端点がとも P に属します。証明は命題的切り詰めのもとにある証人を読み、像のデータを捨てて、二つの端点の所属だけを残します。その積は命題なので、この切り詰めの除去が許されます。
Rsub : (a b : SL.S) → Holds R a b → ⟨ fst a ∈ fst P ⟩ × ⟨ fst b ∈ fst P ⟩ Rsub a b h = PT.rec (isProp× (snd (fst a ∈ fst P)) (snd (fst b ∈ fst P))) (λ { (_ , _ , ma , mb , _) → ma , mb })
外向きの読み出しを適用すると、抽出に必要な証人が得られます。その切り詰めを除去できるのは、結論である二つの端点の所属命題の組もまた命題だからです。
(R-out a b h)
順序型の構成は、P の要素を小さい提示領域 Dom で表します。関係 a ≺ b は、表された要素どうしが R で関係づけられるという符号化された事実をちょうど記録します。そこで以下では、添字上の引き戻し順序を調べ、のちにそれを崩壊できます。
module OT = Code P R Rsub using ( Dom; Dom≡; toDom; up; up-mem; up-toDom; ↪; _≺_; ≺-in; ≺-out ; module Conjuncts )
この領域の添字 b に対し、v b を、b が表す P の要素へ G が割り当てる一意な値とします。次に、これらの代表が δ より下の順序数であることを示します。
v : OT.Dom → SL.S v b = fst (val (OT.up b) (OT.up-mem b))
選んだ値の第二成分は、対応するグラフの事実 Holds G (up b) (v b) を記録します。これは、代表どうしの比較を引き戻した関係の項目へ結びつけます。
v-holds : (b : OT.Dom) → Holds G (OT.up b) (v b) v-holds b = snd (val (OT.up b) (OT.up-mem b))
単射の符号の値域の条項により、G の各値は後続基数 δ に属します。したがって、すべての代表が一つの順序数の中にあり、そこで所属による比較と順序数の三分法を用いられます。
v∈δ : (b : OT.Dom) → ⟨ fst (v b) ∈ fst δ ⟩ v∈δ b = ranG (OT.up b) (v b) (v-holds b)
それぞれの G の値は順序数です。δ の順序数性から受け継がれます。
ord-v : (b : OT.Dom) → IsOrd (fst (v b)) ord-v b = mem-ord {A = fst δ} ordδ (fst (v b)) (v∈δ b)
前向きの比較は、引き戻された関係の一つの先行段階を、二つの代表順序数の間の所属へ移します。関係の項目を読むと二つの像の証人が得られ、G の一価性によって、それぞれが固定した値 v a と v b に同一視されます。
≺-fwd : (a b : OT.Dom) → a OT.≺ b → ⟨ fst (v a) ∈ fst (v b) ⟩ ≺-fwd a b k = PT.rec (snd (fst (v a) ∈ fst (v b))) (λ { (x , y , _ , _ , ha , hb , hxy) → subst2 (λ s t → ⟨ s ∈ t ⟩) (svG (OT.up a) x (v a) ha (v-holds a))
二つの一価性の等式により、R から読み出した像の証人を、固定した代表 v a と v b にそれぞれ置き換えます。x∈y を両方の等式に沿って輸送すると、必要な比較 v a ∈ v b が得られます。
(svG (OT.up b) y (v b) hb (v-holds b)) hxy }) (R-out (OT.up a) (OT.up b) (OT.≺-out a b k))
後ろ向きの比較は、二つの代表の順序数の所属から、引き戻された関係を構成します。二つのグラフの事実と、像の間の所属を、改めて導入することによるものです。
≺-bwd : (a b : OT.Dom) → ⟨ fst (v a) ∈ fst (v b) ⟩ → a OT.≺ b ≺-bwd a b h = OT.≺-in a b (R-in (OT.up a) (OT.up b) (v a) (v b) (OT.up-mem a) (OT.up-mem b) (v-holds a) (v-holds b) h)
整礎性を示すため、階層の要素 u を固定し、代表の値が u であるすべての領域の添字を考えます。述語 Pacc u は、その各添字が引き戻し順序でアクセス可能であることを要求し、周囲の所属関係に関する帰納を準備します。
private Pacc : V ℓ → Type (ℓ-suc ℓ) Pacc u = (b : OT.Dom) → fst (v b) ≡ u → Acc OT._≺_ b
帰納のステップは、代表の順序数が u より厳密に下にある先行者のアクセス可能性を構成します。前向きの比較が所属を代表へ運び、帰納の仮定がそこでアクセス可能性を供給します。
accStep : (u : V ℓ) → (∀ u' → ⟨ u' ∈ˢ u ⟩ → Pacc u') → Pacc u accStep u IH b e = acc (λ a k → IH (fst (v a)) (subst (λ w → ⟨ fst (v a) ∈ˢ w ⟩) e (≺-fwd a b k)) a refl)
すべての階層の要素でのアクセス可能性は、周囲の階層の正則性の帰納で証明されます。それは、所属の整礎性です。
accAt : (u : V ℓ) → Pacc u accAt = WF.WFI.induction regularityV {P = Pacc} accStep
引き戻された順序の整礎性は、代表の順序数ごとのアクセス可能性から組み立てられます。
wf : WellFounded OT._≺_ wf b = accAt (fst (v b)) b refl
引き戻された順序の推移性は、二つの前向きの比較を、順序数 δ の推移性を二つの代表の所属に適用して合成します。
≺-trans : {a b c : OT.Dom} → a OT.≺ b → b OT.≺ c → a OT.≺ c ≺-trans {a} {b} {c} k k' = ≺-bwd a c (ordδ .snd (fst (v c)) (v∈δ c) (≺-fwd a b k) (≺-fwd b c k'))
引き戻された順序の三分法は、δ にある代表値についての順序数の三分法から移されます。任意の a と b に対して、v a ∈ v b、二つの値が等しい、v b ∈ v a のいずれかが成り立ちます。
tri : (a b : OT.Dom) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a)) tri a b = go (ord-tri (fst (v a)) (ord-v a) (fst (v b)) (ord-v b)) where go : Tri (fst (v a)) (fst (v b)) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
厳密に下の場合は、引き戻された比較を直接作ります。等しい場合は、等しい代表の値に G の単射性を適用して、二つの定義域の要素を同一視します。厳密に上の場合は比較を逆向きにします。
go (inl h) = inl (≺-bwd a b h) go (inr (inl e)) = inr (inl (OT.Dom≡ (injG (v a) (OT.up a) (OT.up b) (v-holds a) (subst (λ w → ⟨ pr (OT.↪ b) w ∈ fst G ⟩) (sym e) (v-holds b))))) go (inr (inr h)) = inr (inr (≺-bwd b a h))
整礎性と推移性から、崩壊写像 col とその像 otL が得られます。三分法を加えると崩壊の単射性も従い、異なる領域の添字が同じ崩壊値をもつことはありません。これらの事実は、崩壊の表と、あとでそれを逆向きに読むためのデータの両方を与えます。
module C = OT.Conjuncts wf ≺-trans using ( module Inj; col; col-ord; col-out; colTable; colTable-in ; colTable-pair; otL; otL-in; otL-out ) module I = C.Inj tri using ( code; col-inj; module Inverse )
崩壊の表は、内部の冪集合 P からその崩壊像 otL への符号化された単射です。その特定の表と単射性の証明を命題的に切り詰めることで、内部の主張 InjL P otL が得られます。
power-into-ot : InjL P C.otL power-into-ot = ∣ C.colTable , I.code ∣₁
崩壊像が順序数であることを示すには、像自身の推移性と、その各要素が推移的集合であることの両方が必要です。後者について、otL への所属から、命題的切り詰めのもとで、与えられた要素を崩壊値として提示する添字 b が得られます。
ot-ord : IsOrd (fst C.otL) ot-ord = tr , mem where mem : (x : V ℓ) → ⟨ x ∈ˢ fst C.otL ⟩ → isTransV x mem x h = PT.rec (isPropIsTransV x)
各崩壊値 col b はすでに順序数だと分かっているので、推移的です。この推移性を等式 col b = x に沿って輸送すれば、像の任意の要素 x が推移的であることが従います。
(λ { (b , e) → subst isTransV e (C.col-ord b .fst) }) (C.otL-out x h)
残るのは、像自身が推移的であることです。y∈x と x∈otL が与えられると、otL の外向きの記述は、命題的切り詰めのもとで x をある崩壊値 col b として提示します。目標の所属 y∈otL は命題なので、この証人を局所的に使えます。
tr : isTransV (fst C.otL) tr {x} {y} y∈x x∈ot = PT.rec (snd (y ∈ˢ fst C.otL)) outer (C.otL-out x x∈ot) where outer : Σ[ b ∈ OT.Dom ] (C.col b ≡ x) → ⟨ y ∈ˢ fst C.otL ⟩
x を col b に置き換えると、col b への所属を述べる崩壊の等式から、再び命題的切り詰めのもとで、崩壊値が y である先行者 r≺b が得られます。この小さい崩壊値が、y を像へ戻すために必要な証人です。
outer (b , e) = PT.rec (snd (y ∈ˢ fst C.otL)) inner (C.col-out b y (subst (λ w → ⟨ y ∈ˢ w ⟩) (sym e) y∈x)) where inner : Σ[ r ∈ OT.Dom ] ((r OT.≺ b) × (C.col r ≡ y)) → ⟨ y ∈ˢ fst C.otL ⟩
先行者の崩壊がその等式に沿って y へ運ばれ、y を像の中に置くことで、推移性の証明が完成します。
inner (r , _ , e2) = subst (λ w → ⟨ w ∈ˢ fst C.otL ⟩) e2 (C.otL-in r)
階層の要素 w に対し、ファイバー Fib w は添字 b と等式 col b = w からなります。したがって、このファイバーの要素は、崩壊写像による w の原像そのものです。
Fib : V ℓ → Type (ℓ-suc ℓ) Fib w = Σ[ b ∈ OT.Dom ] (C.col b ≡ w)
col の単射性により、各ファイバーは命題になります。b と b' がともに w へ崩壊するなら、それらの等式から col b と col b' が等しくなり、単射性によって添字も等しくなります。周囲の階層 V ℓ は集合なので、各等式型 col b = w は命題であり、その証明が新たな違いを生むこともありません。
isPropFib : (w : V ℓ) → isProp (Fib w) isPropFib w (b , e) (b' , e') = Σ≡Prop (λ _ → setIsSet _ _) (I.col-inj b b' (e ∙ sym e'))
所属 w∈otL が最初に与える原像の添字は、命題的切り詰めの内側にあります。Fib w が命題であることを直前に示したので、この切り詰めを除去し、崩壊値が w である一意な添字を取り出せます。
fib : (w : V ℓ) → ⟨ w ∈ˢ fst C.otL ⟩ → Fib w fib w h = PT.rec (isPropFib w) (λ z → z) (C.otL-out w h)
いま得た一意な原像により、崩壊の表を otL 全体で逆向きに読めます。その添字が表すもとの要素は P に属するので、逆向きの構成は L にあるグラフを作り、とくに以下で用いる内部の符号化された単射 Back.injL : InjL otL P を与えます。
module Back where open I.Inverse C.otL P (λ w mw → fib (fst w) mw) (λ w mw → OT.up-mem (fib (fst w) mw .fst)) public using ( fn; graph; at; only; M; inj; injL ) renaming ( SourceMem to Mem )
崩壊順序数 otL を μ と書きます。順序数の三分法によって μ と後続基数 δ を比較します。補助関数 from-sub は、等しい場合と δ∈μ の場合に共通する構成を取り出します。δ のすべての要素が μ にも属するなら、必要な InjL δ P を作ります。
result : InjL δ P result = go (ord-tri (fst C.otL) ot-ord (fst δ) ordδ) where from-sub : ((z : SV.S) → ⟨ z ∈ˢ fst δ ⟩ → ⟨ z ∈ˢ fst C.otL ⟩) → InjL δ P
包含の符号が、部分集合の事実を、δ から崩壊の像への符号化された単射としてまとめ、逆崩壊の単射がそれを冪集合の中へ合成します。
from-sub sub = injl-trans δ C.otL P (inclusion-coded δ C.otL sub) Back.injL
三分法では、まず μ∈δ の場合を考えます。この場合、below-succ-injects は後続基数の事実を用いて InjL μ κ を与えます。これを InjL P μ と合成すると InjL P κ が得られ、内部の Cantor の定理に反します。したがって排除されるのは、崩壊順序数が δ より真に小さい場合だけです。
go : Tri (fst C.otL) (fst δ) → InjL δ P go (inl ot∈δ) = Empty.rec (Cantor.no-inj zf κ (injl-trans P C.otL κ power-into-ot (below-succ-injects κ δ sc C.otL ot-ord ot∈δ))) go (inr (inl e)) =
残る二つの場合は、どちらも from-sub に必要な包含を与えます。μ=δ なら、等式に沿う輸送によって、δ への各所属が μ への所属になります。δ∈μ なら、順序数 μ の推移性から同じ包含 δ⊆μ が得られます。いずれの場合も、この包含を単射として符号化し、逆崩壊の単射と合成することで InjL δ P を得ます。
from-sub (λ z h → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) h) go (inr (inr δ∈ot)) = from-sub (λ z h → ot-ord .fst h δ∈ot)
後続基数から冪集合へ到達する
この定理は、後続基数の証人 sc と、命題的に切り詰められた単射 InjL (𝒫 κ) δ を受け取ります。目標 InjL δ (𝒫 κ) 自身が命題なので、特定のグラフ G を調べられるのは局所的な分岐の中だけです。追加の仮定 κ∉ω は SuccIntoPower の主張に現れますが、この証明では使われません。GCH の組み立てでは、succCardExists は命題的切り詰めのもとで δ とその証人 sc だけを与えます。power-into-succ が別に pis : InjL (𝒫 κ) δ を構成し、それを succ-into-power に渡します。得られる結論が記録するのは、二方向の符号化された単射が命題的切り詰めのもとで存在することだけです。どちらのグラフも選ばず、全単射、集合の等しさ、基数の等式も与えません。
succ-into-power : (zf : ModelL.isZFModel) → SuccIntoPower zf succ-into-power zf κ δ κ∉ω sc = PT.rec squash₁ (λ { (G , code) → Build.result zf κ δ sc G code })