「同じ」を考える -- 「型の理論」入門

2019年1月29日 2021年12月16日 MaruyamaFujio

2019/01/29　「同じ」を考える -- 「型の理論」入門　概要

セミナーの呼びかけ

数学では、「同じ」「等しい」というのは、もっとも基本的な概念の一つです。
　「2 x 3 は、3 x 2 と同じである」
　「2辺とその狭角が等しい三角形は、同じ三角形である」
　「自然数と有理数は、同じ数だけ存在する」
　「ドーナツとコーヒーカップは、実は、同じ形である」
ただ、これらの例での「同じ」は、全く「同じ」ではありません。

日常でも、「同じ」という言葉は、よく使われます。
　「彼と僕の身長は同じです」
　「同じ時間、同じ場所で、共に過ごした仲間」
　「みな、同じ気持ちです」
　「この英語と日本語の文章は同じ意味です」
ここでも、「同じ」という言葉は、全く「同じ」ではありません。

これらの表現を、「同じ」という言葉を使わない表現で言い換えて
みようとすると、とても難しいことに気づきます。それは、「同じ」
という概念が、他の言い換えができないほど基本的な概念であることを
意味しています。

セミナーでは、自明なように見えるが、多様さも併せ持つ、「同じ」の
数理を探ります。セミナーでは、また、一昨年急逝した数学者のVoevodskyの
「同一性」をキーコンセプトにした数学の基礎づけの試みを紹介します。

「はじめに」から

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

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

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