講演資料
講義資料スライドの表紙です。スライド画像、または下の要約文中の青いページ番号リンクをクリックすると、別のタブで無駄なノイズのない、純粋なPDFビューア画面が起動し、指定されたページへ直接ジャンプして快適に閲覧できます。
全体概要
本セミナーは、数学の基礎論と計算機科学が交差する最先端領域、すなわち「Homotopy Type Theory（HoTT）」と「Univalent Foundations」を中心的なテーマとして据えています。講義の問いの出発点は、極めて哲学的かつ数学的なものです——「同一性（Identity）とは何か」。ライプニッツが「識別不可能なものの同一性」として提起した問い [p.3] から始まり、プラトンのイデア論 [p.22], [p.23]、ラッセルの型理論 [p.84]、チャーチのλ計算 [p.92], [p.93]、Curry-Howardの対応 [p.100], [p.101] を経て、Martin-LöfのDependent Type Theory [p.108], [p.120] へと至る思想史的な系譜を丁寧に辿ります。
そしてその到達点として、フィールズ賞受賞者Vladimir Voevodsky（1966–2017）[p.2] が提唱した「Univalence Axiom」が登場します [p.4]。このアキシオムは「型と型の間のIdentity型は、それら二つの型の間の弱同値の型と自然に弱同値である」という宣言であり、数学における「同型なものは同一である（Isomorphic objects are identical）」という構造主義の原理 [p.135] を型理論の内部で正確に定式化するものです。
さらに本セミナーは量子力学・量子情報の基礎（Qubit、EPRペア、量子テレポーテーション）[p.46], [p.75] を並走させることで、「不可分性」「同一性」「非局所的な相関」といった概念が物理・数学・論理学にまたがる共通の問いであることを示唆します。Voevodsky自身がCoqによる形式証明の整備を急いだ動機 [p.5] ——すなわち「誤りと不必要な自己検証という苦しみを避けるために、証明支援システムが規範となるべきだ」という確信——もまた、本講義全体を貫く実践的な問題意識です。
同一性をめぐる哲学的探求が、20世紀の論理学・計算機科学の革新を経て、21世紀の数学基礎論における新しいパラダイムへと結実する——その知的旅程を一望できるのが本セミナーの最大の価値です。
講義のロードマップ
■ Part 0: 導入・動機・背景
- この部の核心:
本講義全体の問題意識と動機を提示します。Voevodsky の言葉 [p.4], [p.5] を引用しながら、Univalence Axiom という新公理の意義と、証明支援システムの必要性が論じられます。また講義全体のアジェンダが示され [p.9]、三つのPartの構成が明示されます。
- 論理展開:
- ライプニッツの「識別不可能なものの同一性」原理の引用により、Identity概念の問いが冒頭で立ち上げられます [p.3]。
- Voevodsky による Univalence Axiom の定式化と、証明支援システムへの切実な訴えが動機として提示されます [p.4], [p.5]。
- セミナー全体の三部構成（宇宙論・量子力学、量子情報、型理論史）が概観されます [p.9], [p.10], [p.11], [p.12]。
■ Part I: 宇宙論・時空・量子論の基礎
- この部の核心:
「同一性」と「構造」の問題を物理世界の側から照射するパートです。プラトンの洞窟の比喩 [p.22], [p.23]、実在論と唯名論の対立 [p.24], [p.25]、ライプニッツ–クラーク論争における空間の秩序論 [p.26]、そして宇宙の大規模構造から素粒子・量子論へと視野を広げ、「型（Form）」と「空（Emptiness）」の同一性というモチーフ [p.29] が提示されます。
- 論理展開:
- プラトンのイデア論（Form）が実在論の原型として示され、ペンローズの宇宙サイクル図 [p.33], [p.34] を用いた時空の構造論が展開されます。
- ライプニッツの空間観「空間は事物の秩序に過ぎない」[p.26] と数学的連続体（微積分の発明）[p.27] が接続されます。
- ウィトゲンシュタイン「およそ言い表せることは明確に言い表せる」[p.28] が型理論への橋渡しとして配置されます。
- Qubit・スピン・量子コンピュータの基礎が素粒子論（フェルミオン・ボソン）[p.49], [p.50] と接続され、「同一粒子の識別不可能性」という量子論的同一性問題が浮上します [p.51]。
■ Part II: 量子情報理論
- この部の核心:
量子情報の核心概念——Qubit、量子もつれ（Entanglement）、No Cloning定理、量子テレポーテーション——を体系的に解説するパートです。「情報のコピー不可能性」と「非局所的同一性の転送」というテーマが、後半の型理論における Identity の議論と深く呼応します。
- 論理展開:
- Qubitの定式化 `|ψ⟩ = α|0⟩ + β|1⟩`、ブロッホ球による幾何学的描像が提示されます [p.46], [p.47], [p.48]。
- EPRペア `1/√2 (|00⟩+|11⟩)` によるEntanglementの数学的定義と、積状態への分解不可能性が証明されます [p.53]。
- No Cloning定理（量子状態のコピー不可能性）が線形性から導かれます [p.63], [p.64]。
- 量子テレポーテーションのプロトコルが4段階の状態遷移 `|ψ₀⟩→|ψ₁⟩→|ψ₂⟩→|ψ₃⟩→|ψ₄⟩` として詳細に展開されます [p.70], [p.71], [p.72], [p.73], [p.74]。
- テレポーテーションの本質：古典通信2ビット＋EPRペアによる量子状態の完全転送、かつNo Cloningとの無矛盾性が確認されます [p.75]。
■ Part III: 型理論の思想史とHomotopy Type Theory
- この部の核心:
Leibniz → Russell → Church → Curry-Howard → Martin-Löf → Voevodsky という知的系譜を辿り、「命題とは何か」「証明とは何か」「同一性とは何か」という問いが型理論の発展の中でどのように深化してきたかを示します。そしてVoevodsky の Univalence Axiom が、この系譜の必然的な到達点として位置づけられます。
- 論理展開:
Leibniz の同一性論 [p.78], [p.79], [p.80], [p.81], [p.82], [p.83]
- 「識別不可能なものの同一性（Indiscernibility of Identicals）」と「同一なものの識別不可能性（Identity of Indiscernibles）」の区別が定式化されます。
- 等価関係（反射律・対称律・推移律）が Indiscernibility 公理から導出可能であることが示されます [p.81], [p.82], [p.83]。
Russell の型理論 [p.84], [p.85], [p.86], [p.87], [p.88]
- Frege の Comprehension Axiom が Russell のパラドックス `R = {x | ¬(x∈x)}` を引き起こすことが示されます [p.85], [p.86]。
- 解決策としての「悪循環回避原理」と階型理論（degree/order）が提示されます [p.87], [p.88]。
- ZF 集合論との対比と、古典論理（排中律）をめぐる直観主義との緊張が描かれます [p.89], [p.90]。
Church のλ計算 [p.92], [p.93], [p.94], [p.95]
- α変換・β簡約・η変換の三規則によるλ計算の定義 [p.93]。
- 単純型付きλ計算の型規則（変数・適用・抽象）[p.94]。
- 型付きλ計算が `Ω := (λx.xx)(λx.xx)` のような非停止項を排除することが示されます [p.95]。
Curry-Howard 対応 [p.100], [p.101], [p.104], [p.105], [p.106], [p.107]
- 「命題は型である（Propositions as Types）」「証明は項である（Proofs as Terms）」という PAT 対応の宣言 [p.101], [p.104]。
- `p : P` という記法が「p は P の証明である」と「p は P の要素である」の二重の意味を担うことが示されます [p.105], [p.106], [p.107]。
- Curry の 1934 年の発見 [p.102] と Howard の 1969/1980 年の定式化 [p.103] の歴史的経緯。
Martin-Löf の Dependent Type Theory [p.108], [p.116], [p.120], [p.121], [p.122], [p.123], [p.124]
- Dependent Type `Π(x:A).B(x)` により、型が項に依存する表現力が得られます [p.125], [p.126]。
- Identity Type `a = b : Id_A(a,b)` の導入：等式そのものが型であり、その要素が「等式の証明」です [p.122]。
- E3規則（elimination rule）による Identity Type の除去則：`f(a, refl(a)) := p` [p.123]。
- Inductive Type の定義（自然数を `0` と `S` で帰納的に定義する例）[p.128]。
Voevodsky の Homotopy Type Theory [p.130], [p.131], [p.132], [p.135], [p.136], [p.137]
- HoTT における `a : A` の解釈：Voevodsky の視点では「A は空間であり、a はその点である」[p.132]。
- 「同型なものは同一（Isomorphic objects are identical）」という構造主義の原理（PS）[p.135]。
- CauchyとDedekindによる実数の二定義が同型ゆえに同一視されるべきという例 [p.135]。
- Univalence Axiom の定式化：`A ≅ B ⟺ A と B が Identity である` [p.137], [p.149]。
- 同値（Equivalence）の三種類の定義（集合的・論理的・groupoid的）[p.148]。
- Identity / Isomorphy / Equivalence の三概念の関係整理 [p.152], [p.153], [p.154]。