Loading article…
ゲンツェンの無矛盾性証明は、ゲルハルト・ゲンツェンが1936年に発表した数理論理学における証明論の成果である。この証明は、証明に用いられるある別の体系にも矛盾がない限り、一階述語論理のペアノ公理系には矛盾がないこと（すなわち「無矛盾」であること）を示している。この別の体系は、今日では「順序数ε₀までの量化子なし超限帰納法の追加原理を持つ原始再帰的算術」と呼ばれており、ペアノ公理系よりも弱くも強くもない。ゲンツェンは、この体系はペアノ算術に含まれる疑わしい推論方法を回避しており、したがってその無矛盾性は議論の余地が少ないと主張した。
ゲンツェンの定理は、一階算術、すなわち自然数の理論（加算と乗算を含む）に関するものであり、一階ペアノ公理によって公理化されています。これは「一階」理論であり、量化子は自然数に及びますが、自然数の集合や関数には及びません。この理論は、べき乗、階乗、フィボナッチ数列など、再帰的に定義される整数関数を記述するのに十分な強度を持っています。
ゲンツェンは、一次ペアノ公理の無矛盾性が、量化子なし超限帰納法の追加原理を順序数ε₀まで加えた原始再帰算術の基本理論上で証明可能であることを示した。原始再帰算術は、かなり単純化された算術の形式で、議論の余地はほとんどない。追加原理は、非公式には、有限根付き木の集合上に整列が存在することを意味する。形式的には、ε₀は最初の順序数である。そのためつまり、数列の極限
これは、大きな可算順序数よりもはるかに小さい可算順序数です。順序数を算術の言語で表現するには、順序数表記法、つまり ε 0より小さい順序数に自然数を割り当てる方法が必要です。これはさまざまな方法で実行できますが、1 つの例はカントールの標準形定理によって提供されています。ゲンツェンの証明は、次の仮定に基づいています。任意の量化子のない式 A(x) に対して、A(a) が偽となる順序数a < ε 0が存在する場合、そのような順序数の最小値が存在する。
ゲンツェンは、ペアノ算術における証明のための「還元手続き」の概念を定義している。与えられた証明に対して、この手続きは証明の木を生成する。与えられた証明は木の根となり、他の証明はある意味で与えられた証明よりも「単純」である。この単純化の増大は、すべての証明に < ε 0という順序数を付加し、木を下に進むにつれてこれらの順序数がステップごとに小さくなることを示すことによって形式化される。そして彼は、矛盾の証明が存在する場合、還元手続きは、量化子のない式に対応する証明に対する原始的な再帰操作によって生成される、 ε 0より小さい順序数の無限に厳密に減少する列をもたらすことを示している。[ 1 ]
ゲンツェンの証明は、ゲーデルの第二不完全性定理のよく見落とされがちな側面を浮き彫りにしている。理論の無矛盾性は、より強い理論でのみ証明できると主張されることがある。原始再帰算術に量化子なし超限帰納法を追加して得られたゲンツェンの理論は、一階ペアノ算術（PA）の無矛盾性を証明するが、PAを包含しない。例えば、PAはすべての数式に対して通常の数学的帰納法を証明できるのに対し、ゲンツェンの理論はそれを証明できない（帰納法のすべての事例はPAの公理であるため）。しかし、ゲンツェンの理論はPAに含まれない。なぜなら、PAでは証明できない数論的事実、すなわちPAの無矛盾性を証明できるからである。したがって、この二つの理論はある意味で比較不可能である。
とはいえ、理論の強さを比較するより洗練された方法も存在し、その中でも最も重要なのは解釈可能性という概念で定義されるものです。ある理論Tが別の理論Bにおいて解釈可能であれば、Bが矛盾しないならばTも矛盾しないことが示せます。（実際、これは解釈可能性という概念の重要なポイントです。）そして、Tが極めて弱い理論でない限り、T自身もこの条件付き命題を証明できます。すなわち、Bが矛盾しないならば、Tも矛盾しないということです。したがって、第二不完全性定理により、TはBが矛盾しないことを証明できませんが、BはTが矛盾しないことを証明できる可能性があります。これが、理論を比較するために解釈可能性を用いるという考え方、つまり、BがTを解釈できるならば、Bは少なくともTと同程度に強い（「矛盾しない強さ」という意味で）という考え方を動機づけるものです。
パヴェル・プドラック[ 2 ]がソロモン・フェファーマン[ 3 ]の以前の研究に基づいて証明した、第2不完全性定理の強い形式は、ロビンソン算術Qを含む無矛盾な理論Tは、Tが無矛盾であるという命題Q+Con(T)を解釈できないと述べている。対照的に、算術化された完全性定理の強い形式により、Q+Con(T)はTを解釈する。したがって、Q+Con(T)は常にTよりも強い（ある意味で）。しかし、ゲンツェンの理論はQを含みCon(PA)を証明するので、自明にQ+Con(PA)を解釈し、したがってゲンツェンの理論はPAを解釈する。しかし、プドラックの結果によれば、ゲンツェンの理論は（前述のように）Q+Con(PA)を解釈し、解釈可能性は推移的であるため、PAはゲンツェンの理論を解釈できない。つまり、PAがゲンツェンの理論を解釈するとすれば、Q+Con(PA)も解釈することになり、プドラックの結果によれば矛盾が生じる。したがって、解釈可能性によって特徴づけられる一貫性の強さという観点から言えば、ゲンツェンの理論はペアノ算術よりも強い。
ヘルマン・ワイルは1946年に、ゲーデルの1931年の不完全性定理がヒルベルトの数学の無矛盾性証明計画に壊滅的な影響を与えたことを受けて、ゲンツェンの無矛盾性定理の重要性について次のようにコメントした。[ 4 ]
クリーネ（2009年、479ページ）は、1952年にゲンツェンの結果の重要性について、特にヒルベルトによって始められた形式主義プログラムの文脈において、次のようにコメントした。
それとは対照的に、ベルネイズ（1967）は、ヒルベルトが有限的方法に限定したことが制約が厳しすぎるかどうかについて次のようにコメントした。
ゲンツェンの無矛盾性証明の最初のバージョンは、ポール・ベルネイズが証明の中で暗黙のうちに用いられている手法に異議を唱えたため、彼の生前には発表されなかった。上記で説明した修正された証明は、1936年に『アナルズ』誌に掲載された。ゲンツェンはその後、1938年と1943年にさらに2つの無矛盾性証明を発表した。これらはすべて（Gentzen & Szabo 1969 ）に収録されている。
クルト・ゲーデルは1938年の講演で、ゲンツェンの1936年の証明を再解釈し、後に反例なし解釈として知られるようになった。元の証明と再定式化の両方をゲーム理論の観点から理解することができる。（テイト 2005 ）。
1940年、ヴィルヘルム・アッカーマンは、順序数ε 0を使用したペアノ算術の別の無矛盾性証明を発表した。
算術の一貫性に関する別の証明は、1959年にI.N.クロドフスキーによって発表された。
ゲンツェンの証明は、証明論的順序数解析と呼ばれるものの最初の例である。順序数解析では、整列していることが証明できる（構成的）順序数の大きさを測定することによって、あるいは同等に、超限帰納法が証明できる（構成的）順序数の大きさを測定することによって、理論の強さを測る。構成的順序数とは、自然数の再帰的整列の順序型のことである。
この言語では、ゲンツェンの研究では、1階ペアノ算術の証明論的順序数は ε 0であることが確立されています。
ローレンス・カービーとジェフ・パリスは1982年に、グッドスタインの定理はペアノ算術では証明できないことを証明した。彼らの証明はゲンツェンの定理に基づいていた。[ 5 ]
