この章を読むか、対話型目次と依存グラフで別のルートを選べます。

対話型目次 · 依存グラフ

そこで、宇宙レベルとこの排中律の実例を章全体のパラメータとして明示する。以下の構成はすべて同じ lem に相対しており、途中で別の公理を加えることはない。ここでの目的は、後の基数論に必要な正確な概念と有界な順序を準備することである。基数代表や後続基数の存在を、この時点で主張するわけではない。

module L.Cardinal {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

L の内部で基数を論じるには、互いに関係する二種類の比較を区別する必要がある。ホストでは集合を提示する小さな型を実際の関数で比較できるが、L の内部で述べる主張は、それ自身が構成可能なグラフによって証されなければならない。本章では両方の概念を展開し、それぞれの論理的な強さを明確に保つ。具体的な関数とグラフの符号はデータを持ち、後で使う基数の比較は存在だけを保持する。

議論は基礎語彙の章で説明したホスト言語の中で行う。用いる古典的な原理は、Type (ℓ-suc ℓ) にある命題に対する排中律だけである。これは宇宙レベルで制限された仮定であり、無制限の排中律や選択原理ではない。単射やグラフの符号の定義自体は証人を選ばない。古典的な推論が働くのは、順序数の整列順序を構成するときと、後でその順序から最小元を得るときである。

以下では二つの数学的な場を同時に扱う。累積階層は周囲の集合と命題値の所属を与え、構成可能モデルは L に属する集合と、その上で解釈される関係を与える。基本的な事実 a ∈ sucV a は、すべての集合が集合論的後続 a ∪ {a} に属すことを表し、後で有界な探索のための特定の点を与える。

周囲の各集合には標準的な小さな提示もある。そのインデックスは集合のすべての要素を名指し、member はインデックスを所属証明へ変え、fiber は所属からインデックスを復元する。順序対を使えば、集合で関係を表せる。構成可能な側では、モデルの要素は周囲の集合と、それが L に属すことの証明を組にしたものである。さらに L の推移性により、集合の構成可能性はその各要素へ受け継がれる。これらの事実が、小さな提示と構成可能なグラフの符号を結び付ける。

有界な探索には、順序数の所属が提示上に誘導する狭義の整列順序を使う。その三分性は最終的に lem を用い、整礎性は周囲の所属の正則性から得られる。ほかの材料は、一価性、正確な定義域、単射性というグラフの性質を対象言語で記述する。後で具体的なグラフの符号を命題的切り詰めによって隠すとき、順序に関する材料と論理式に関する材料を区別することが重要になる。

集合 a に対し、その要素を添字付ける小さな型を ⟪ a ⟫、インデックスをそれが名指す要素へ送る写像を ⟪ a ⟫↪ と書く。集合論的後続 sucV a は a のすべての要素と a 自身を含む。したがって a が順序数なら、⟪ sucV a ⟫ は、すべてのより小さい順序数を名指すインデックスと a を名指すインデックスを含む、小さな探索空間である。

open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( sucV )

本書では、存在を命題的切り詰めによって意図的に弱めることがよくある。∥ X ∥₁ の要素は X に要素があることを主張するが、具体的な要素は明らかにしない。反証を表す空型のような命題へは消去できるが、任意のデータへは消去できない。この規則により、後で InjCode に含まれる具体的なグラフの情報と、InjL が述べる単なる存在が厳密に区別される。

以下の記法は、主張がどちらの場に属すかを示す。周囲の構造では、_∈ˢ_ は階層の生の集合どうしの命題値をもつ所属関係である。これに対して S は構成可能な構造の台であり、要素 a : S は、底にある周囲の集合 a .fst と、その構成可能性を示す命題値の証明からなる。したがって ⟨ x .fst ∈ˢ a .fst ⟩ は底の周囲の集合に関するホスト側の命題であり、x : S 上の量化は構成可能集合だけにわたる。対象言語の構文は、以下で導入する充足関係を通して別に現れる。

open hPropView 𝒮ᵥ using ( _∈ˢ_ )
open hPropView 𝒮ʟ using ( S )

構成可能な構造には、命題値をもつ点ごとの部分集合関係もある。⟨ a ⊆ˢ b ⟩ の証明は、各 x : S について、x が a に属するという証明を x が b に属するという証明へ送る。したがって、その量化は構成可能な台にわたる。L の推移性により、これは底にある集合について通常の部分集合関係として読める。a と b が順序数なら、これは両者の非狭義の順序である。そのため、後続基数の最小性は包含を結論とし、狭義の比較は所属で表す。

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( _⊆ˢ_ )

充足の記号 _⊨_ は、構成可能な構造における解釈を表すものとして固定する。判断 γ ⊨ φ では、環境 γ は S の要素を並べるため、φ の非有界量化子は構成可能集合にわたる。これが InjCode の最初の三条件の意味である。それらは L の内部で成り立つ対象言語の主張であり、その証明自体はホストで扱われる。

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )

