数学基礎論論争は結局どうなったか

数学に関心のある人なら、20世紀の初めに「数学基礎論論争」があったことをぼんやりとは聞いたことがあると思います。数学基礎論論争が結局どうなったかについて書きます。

数学基礎論論争とは

19世紀を通じて数学は厳密化の道をたどってきました。たとえばフーリエ級数の収束については多くの誤った「証明」がなされ、最終的に「測度0上の除外点を除いて収束する」という条件にたどりついたのは20世紀になってからです。そして「測度」という概念を定式化するには集合論が不可欠です。

そこで集合論を厳密に公理的に取り扱う試みが行われましたが、ここで表面化したのが集合論のパラドックスです。例えばXを自分自身を元として含まない集合の集合としましょう。さてX∈Xでしょうか。X∈XとするとXの定義からXの元ではありません。一方X∈Xではないとすると、X∈Xのはずです。いずれにしても矛盾が導かれます。

このようなパラドックスにどう対応するかという問題を契機にして、数学をどのように行うべきか関する論争が行われました。これを数学基礎論論争といいます。数学の危機とも呼ばれます。

ただし、この「危機」の最中にも数学は普通に発展していました。したがって「危機」というのは誇張だという考えもあります。また、現代から見ると何を論争しているかよくわからないところがあります。個人的な誤解にもとづく争いであったと考える人もいるようです（ファン・ダーレンとか）。また、単に集合論のパラドックスの解決を目指したものではなく、無矛盾性や数学の確実性を担保することだけがゴールでもありませんでした。

論理主義

論理主義は最初にフレーゲが唱えた立場です。「数学はじつは論理である」という主張です。フレーゲはこの立場に立って論理と数学の形式体系を歴史上初めて提示しました。しかしこの体系は集合論のパラドックスと同じ問題が含まれており、晩年にはフレーゲはこれを放棄しています。その後ラッセルがフレーゲの体系に修正を加え矛盾を取り除いた上、全数学の形式化を目指す「プリンキピア・マテマチカ」を書きました。

論理主義の問題は、そもそもここでいわれている論理とは何か、ということです。フレーゲやラッセルが論理という言葉で何を考えていたかは思想史の問題になります。そもそも論理とは何か、は論理学の哲学の問題です。ラッセルの体系は形式的には現在の高階論理と言われているものに当たります。高階の論理はその正しい推論を完全に網羅する推論規則が存在しないという問題があります。論理といえばなにか「自明に正しい」とか「確実」というイメージがありますが、高階論理には「正しい推論」の定義に集合の性質が本質的に含まれているので、高階論理にそのようなことが言えるかどうか疑問です。もっとも現在のまともな論理学者で論理が「自明に正しい」とか「確実」とか思っている人はいないと思います。

形式主義

形式主義はヒルベルトが唱えた立場とされています。「無限について」という講演でヒルベルトは、まず「無限」への言及を含むような理論Tを考えます。無限に関わる言明は有限の手段では真偽が確かめることができず、意味がはっきりしないとも言えます。しかし、Tの論証を形式論理で書けば、Tの論証自体は記号列なので有限的な対象になります。Tの無矛盾性が有限的な（今風の言い方で言えば計算可能な）対象についての理論だけで証明できたとします。するとΠ01文という特別な形の文については、Tでそのような文Sが証明できると、Sの有限的な証明があります。Tでの証明はSの有限的な証明をそれ自体としては「意味がない」無限的な概念を経由して証明したものとみなせます。

