BedrockBedrock
𝑉 の形而上学のために基礎を築く
Cubical Agda で集合論を形式化する三言語の対話型教科書。排中律の仮定のもとで、構成可能宇宙 L が ZFC と GCH を満たすことを証明する。
まず本書の主要定理を見てから、学習ルートやその前提関係を確かめます。
原点は本書の始まりと終わりをつなぐ。まず探究の動機を述べ、続いて各証明の道筋が到達する成果をまとめる。
前書き
Bedrock は Cubical Agda で機械検証された集合論を展開し、集合宇宙についての問いに土台を与える。最初に達成した目標は、構成可能宇宙が ZFC と GCH を満たすことである。本書はそのための言語、モデル、証明を順に構築する。以下のマイルストーンは、出発前に到達点を見渡すためのものである。
基本方針は、できる限りホスト言語で数学を表現し、式自体が研究対象となる場合に深く埋め込まれた一階言語を使うことである。また、立方型理論では累積階層を高階帰納型として構成できる。これは数学的基礎の選択であり、メタ理論が研究対象の理論より弱いという主張ではない。
最初の目標の先には、強制、内部モデル、𝑉 の構造についての問いがある。それらはプロジェクトの動機であって、本書ですでに得られた成果ではない。目指すのは、これらの問いに検証された土台を与えることである。
マイルストーン
定理0 SetChoice は LEM を含意し、LEM はさらに ΩResizing を含意する。
open import Base.Choice public using ( SetChoice→LEM )
open import Base.Classical public using ( LEM→ΩResizing )
定理1 ΩResizing を仮定すると、HIT による累積階層 V は ZF のモデルである。
open import V.Model public using ( V⊨ZF )
定理2 SetChoice を仮定すると、HIT による累積階層 V は ZFC のモデルである。
open import V.Model public using ( V⊨ZFC )
定理3 LEM を仮定すると、構成可能宇宙 L は ZFC のモデルである。
open import L.Model public using ( L⊨ZFC )
定理4 LEM を仮定すると、構成可能宇宙 L は内部的に一般連続体仮説を満たす。
open import L.GCH.Theorem public using ( L⊨GCH )
{-# OPTIONS --cubical --safe --guardedness #-}
module Origin whereopen import Base.Choice public using ( SetChoice→LEM )open import Base.Classical public using ( LEM→ΩResizing )open import V.Model public using ( V⊨ZF )
open import V.Model public using ( V⊨ZFC )open import L.Model public using ( L⊨ZFC )open import L.GCH.Theorem public using ( L⊨GCH )主題を選び、ルートを比較し、修了した前提から進めます。
対話型目次 · 依存グラフ用語集
用語は本書で最初に現れる順に並んでいます。用語を選ぶと、最初の導入箇所を振り返れます。
- 対象理論
- メタ理論の中で表現され研究される理論。本書では集合論を指す。
- メタ理論
- 対象理論を表現し研究するための理論。本書では立方型理論を指す。
- ホスト
- 対象理論の形式化を支える Cubical Agda の環境。
- 宇宙レベル
- 型宇宙 Type ℓ の大きさを表す添字 ℓ。ホモトピーレベルや構成可能階層の一つの層とは異なる。
- Π 型
- 結果の型が入力に応じて変わりうる依存関数型。
- 依存関数
- Π 型の元。各入力に対し、その入力に対応する型の元を与える。
- Σ 型
- 第二成分の型が第一成分に依存しうる依存対型。
- 依存対
- Σ 型の元。選ばれた第一成分と、対応する型に属するデータの組。
- 第一成分
- 依存対で先に選ばれる元であり、fst で取り出す。
- 第二成分
- 型が第一成分に依存しうる依存対のもう一方の元であり、snd で取り出す。
- 証明書
- 後の議論でその性質を使えるよう、対象とともに携える証明。
- 優先順位
- 括弧を省いたときの演算子のまとまり方を決める規則。作れる式の種類は変わらない。
- 直和型
- A と B のどちら側から来たかと、その側の元を保持する帰納型 A ⊎ B。
- 帰納型
- 指定された構成子から生成され、対応する帰納原理によって要素を分析する型。
- 構成子
- 帰納型やレコード型の元を直接作り出す基本の操作。
- レコード型
- 名前付きフィールドで値をまとめる型。後のフィールドの型は先のフィールドに依存してよい。
- フィールド
- レコード型の名前付きの成分であり、同名の射影で取り出せる。
- 射影
- 対から成分を、レコードからフィールドを取り出す操作。
- パス
- 型の二つの元の間の等しさの証明。始点と終点を持ち、逆向きにも、つなぎ合わせることもできる。
- 判断的等しさ
- 型システムが定義と計算の規則によって認める等しさ。本書では = と書く。これは判断であって、パス型ではない。
- ホモトピーレベル
- 要素とその等しさの証明に区別できる構造がどれだけ残るかによる型の分類。
- 可縮
- 選ばれた中心を持ち、すべての元が中心とパスで結ばれる型。
- 一意存在
- 存在と一意性を合わせた概念。本書では可縮型で表し、その中心が必要な証人を与える。
- 命題
- 任意の二つの元が等しい型であり、証明が存在するかどうかだけを保つ。
- h-集合
- 等しさの型がすべて命題である型。元は互いに異なりうるが、同じ二元が等しいことの証明は互いに一致する。
- 型同値
- 型同値 A ≃ B は、各ファイバーが可縮である写像であり、逆写像と二つの往復パスはこの条件から導かれる。
- ファイバー
- 写像 f : A → B の b : B 上のファイバーは依存対型 Σ (a : A) (f a ≡ b) であり、その要素は原像と、それが b へ写ることを示すパスからなる。
- 同型
- 同型は順写像、逆写像、および二つの往復則を明示的に与える。
- 往復則
- 往復するとパスの意味で入力に戻ることを表す法則。f : A → B と g : B → A の二つの往復則は、すべての入力についての g (f a) ≡ a と f (g b) ≡ b である。
- 基礎型
- 型とともに収められた性質や構造を忘れて得られる型。P : hProp ℓ については第一成分 ⟨ P ⟩ である。
- 命題的切り詰め
- 型を、要素の有無が同じ命題へ送る操作。要素があることは保ち、それがどれであったかは忘れる。
- 高階帰納型 (HIT)
- 点の構成子だけでなく、パスやさらに高次のパスも構成子にできる帰納型。
- 単なる存在
- 命題的切り詰めで表す存在。∥ A ∥₁ は要素を指定せずに A に要素があることを述べ、∥ Σ[ x ∶ A ] P x ∥₁ は P を満たす証人の単なる存在を述べる。
- 空型
- 構成子を持たない型。元が存在しないので、任意の型へ消去できる。
- 論理的同値
- 論理的同値は両方向の含意を与え、命題については isProp によってそれらの写像を型同値へ高められる。
- クラス
- 与えられた論域上の述語。本書では、その論域から命題の宇宙への関数として表す。
- 論域
- 変数が動く型。論域と呼ぶだけでは、関係、演算、その他の構造は加わらない。
- 台
- 構造の対象を担い、その関係や演算が定義される基礎の型。
- 命題リサイズ
- 命題リサイズは、各命題を指定した宇宙レベルにある型同値な代表で置き換える。
- 命題宇宙リサイズ
- 命題宇宙リサイズは、命題宇宙全体を指定した宇宙レベルの型で提示する。
- 集合値族に対する選択
- h-集合 X と h-集合値の族 B に対し、添字ごとの単なる存在から、各 B x で要素を選ぶ依存関数の単なる存在が従う。SetChoice は X と各 B x の両方に h-集合性を要求する。
- 集合商
- A / R は点 [ a ]、R a b から得られるパス、および h-集合性を保証する構成子をもつ。R が命題値の同値関係なら、商類の間のパスから元の関係も得られる。
- 対象言語
- 項と論理式で集合論の主張を書く形式言語。その意味は別に与える。
- 項
- 一つの対象を指す書き方。ここでは定数名か変数位置から作る。
- 定数名
- K から選んで項を作る記号。構文だけでは、それが指す対象は決まらない。
- 定数域
- 項や論理式を作るときに使える定数名の型 K。モデルの台である必要はない。
- 文脈
- 式で現在使える変数位置の有限列。その長さが n である。
- 変数位置
- 現在の文脈で使える番号付きの場所。Fin n の元で表す。
- 論理式
- 原子的な比較、結合子、量化子から作る主張の書き方。構文だけでは成否は決まらない。
- 原子論理式
- 二つの項を所属または等号で直接比較した論理式。結合子や量化子はまだ加えていない。
- 量化子
- 「すべて」や「ある」を表す構文。本体には変数位置が一つ増える。
- 束縛変数
- 外側の量化子によって指す対象が与えられる変数の出現。
- 自由変数
- いま扱う量化子に束縛されず、外側の文脈から値を受け取る変数の出現。
- de Bruijn 添字
- 変数名を保存せず、出現位置から対応する束縛子までの距離を番号で表す方法。
- 有界量化子
- すべての対象ではなく、項が表す集合の要素に範囲を限る量化子。
- 文
- 自由変数をもたない論理式。定数名は含んでよい。
- 無パラメータ
- 定数名を含まない論理式。ここでは定数域を空型とし、自由変数は残ってよい。
- 環境
- 利用できる各変数位置に台の要素を割り当てるベクトル。長さは項や論理式の文脈の長さと一致する。
- 定数解釈
- 各定数名に台の要素を割り当てる関数 ι : K → S。量化子が変数の環境を拡張しても、この割当は変わらない。
- 項の評価
- 項の台における値 ⟦ t ⟧ γ を求めること。定数の値は ι から、変数の値は γ の対応する位置から得る。
- 充足関係
- 構造と定数解釈を固定したとき、γ ⊨ φ は環境 γ のもとで φ が成り立つという命題。意味を与えること自体は真偽の判定ではない。
- 構造の同型
- 構造の関係を保存し反映する台の間の全単射。ここでの関係は所属である。
一致する用語がありません。