同じを考える ? 型の理論入門

全体概要

本セミナーは、「同一性（Identity）とは何か」という哲学的・数学的な根本問題を軸に据え、ライプニッツの不可識別者同一の原理から出発し、現代数学の最前線であるホモトピー型理論（Homotopy Type Theory, HoTT）へと至る壮大な知的旅程を辿るものです [p.3], [p.4]。

17世紀にライプニッツが「完全に区別のつかない二つの個体は存在しない」と述べたとき、彼は同一性の問題を哲学の中心に置きました [p.3], [p.41]。この問いは、20世紀に入ってフレーゲの集合論、ラッセルのパラドックス、そしてチャーチのλ計算と型理論へと受け継がれ、さらにカリー＝ハワード対応（Curry-Howard Correspondence）によって「命題」と「型」が、「証明」と「プログラム」が本質的に同一であるという深い洞察へと結実します [p.100], [p.101]。

そしてVoevodsky（1966–2017）は、この流れを受け継ぎながらも、従来の型理論では「証明の同一性」が一意に決まるという暗黙の前提を打ち破りました [p.2], [p.122]。彼は、Martin-Löfの依存型理論（Dependent Type Theory）に「単価公理（Univalence Axiom）」を付け加えることで、同型（isomorphic）な構造は同一（identical）であるという数学的構造主義の理想を、計算機上で厳密に形式化することに成功します [p.4], [p.149]。この体系はHoTTと呼ばれ、型をホモトピー空間として、同一性の証明をパスとして解釈することで、代数的トポロジーと型理論を統一する新たな数学の基礎を提供します [p.131], [p.160]。

本セミナーは単なる技術解説にとどまらず、Voevodsky自身が「コンピュータによる証明支援なくして数学の誤りは防げない」と警告した言葉 [p.5] を手がかりに、数学の厳密性と計算可能性の未来を問い直す、哲学・物理・情報科学を横断する知的探求です。

講義のロードマップ

■ Part I: 同一性の哲学的・物理的背景

• この部の核心:

「同一性」という概念を、哲学（プラトン、ライプニッツ、ウィトゲンシュタイン）、物理学（量子力学、素粒子、宇宙論）、仏教哲学という多角的な視点から照射します。同一性の問題は純粋に数学的・論理的なものではなく、物理世界の構造そのものに根差していることを示すことで、後半の型理論の議論に哲学的深みを与えます [p.14], [p.22], [p.23]。

• 論理展開:
• プラトンの洞窟の比喩を手がかりに、現象と実在（Form）の区別を論じ、数学的実在論（リアリズム）の立場を紹介します [p.22], [p.23], [p.24]。
• ライプニッツの「空間は事物の秩序である」という立場と、唯名論・実在論の対立を確認します [p.26], [p.25]。
• ウィトゲンシュタイン「5.5303」、仏教の「色即是空」など、同一性をめぐる多様な思想的立場を俯瞰します [p.28], [p.29]。
• 量子力学（スピン、フェルミオン、ボゾン）、量子ビット（Qubit）、エンタングルメントを通じて、物理的同一性の問題を具体的に提示します [p.45], [p.46], [p.49], [p.53]。

■ Part II: 量子情報理論と同一性

• この部の核心:

量子テレポーテーションを題材に、「情報の同一性」とは何かを具体的・技術的に掘り下げます。古典情報と量子情報の根本的な差異、No-Cloning定理、EPRペアによるテレポーテーションの数学的プロセスを丁寧に追うことで、「コピー不可能な同一性」という概念を物理的に確立します [p.53], [p.63], [p.65]。

• 論理展開:
• EPRペア `1/√2(|00⟩+|11⟩)` の生成と、2量子ビットのエンタングルメントが積状態に分解できないことを示します [p.53], [p.54]。
• No-Cloning定理：任意の未知量子状態 `|φ⟩` をコピーするユニタリー演算子は存在しないことを証明します [p.63], [p.64]。
• 量子テレポーテーションの全プロセス（`|ψ₀⟩` → `|ψ₄⟩`）を行列演算で追い、AliceのBell測定結果をもとにBobがX・Z変換を施すことで状態を復元することを示します [p.70], [p.71], [p.72], [p.73], [p.74]。
• テレポーテーションは情報の転送であり、量子状態の「コピー」ではないという、同一性の本質的区別を確認します [p.75]。

