概要

フレーゲが創始した述語論理が数学を基礎づけるまで

オブジェクトレベルの話

フレーゲ「なんか凄い記法作った」: 「概念記法」を記し、述語論理を創始。その勢いで数学を論理学に還元しようとする。「算術の基本法則」を出版したが、ラッセルが「その方法ではパラドックスが発生してしまう」と指摘し、二階述語論理ではうまくいかないことが明らかに。

ラッセル「タイプ理論でパラドックスを回避できた」: 数学を論理学に還元するというフレーゲの試みを継承。パラドックスが生じないように述語論理を上手く手なずける タイプ理論を創始。「プリンキア・マティマティカ」を記し、その有用性を世界に知らしめた。とはいえ、現在では主流でない。間違いが発見されたというのではなく、ツェルメロの方法がよりよかったため。タイプ理論の公理が人間には哲学的観点から承服が難しかったという側面もある。

ツェルメロ「一階述語論理で数学を基礎づけできた」: ZFC と呼ばれる公理系を整備。一階述語論理にいくつかの公理(公理図式＝無限の公理が必要なものも含む)を付け加えると、数学の大部分を基礎づけできることを示す。現在の集合論、ひいては数学はこれに基礎づけされている。

論理や数学自身の評価

メタレベルの話。論理学は「正しい道具立て」なのだろうか？をしっかりするべきとの問題認識。ラッセルのパラドックスのようなことが他に起きないようにしたい。

ヒルベルト「有限の立場で！」: 論理学の営みを二段階に分けよう。オブジェクトレベルでは、意味を忘れてただの記号変形ゲームに落とし込んで各種の知見を得ればよい、メタレベルでは、有限の方法（数学的帰納法など）を用いて論理学/数学 の健全性や完全性を議論すればよい。

ゲーデル「一階述語論理は完全だったよ」: 無矛盾性=健全性 は知られていたので、一階述語論理は無矛盾で完全であることが分かった。つまり「正しい文は証明できるし、証明できる文は正しい」。

ゲーデル・ロッサー「でも、数学は完全じゃないかも」: 上述の意味とは異なる完全性に対して否定的に答えた。つまり「初等的な算術を含む理論が無矛盾であれば 証明も反証もできない文が存在する」ことを実際にその文を構成してみせた。ZFC を含む大体の公理系はこの条件を満たす。この文は見るからに正しいので「数学には 正しいけど証明できない命題がある」。

ゲーデル「さらに、数学は無矛盾とも言い切れないんだよね」: 初等的な算術を含む理論の無矛盾性を、有限の立場で証明できないこともいえる。これはヒルベルトの目論見を完全に打ち砕かれた。

ゲンツェン「超限帰納法つかったら数学の完全性を証明できたよ」: ヒルベルトの「有限の立場」というのをあきらめて、メタのレベルで超限帰納法を使えば完全性を証明できた。ただし、どんな道具立てがメタレベルの議論で許容されるのかは哲学的な議論が必要。

計算と論理の話

論理とコンピュータの話。

チューリング＆チャーチ「計算に対する定義をしてみた」: チャーチ・チューリングのテーゼによって、「計算可能である」ということをチューリングマシンやラムダ計算（この二つは同等の「計算」能力を持つ）で定義できるのでは、と提案。