まず、ホストレベルだけで単射を定義する。X ↪ Y の要素は関数 f : X → Y とその単射性の証明からなり、その証明は f x と f y の等しさから x と y の等しさが従うことを述べる。関数は具体的なデータなので、この対から射影できる。全射性や逆関数は含まれず、集合、構成可能性の証明、充足の判断、切り詰めもこの定義には現れない。後では、二つの周囲の集合を表す小さな提示型が典型的な始域と終域になる。

_↪_ : Type ℓ → Type ℓ → Type ℓ
X ↪ Y = Σ[ f ∶ (X → Y) ] ((x y : X) → f x ≡ f y → x ≡ y)

ここで、底にある集合が順序数である構成可能集合 α を固定する。後で必要な大きさの順序数を探すには、sucV (α .fst) の標準的な提示の中で探索すれば十分である。この集合は α のすべての要素と α 自身を含むので、探索空間は小さな型であると同時に自然な始点を持つ。ここでの定義が作るのは、この順序付けられた探索空間である。候補の述語を与えて最小元を選ぶのは後の議論である。

module LeastCardInjL (α : S) (oα : IsOrd (α .fst)) where

最初に、この集合論的後続自身が L に属すことを示す。oα に順序数の後続を二度適用すると、sucV (sucV (α .fst)) が順序数だと分かる。順序数が次の構成可能な段階に属すという定理により、sucV (α .fst) はこの明示された段階に入り、ある段階への所属からその構成可能性が得られる。したがって、この証明は後続を含む具体的な段階を示しており、構成可能性が一般に sucV について閉じているという性質を仮定してはいない。

hSucα : ⟨ isL (sucV (α .fst)) ⟩
hSucα = Lset→isL (sucV (sucV (α .fst))) (suc-ord (suc-ord oα)) (sucV (α .fst))
          (ord∈Lset-suc (sucV (α .fst)) (suc-ord oα))

提示の各インデックス m は sucV (α .fst) の要素を名指す。この後続は構成可能であり、L は推移的なので、名指された要素も構成可能である。そこで up は、m が名指す底の集合を保ち、この事実から得た証明を添えて S の要素を作る。この写像はこの有界な提示上だけで定義され、任意の周囲の集合を構成可能集合へ変えるものではない。

up : ⟪ sucV (α .fst) ⟫ → S
up m = ⟪ sucV (α .fst) ⟫↪ m
     , isL-trans (member (sucV (α .fst)) m) hSucα

順序数の所属によって、これらのインデックスを順序付ける。順序数 sucV (α .fst) に ordSWO を適用すると、⟪ sucV (α .fst) ⟫ 上の狭義の整列順序 w が得られる。この比較は名指された集合どうしの所属に従い、三分性は lem に依存し、整礎性は正則性から従う。この値を不透明にする指定は、後の証明での展開を制御するだけであり、関係、その法則、あるいは法則が依存する仮定を変えない。

opaque
  w : SWO (⟪ sucV (α .fst) ⟫)
  w = ordSWO (sucV (α .fst)) (suc-ord oα)

