Loading article…
数学において、ヒルベルトの第2問題は、 1900年にダフィット・ヒルベルトが23の課題の1つとして提起したものである。これは、算術が内部矛盾のない、つまり無矛盾であることを証明することを求めるものである。ヒルベルトは、算術に関して彼が考慮した公理は、ヒルベルト（1900）で示されたものであり、その中には2次完全性公理が含まれていると述べている。
1930年代、クルト・ゲーデルとゲルハルト・ゲンツェンは、この問題に新たな光を当てる結果を証明した。ゲーデルの定理は問題に対する否定的な解決策を与えると考える人もいれば、ゲンツェンの証明は部分的な肯定的な解決策だと考える人もいる。
ある英語訳では、ヒルベルトは次のように問いかけている。
「科学の基礎を研究する際には、その科学の基本概念間の関係を正確かつ完全に記述する公理系を構築しなければならない。…しかし、公理に関して問われる数多くの質問の中で、私が最も重要だと考えるのは次の点である。すなわち、公理が矛盾していないこと、つまり、公理に基づく一定数の論理的ステップが矛盾した結果を導き出すことは決してないことを証明することである。幾何学においては、公理の整合性の証明は、適切な数の体を構築することによって行うことができる。その体における数間の類似の関係が幾何学的公理に対応するようにする。…一方、算術的公理の整合性の証明には直接的な方法が必要である。」[ 1 ]
ヒルベルトの主張は時として誤解されることがある。なぜなら、彼が「算術的公理」と言ったのは、ペアノ算術と同等の体系ではなく、2階完全性公理を持つより強力な体系を意味していたからである。ヒルベルトが完全性証明を求めた体系は、 1階ペアノ算術よりも2階算術に近い。
現在では一般的な解釈として、ヒルベルトの第二の問いに対する肯定的な解答は、特にペアノ算術が無矛盾であることの証明となるだろう。
ペアノ算術が無矛盾であることを示す既知の証明は数多くあり、それらはツェルメロ＝フレンケル集合論のような強力な体系で実行できる。しかし、これらはヒルベルトの第二の疑問に対する解決策とはならない。なぜなら、ペアノ算術の無矛盾性を疑う者は、その無矛盾性を証明するために（はるかに強力な）集合論の公理を受け入れる可能性が低いからである。したがって、ペアノ算術が無矛盾であると既に信じていない者にも受け入れられる原理を用いて、ヒルベルトの問題に対する満足のいく解答を行う必要がある。このような原理は、完全に構成的であり、自然数の完全な無限を前提としないため、しばしば有限主義的と呼ばれる。ゲーデルの第二不完全性定理（ゲーデルの不完全性定理を参照）は、ペアノ算術の無矛盾性を証明しながら有限主義的体系がどれほど弱くてもよいかに厳しい制限を設けている。
ゲーデルの第2不完全性定理は、ペアノ算術が無矛盾であることを証明するいかなる証明も、ペアノ算術自体の中では実行できないことを示している。この定理は、許容される証明手続きが算術内で形式化できるものだけである場合、ヒルベルトの無矛盾性証明の要求には応えられないことを示している。しかし、Nagel & Newman (1958)が説明するように、算術で形式化できない証明の余地はまだある。[ 2 ]
1936年、ゲンツェンはペアノ算術が無矛盾であることの証明を発表した。ゲンツェンのこの結果は、集合論よりもはるかに弱い体系においても無矛盾性の証明が得られることを示している。
ゲンツェンの証明は、ペアノ算術の各証明に、証明の構造に基づいて順序数を割り当て、これらの順序数はすべてε 0より小さいという手順で進められます。[ 4 ]彼は次に、これらの順序数に対する超限帰納法によって、どの証明も矛盾に至らないことを証明します。この証明で使用される方法は、一階述語論理よりも強い論理でペアノ算術のカット除去結果を証明するためにも使用できますが、一貫性証明自体は、原始再帰算術の公理と超限帰納原理を使用して通常の一階述語論理で実行できます。テイト (2005)は、ゲンツェンの方法をゲーム理論的に解釈しています。[ 5 ]
ゲンツェンの無矛盾性証明は、証明論における順序数解析という研究プログラムの始まりとなった。このプログラムでは、算術や集合論の形式理論に、その理論の無矛盾性の強さを測る順序数が割り当てられる。ある理論は、より高い証明論的順序数を持つ別の理論の無矛盾性を証明することはできない。
ゲーデルとゲンツェンの定理は現在、数理論理学コミュニティでよく理解されているが、これらの定理がヒルベルトの第二問題に答えるかどうか（あるいはどのような方法で答えるか）については合意が形成されていない。シンプソン（1988）は、ゲーデルの不完全性定理は、強理論の有限的無矛盾性証明を生成することは不可能であることを示していると主張している。[ 6 ]クライゼル（1976）は、ゲーデルの結果は有限的構文的無矛盾性証明が得られないことを示唆しているが、意味論的（特に、2階）議論を使用して説得力のある無矛盾性証明を与えることができると述べている。デトレフセン（1990）は、ゲーデルの定理の仮説が無矛盾性証明を実行できるすべてのシステムに適用できるとは限らないため、ゲーデルの定理は無矛盾性証明を妨げるものではないと主張している。[ 7 ]ドーソン (2006)は、ゲーデルの定理が説得力のある無矛盾性証明の可能性を排除するという考えを「誤り」と呼び、ゲンツェンによる無矛盾性証明と、後にゲーデルが 1958 年に与えた無矛盾性証明を引用している。[ 8 ]