「同じ」を考える -- Univalence Axiom 入門

2022/03/01 マルゼミ「「同じ」を考える -- Univalence Axiom 入門」

小論は、2019 年1月29日のセミナー「「同じ」を考える -- 「型の理論」入門」をベースにして、Homotopy Type Theory の Univalence Axiom にフォーカスしてバージョンアップしたものです。以前のは、音声なしの「無声映画」だったのですが、今回は、その「talkie 版」です。

「2022/03/01 マルゼミ」という記されていますが、これは、この日にセミナーを行うことを意味していません。この日から、コンテンツの配信が始まるものとお考えください。可能であれば、セミナーの開催とコンテンツの配信を分離するスタイルを進めていきたいと思っています。

「はじめに」から（旧バージョン）

「同じ」あるいは「同じではない」という判断は、知覚にとっても認識にとっても、最も基本的な判断の一つである。認識の対象が、自然であれ、人間であれ、あるいは、思惟が産み出す抽象的な概念であれ、その認識の土台には、対象の「同一性」についての判断があるように思う。
小論の第一部では、まず、日常の生活の中にも現れる「同じ」をめぐる問題を、いくつかのサンプルで考えてみようと思う。その後で、「哲学者」たちが、こうした問題をどのように考えていたのかを、きわめて簡単に振り返ろうと思う。
残念ながら、小論は、「同一性」についての、「哲学的」議論を紹介することを目的とはしていない。ただ、第一部での議論を通じて、日常の中にも、浅からぬ哲学への入り口が存在していることを意識することを楽しんでもらえれば嬉しいと思う。

小論の第二部では、20世紀の科学が、すくなくとも自然認識の領域では、「同一性」概念の大きな変化を引き起こしたことを述べようと思う。
相対論は、宇宙規模の巨大な空間では、時間の「同時性」が成り立たないことを示し、量子論は、極めて微小な領域では、すべての物質と力は、「同じ」性質を持つ不断に変化する素粒子の運動として記述できることを示した。同時に、両者ともに、その法則性は、ある種の「不変性」として記述される。
物理的な「同一性」は、基本的には「情報」の「同一性」として表現されるのだが、この分野でも、量子情報理論の発展は、エンタングルメントや量子テレポーテーションといった、「同一性」にかかわる思いがけない知見を我々にもたらしている。

小論の第三部は、数学での「同一性」にまつわる議論を、「型の理論」の成立と発展を中心に概観したものである。
「型の理論」は、20世紀初頭のラッセルに始まる。40年代のチャーチの「型付きラムダ計算」を経て、70年代には、マーティン・レフの「従属型理論」として発展してきた。その理論は、「関数型言語」の成立に大きな影響を与えた。
21世紀に入ってから、この分野は、ヴオェボドスキーの「ホモトピー型理論」の登場によって、大きな飛躍を遂げる。彼がこの理論の基礎に置いた “Univalent Axiom” は、「同一性」についての新しい原理に他ならない。それは、数学の基礎そのものについての新しい洞察を可能にするものであった。
彼が、この理論の展開をすべてコンピュータを使った証明支援システム上で行なったことは、特筆に値する。