■ Part III: 論理・型理論と単価基礎

• この部の核心:

ライプニッツの同一性原理から出発し、フレーゲの集合論、ラッセルのパラドックス、チャーチのλ計算、カリー＝ハワード対応、マルティン＝レフの依存型理論、そしてVoevodskのホモトピー型理論（HoTT）へと至る型理論の歴史的発展を一気に辿ります。「同型なものは同一である」というUnivalence Axiomが、この長大な議論の帰結として提示されます [p.77], [p.131], [p.149]。

• 論理展開:

Leibniz — 不可識別者の同一性 [p.78], [p.79], [p.80]

• 同一性（`x = y`）を「すべての性質Pについて、P(x)ならばP(y)」という識別不可能性（Indiscernibility）で定義します。
• IndiscernibilityからRefl・Symm・Transが導出でき、等号関係が完全に公理化されることを示します [p.81], [p.82], [p.83]。

Russell — 型と階層 [p.84], [p.85], [p.86], [p.87], [p.88]

• フレーゲのComprehension Axiomからラッセルのパラドックス `R = {x | ¬(x∈x)}` が生じることを確認します。
• 解決策として、対象を「型（type）」と「階層（order）」によって分類する型階層理論を導入します。
• ZF集合論もまた、同様の問題意識から生まれた代替的基礎づけであることを指摘します [p.89]。

Church — λ計算と型付きλ計算 [p.92], [p.93], [p.94], [p.95]

• α変換、β簡約、η変換という3規則でλ計算を構成します。
• 型付きλ計算では `x_σ x_{σ→τ}` のような自己適用が排除され、発散項 `Ω := (λx.xx)(λx.xx)` が型付けできないことを示します。

Curry-Howard対応 [p.100], [p.101], [p.104], [p.105], [p.106]

• 「命題は型である（Propositions as Types）」「証明は項である（Proofs as Terms）」というPAT原理を確立します。
• `p : P` という記法が「pはPの証明」「pはPの要素」「pはPのプログラム」という三重の意味を持つことを示します。
• この対応がCoqなどの定理証明支援系の理論的基盤であることを確認します [p.104]。

Martin-Löf — 依存型理論 [p.108], [p.121], [p.122], [p.123], [p.124], [p.125], [p.126]

• 型が値に依存できる依存型（Dependent Type）`Π(x:A).B(x)` を導入します。
• Identity Type `a = b : Id_A(a, b)` を定義し、同一性の証明がそれ自体ひとつの型を成すことを示します。
• E3公理（J-rule）：`a = b` の証明 `e` と `P(a, refl(a))` の証明から `f(b, e) : P(b, e)` が構成できるという、同一性型の消去則を提示します [p.123]。

Voevodsky — HoTTと単価公理 [p.130], [p.131], [p.132], [p.135], [p.147], [p.148], [p.149], [p.155]

• HoTTでは `a : A` を「aはAという空間上の点」と解釈し、`a = b` の証明をaからbへのパス（homotopy）として幾何学的に読み替えます [p.132], [p.160]。
• 構造主義の原理「同型なものは同一である（Isomorphic objects are identical）」を動機として、Univalence Axiom `(A = B) ≃ (A ≅ B)` を定式化します [p.135], [p.149]。
• 同値（Equivalence）の3種の定義（同型写像の存在・単射性+全射性・groupoid的同値）を整理し、Univalence AxiomをCoqで形式化した`UniMath`ライブラリとして公開したことを紹介します [p.133], [p.148], [p.162]。
• 最終的に、HoTTは型を∞-groupoidとして解釈することで、ホモトピー論と型理論を統一する新たな数学の基礎となることを示します [p.131], [p.150]。