Π01文とはすべてのxについてA(x)という形をしていて、A(x)は有限的な（計算手続きでテスト可能な）文のことです。例えばABC予想はΠ01文です（詳しい人むけ：一見実数が出てきますが、有理数近似をすることによりΠ01文に落とすことができます）。もし理論Tが無矛盾で、なおかつあるΠ01文∀xA(x)を導いたとしましょう。∀xA(x)とは「すべてのxについてA(x)」という意味です。一方である自然数nでA(n)ではなかったとしましょう。A(n)かどうかは具体的な計算手続きで確かめられます。具体的な計算手続きはTの中でも実行可能ですから、Tは「A(n)ではない」を導きます。これはTは「すべてのxについてA(x)」を導きますから、とくにTはA(n)を導きます。これは矛盾です。よってA(n)はかならず成り立ちます。nは任意でしたから∀xA(x)が（Tの中で導かれるというだけでなく）有限的な理論でも示せることになります。

形式主義は失敗したということになっています。ゲーデルの不完全性定理より、Tの中に含まれる手段ではTの無矛盾性を示すことはできません。有限的な理論がTに含まれていると考えれば、Tの無矛盾性を有限的に示すことはできません。

ただ、個人的にはこの結論は性急だと思っています。Tに含まれない有限的な原理を想定することが可能だからです。例えば、順序数解析では自然数上のある種の順序について帰納法が可能であることから、いろいろな数学体系の無矛盾性を示しています。

直観主義（構成主義）

直観主義数学とは、オランダの数学者ブラウアー(1881-1966)によって提唱された立場です。直観主義数学は排中律（任意の命題Pについて「PであるかPでないかどちらかである」とする主張)を否定する数学と紹介されることがありますが、排中律を否定するのはその主張の一部であって、他の古典数学の主張も否定されたり、古典数学とは相容れない独自の主張がなされることもあります。また、気まぐれに排中律を否定しているわけではなく、その背景には理由付けが存在します。

直観主義数学は大雑把に言って「具体的に操作可能なもの」だけが数学の対象だと考えます。そして、何かが存在すると主張することはそれを「構成」することだと考えます。また、「証明」自体も数学の対象です。ただし、数学の証明とは形式論理の推論の並びではなく、ある数学的命題の正しさを「構成」する「直観」です。

例で考えてみましょう。次のような問題を考えます。

「二つの無理数a, bでaのb乗が有理数になるものがある。」

通常これはこのように証明されます。

まず√2の√2乗を考えます。これが有理数ならば証明は終わりです。もし無理数だとすると、√2の√2乗の√2乗を考えます。√2の√2乗の√2乗＝√2の2乗＝2ですから有理数です。a=√2の√2乗、b=√2とおけば命題が証明されます。

この「証明」は直観主義の立場からは証明ではありません。a, bを具体的に与えていないからです。ちなみに√2の√2乗は超越数なので、a=b=√2とおけばこの命題は証明されますが、証明は遥かに難しいです。

上の「証明」が成り立つのは排中律「√2の√2乗は有理数であるかそうでないかのどちらかである」を使っているからです。したがって、直観主義数学では排中律は論理の法則として採用されません。

直観主義数学は数学をあまりに煩雑にするとして、一般の数学者からは受け入れられませんでした。しかし、「具体的に操作可能なものだけを考える」「証明自体を基本的な対象として考える」といった立場は計算機科学と親和性が高く、現在も研究が続いています。例えば、定理証明支援系のCoqやAgdaは直観主義論理に基づいています。また、新しい数学の基礎として注目されているホモトピー型理論は直観主義型理論にUnivalent axiomという公理を追加したものになっています。また、古典的な数学をある程度直観主義の数学で解釈することが可能です。なので真っ向から対立するものだ、と考える必要はないことを付け加えておきます。

その後どうなったか

集合論のパラドックスについては、矛盾を含まないだろうと思われるZFCという小公理系が整備されて、あまり問題にならなくなりました。一方で、数学基礎論論争をきっかけに始まった数学の基礎についての研究は、数理論理学という形で（数学の基礎とはもはやあまり関係はなく）発展しています。また、集合論は圏論を扱うのがやや不便なので圏論そのものを基礎に据える考えや、直観主義の立場にたったホモトピー型理論などが新しい数学の基礎として研究されています。