講演資料
講義資料スライドの表紙です。上のスライド画像をクリックすると、同じ画面のまま全編の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（19662017）[p.2] が提唱した「Univalence Axiom」が登場します [p.4]。このアキシオムは「型と型の間のIdentity型は、それら二つの型の間の弱同値の型と自然に弱同値である」という宣言であり、数学における「同型なものは同一である（Isomorphic objects are identical）」という構造主義の原理 [p.135] を型理論の内部で正確に定式化するものです。
さらに本セミナーは量子力学・量子情報の基礎（Qubit、EPRペア、量子テレポーテーション）[p.46p.75] を並走させることで、「不可分性」「同一性」「非局所的な相関」といった概念が物理・数学・論理学にまたがる共通の問いであることを示唆します。Voevodsky自身がCoqによる形式証明の整備を急いだ動機 [p.5] すなわち「誤りと不必要な自己検証という苦しみを避けるために、証明支援システムが規範となるべきだ」という確信もまた、本講義全体を貫く実践的な問題意識です。
同一性をめぐる哲学的探求が、20世紀の論理学・計算機科学の革新を経て、21世紀の数学基礎論における新しいパラダイムへと結実するその知的旅程を一望できるのが本セミナーの最大の価値です。
講義のロードマップ
ここでは、セミナーの講演資料がどのようなパートから構成されているかを示します。また、それぞれのパートのポイントを紹介します。
■ Part 0: 導入・動機・背景
本講義全体の問題意識と動機を提示します。Voevodsky の言葉 [p.4, p.5] を引用しながら、Univalence Axiom という新公理の意義と、証明支援システムの必要性が論じられます。また講義全体のアジェンダが示され [p.9]、三つのPartの構成が明示されます。
■ Part I: 宇宙論・時空・量子論の基礎
「同一性」と「構造」の問題を物理世界の側から照射するパートです。プラトンの洞窟の比喩 [p.22, p.23]、実在論と唯名論の対立 [p.24, p.25]、ライプニッツクラーク論争における空間の秩序論 [p.26]、そして宇宙の大規模構造から素粒子・量子論へと視野を広げ、「型（Form）」と「空（Emptiness）」の同一性というモチーフ [p.29] が提示されます。
■ Part II: 量子情報理論
量子情報の核心概念Qubit、量子もつれ（Entanglement）、No Cloning定理、量子テレポーテーションを体系的に解説するパートです。「情報のコピー不可能性」と「非局所的同一性の転送」というテーマが、後半の型理論における Identity の議論と深く呼応します。
■ Part III: 型理論の思想史とHomotopy Type Theory
Leibniz → Russell → Church → Curry-Howard → Martin-Löf → Voevodsky という知的系譜を辿り、「命題とは何か」「証明とは何か」「同一性とは何か」という問いが型理論の発展の中でどのように深化してきたかを示します。そしてVoevodsky の Univalence Axiom が、この系譜の必然的な到達点として位置づけられます。
ページのナビゲート