型理論のはじまり
December 30, 2024型理論の起源はラッセルのパラドクスにある。 ただし、厳密な起源となる出来事は何かという問いになると、意見は分かれると思う。 名前の通り、ラッセルのパラドクスはラッセルが見つけたものだが、集合論を確立したカントールも同時期に独立して同等のパラドクスを発見した。 またラッセルとフレーゲの往復書簡の中で、フレーゲは、彼の概念記法における述語は述語を引数にとらないと回答した。 ラッセルが概念記法の要素の階層関係を発展させてパラドクスの解消を試みたことを考えれば、フレーゲの述語論理を型理論の起源とみなすこともできるだろう。
型理論のなりたちに興味があり、調べたことをスライドにまとめた。 興味があった理由は、その過程にコンピュータ科学以外の分野も関与していることにある。 カントールは数学者であり、フレーゲやラッセルは言語哲学でも参照される。 コンピュータ科学に関心がある人がコンピュータ科学に関連する分野を持ち、また、関連分野の知識をコンピュータ科学にどう活用できるかということに興味がある。 具体的には、数学、言語哲学、記号論などの抽象的な分野が日々のプログラミングに役立つのか、役立つのであれば、どのように関連分野に興味をもつことができるのかということが知りたかった。 そのため、歴史上の出来事の因果関係を慎重に議論するよりも、コンピュータ科学とほかの分野との関係に焦点をあててスライドを作った。
作成した資料は上のスライドであり、章立ては非ユークリッド幾何学の発見、素朴集合論、数理論理学になっている。 非ユークリッド幾何学の発見によって、すべての数学の対象は公理から構築されるものという見方がはじまった。 それから、カントールとデデキントが確立した集合論で数学の対象を定義するようになった。 フレーゲは、述語論理を提案した概念記法と集合論をもちいた論理学を数学を基礎にしようとした。 しかし、フレーゲの公理系からラッセルのパラドックスを導けるので、フレーゲの方法を見直す必要があることがわかった。 ラッセルは、概念記法のobject、述語、述語の述語という階層関係を発展してパラドクスを解消できないか考え、その草案をプリンキピア・マテマティカに記した。 今日、この述語論理の階層関係が型理論のはじまりと考えられている。