講演資料
講義資料スライドの表紙です。上のスライド画像をクリックすると、同じ画面のまま全編のPDF資料を快適に閲覧・印刷することができます。
セミナーの概要
本セミナーは、「同一性（Identity）とは何か」という哲学的・数学的な根本問題を軸に据え、ライプニッツの不可識別者同一の原理から出発し、現代数学の最前線であるホモトピー型理論（Homotopy Type Theory, HoTT）へと至る壮大な知的旅程を辿るものです [p.3, p.4]。
17世紀にライプニッツが「完全に区別のつかない二つの個体は存在しない」と述べたとき、彼は同一性の問題を哲学の中心に置きました [p.3, p.41]。この問いは、20世紀に入ってフレーゲの集合論、ラッセルのパラドックス、そしてチャーチのλ計算と型理論へと受け継がれ、さらにカリー＝ハワード対応（Curry-Howard Correspondence）によって「命題」と「型」が、「証明」と「プログラム」が本質的に同一であるという深い洞察へと結実します [p.100, p.101]。
そしてVoevodsky（19662017）は、この流れを受け継ぎながらも、従来の型理論では「証明の同一性」が一意に決まるという暗黙の前提を打ち破りました [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]。
■ Part II: 量子情報理論と同一性
量子テレポーテーションを題材に、「情報の同一性」とは何かを具体的・技術的に掘り下げます。古典情報と量子情報の根本的な差異、No-Cloning定理、EPRペアによるテレポーテーションの数学的プロセスを丁寧に追うことで、「コピー不可能な同一性」という概念を物理的に確立します [p.53, p.63, p.65]。
■ Part III: 論理・型理論と単価基礎
ライプニッツの同一性原理から出発し、フレーゲの集合論、ラッセルのパラドックス、チャーチのλ計算、カリー＝ハワード対応、マルティン＝レフの依存型理論、そしてVoevodskのホモトピー型理論（HoTT）へと至る型理論の歴史的発展を一気に辿ります。「同型なものは同一である」というUnivalence Axiomが、この長大な議論の帰結として提示されます [p.77, p.131, p.149]。
ページのナビゲート