パス w-lt が、この順序の利用可能な記述を与える。インデックス m と n に対し、w のもとで m が n に先行するという命題は、m が名指す集合が n の名指す集合に属すという命題と同一視される。これは命題型どうしの等しさであり、集合どうしの等しさではない。後の証明はこのパスに沿って、インデックスの比較と順序数の所属の間で証拠を両方向に移せる。その際、整列順序を展開する必要はない。

opaque
  unfolding w
  w-lt : (m n : ⟪ sucV (α .fst) ⟫)
       → let module W = SWO w in (m W.<∙ n) ≡ ⟨ ⟪ sucV (α .fst) ⟫↪ m ∈ˢ ⟪ sucV (α .fst) ⟫↪ n ⟩
  w-lt m n = refl

この探索空間には、α .fst を名指す特定のインデックスがある。証明 self∈sucV (α .fst) は順序数がその集合論的後続に属すことを与え、fiber はその所属を、インデックスとその像を記述する等式の組へ変える。階層の所属は命題値であるが、提示写像は埋め込みなので、そのファイバー自体が命題である。したがって選択原理を用いずに、切り詰めをこの一意なファイバーへ消去できる。self はこうして復元されたインデックスであり、順序数そのものではない。

self : ⟪ sucV (α .fst) ⟫
self = fiber (sucV (α .fst)) (self∈sucV (α .fst)) .fst

付随する等式は、self が何を名指すかを正確に述べる。提示写像によるその像は α .fst に等しくなる。この等式は底にある周囲の集合どうしのものであり、対応する S の要素どうしの等しさまでは主張しない。後者には構成可能性の証明も同一視する必要があるからである。self と self-eq を合わせると、後の探索で α の性質を調べるための具体的なインデックスが得られる。

self-eq : ⟪ sucV (α .fst) ⟫↪ self ≡ α .fst
self-eq = fiber (sucV (α .fst)) (self∈sucV (α .fst)) .snd

内部の単射と後続基数

具体的な構成可能集合 F は、まず L の内部での三つの充足条件によって、a から b への単射を符号化する。第一の条件は、対の形をした項目が一価であること、つまり同じ入力が異なる二つの出力を持たないことを述べる。第二の条件は、定義域が正確に a であることを両方向に述べる。対の形をした各項目の第一成分は a に属し、a の各要素には出力が単に存在する。第三の条件はグラフの単射性、つまり出力が同じ二つの項目の入力が等しいことを述べる。三つの判断では、環境の第一項が F、第二項が a であり、すべての非有界量化子は S にわたる。

InjCode : S → S → S → Type (ℓ-suc ℓ)
InjCode F a b =
    ⟨ (F ∷ a ∷ []) ⊨ svAt zero ⟩
  × ⟨ (F ∷ a ∷ []) ⊨ domAt zero (suc zero) ⟩
  × ⟨ (F ∷ a ∷ []) ⊨ injAt zero ⟩

第四の条件はホストで直接述べられる。任意の x,y : S に対し、底にある集合の順序対が底のグラフに属すなら、底にある出力は b に属する。したがって b は値の終域となる上界であり、b のすべての要素が値として取られるとは述べない。また InjCode は、F のすべての要素が順序対であるとも主張しない。その条件が調べるのは対の形をした要素だけなので、別の形をした余分な要素は符号から読み出される関数に影響しない。このホストレベルの値域条件は、先の三つの対象言語における充足の判断と区別する必要がある。

  × ((x y : S) → ⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩ → ⟨ y .fst ∈ b .fst ⟩)

InjL a b は、四つの条件をどの具体的なグラフが満たすかを忘れる。これは F と InjCode F a b からなる依存対の命題的切り詰めなので、L の内部に a から b への符号化された単射が単に存在することだけを述べる。特定のグラフやホストレベルの関数を射影することはできない。これを局所的に開けるのは目標が命題である場合だけである。後で単射を合成したり変換したりする構成は、そのような枝の中でグラフを使い、得られたグラフを再び命題的切り詰めに入れる。向きも主張の一部であり、InjL a b だけから InjL b a は何も分からない。

InjL : S → S → Type (ℓ-suc ℓ)
InjL a b = ∥ Σ[ F ∶ S ] InjCode F a b ∥₁

κ が順序数であるとき、基数性は始順序数であることによって表される。von Neumann 順序数の各要素 δ はより小さい順序数であり、IsCardinalL κ は、InjCode F κ δ を満たす構成可能なグラフが存在するという命題的切り詰めを反証する。直前の記法で言えば、排除されるのは InjL κ δ であり、InjL δ κ ではない。これらは内部の符号化された単射を表す命題であって、ホストレベルの型 _↪_ の実例ではなく、その切り詰めから後者のホストレベルの単射を一般に取り出すこともできない。この定義は一般の構成可能集合についても形成でき、κ が順序数であるという証明を含まない。後の使用箇所では IsOrd (κ .fst) を別に与えてから、始順序数として解釈する。反証の行き先は空型なので、必要となる命題的切り詰めの消去は正当である。

IsCardinalL : S → Type (ℓ-suc ℓ)
IsCardinalL κ =
  (δ : S) → ⟨ δ .fst ∈ κ .fst ⟩
          → (∥ Σ[ F ∶ S ] InjCode F κ δ ∥₁ → ⊥₀)

SuccCardL δ κ の引数の順序では、δ が候補となる後続基数であり、κ がそれより下にある対象である。最初の三条件は、δ の底にある集合が順序数であること、δ が始順序数を表す述語を満たすこと、そして κ ∈ δ、すなわち順序数の文脈で δ が κ より真に大きいことを述べる。これらは与えられた対の性質を記述するだけで、そのような δ を作るものではなく、κ 自身が順序数や基数であることも要求しない。定義の最後の条件が、さらに大域的な最小性を加える。ここに sucV は現れない。後続基数は集合論的後続 κ ∪ {κ} ではない。

SuccCardL : S → S → Type (ℓ-suc ℓ)
SuccCardL δ κ =
    IsOrd (δ .fst)
  × IsCardinalL δ
  × ⟨ κ .fst ∈ δ .fst ⟩

最後のフィールドは、κ より大きい内部順序数基数全体の中での最小性を表す。基礎集合が順序数で、IsCardinalL c を満たし、κ を含む任意の c : S を与えると、このフィールドは内部の包含 δ ⊆ˢ c を返す。第一のフィールドによって δ も順序数であることが分かっているので、ここで包含は順序数の非狭義の比較である。すなわち、δ はそのようなすべての c 以下である。結論が所属ではなく包含になっているのは、c が δ 自身である場合も扱う必要があるからである。S 上の量化と _⊆ˢ_ はどちらも構成可能な台に対するものなので、これは L に見える候補の中での最小性である。このフィールドが κ について仮定するのは κ ∈ c だけである。κ 自身の順序数性と内部基数性は、この述語を用いる各定理で仮定される。

このフィールドは単射のグラフを構成しない。InjCode F a b は特定の構成可能な符号 F と単射の四条件を保持するが、InjL a b は ∥ Σ[ F ∶ S ] InjCode F a b ∥₁ という命題的切り詰めである。したがって、IsCardinalL c と c の順序数性を合わせた仮定は、c からその要素であるより小さな順序数への InjL 単射が存在しないことを述べる。SuccCardL δ κ 自体は、固定された対 δ, κ に関する切り詰められていない性質である。適切な δ の存在を証明せず、特定の δ も選ばない。後の succCardExists は、κ が順序数である内部基数であり、有限順序数ではないとき、そのような δ の存在を命題的切り詰めの下で証明する。そこで用いる古典的仮定は、このモジュールのパラメータ LEM (ℓ-suc ℓ) だけである。集合論的後続 sucV はこの定義に現れない。

  × ((c : S) → IsOrd (c .fst) → IsCardinalL c → ⟨ κ .fst ∈ c .fst ⟩
             → ⟨ δ ⊆ˢ c ⟩)