不完全性定理自然数論をどう形式化しても、決定不能な命題が存在するゲーデルの第一不完全性定理

クルト・ゲーデル

形式体系が健全で、その中で自然数の和積演算が
正しく行えるなら、証明も反証もできない命題がある。
※健全とは、証明できる命題がすべて真になること。改良条件については下記の【補足説明】【補足説明】ゲーデルの不完全性定理の原論文においては、形式体系に対する仮定は「健全性」より少し弱い「ω無矛盾性」という条件で、体系がω無矛盾であるとは「どの論理式A(x)についても、∃x A(x)が証明できれば、¬A(n*)が証明されない自然数nがある」ことをいう。ここで、n*は自然数nを形式的に表現する記号列で、例えば 3*は「1+1+1」などとする。そして、ゲーデルの結果を厳密に述べれば、(1) 無矛盾な体系では、Gは証明できない。(2ω無矛盾な体系では、¬Gは証明できない。となる。(2)の仮定を「無矛盾」に弱めたのはロッサーの仕事(1936年)である。 を参照。

ゲーデルはこの定理の証明に向けて、「自らが証明できない」という意味をもつ文(厳密にいえば、それと同値な文)を形式体系の中で構成した。これをゲーデル文Gといい、以下で示すように文Gは証明も反証もできない。

数学を語る言葉ないしそれに関する約束事を「メタ数学」という。ゲーデルは記号列に自然数のコード(「ゲーデル数」)を一意に割り振る方法を考案して、例えば「ゲーデル数n の論理式が証明可能である」というメタ数学的言明が、自然数n に関する述語とみなせることに注目した。ゲーデル数の扱いにおいて基本となる数学的事実はどの自然数も一意に素因数分解できることで、さらに次の事実も使われるので、考えてみよう。

問1 k より大きな素数は、k !+1以下に存在することを示せ。ただし、k ! =1・2・3・4・・・・・k である。

k ! +12k のどの数で割っても1余るから、言い換えれば2k のどの数でも割り切れない。そこで、k ! +1の最小の素因数を考えると、それは k より大きいことが分かる。つまり、k ! +1以下の範囲にk より大きい素数がある。この原理は、メタ数学を算術化する際に必要概念が再帰的に(Δ1論理式で)定義されることを確認するために頻繁に用いられる。

問2 3で割ると2余り、5で割ると3余り、7で割ると2余る数は何か?

3〜5世紀の中国の算術書『孫子算経』に解説されている問題である。
この解法には 3・ 5・7 = 105 という数が鍵になるので、江戸時代の和算では百五減算という名で知られた。まず、
 5×7 の倍数で、3で割ると1余る数は、70
 3×7 の倍数で、5で割ると1余る数は、21
 3×5 の倍数で、7で割ると1余る数は、15
したがって、求める解(の一つ)は 70×2 + 21×3 + 15×2 = 233 である。一般解は、合同式 𝑥 233 (mod 105) で与えられる。その最小解を求めるには、233から次々と105を減じ、233-105=128、128-105=23。よって、23が最小解である。
ゲーデルは、これを一般化した原理(中国剰余定理)を用いて、数列を一つの数で表す方法を開発した。簡単に説明すると、予め素数の列 3, 5, 7, … を固定しておき、例えば数列 (2, 3, 2) には今求めた数 23 を対応させると、それを3, 5, 7で割ることで、2, 3, 2 をそれぞれ余りとして取り出すことができる。ゲーデルの論文はとても丁寧に書かれているものの、あくまで数学者向けで、このような基本原理は既知とされる。さらに詳しくは、田中一之氏の著書『ゲーデルに挑む』に説明がある。

原論文の「17Gen r」

以下では、0も自然数とする。まず、「変数𝑥 に関する論理式」を(ゲーデル数の)大きさの順に並べる。F0(𝑥 ), F1(𝑥 ), F2(𝑥 ), ... 。たとえば、F0(𝑥 )は「𝑥 は偶数である」、F1(𝑥 )は「𝑥 >0」などだ。そして、「論理式F𝑥 (𝑥 )が証明できない」という論理式をP(𝑥 )とする。たとえば、P(0)は「F0(0)が証明できない」、つまり「「0は偶数である」が証明できない」になる。すると、P(𝑥 )も𝑥 に関する論理式なので、あるk が存在して、Fk (𝑥 )がP(𝑥 )と一致する。そこで、𝑥 =k とおけば、Fk (k ) は P(k )と一致する。他⽅、P(k )は「Fk (k )が証明できない」を表しているから、Fk (k )をGと置き直せば、Gは「Gが証明できない」を表しており、これがゲーデル⽂となる。

※もう少し厳密にみると、P(𝑥 ) ≡ 「F𝑥 (𝑥 )が証明できない」の右辺は、各 𝑥 毎にF𝑥 (𝑥 )が証明できないとそのまま書かれるのではなく、F𝑥 (𝑥 )のゲーデル数を並べ上げる関数と証明(不)可能性を表す述語を合成した論理式によって表わされる。したがって、Fk (k ) と P(k ) は論理的に同値にはなるのだが,文字列として一致しているわけではない。つまり、G と 「Gが証明できない」 は同値であるが、G は 「自らが証明できない」 ことをそのまま表しているわけではない。

ゲーデル⽂Gは健全な算術体系では証明も反証もできない。

最初に、Gが証明されたと仮定して矛盾を導く。健全な体系では、 証明されるものは真なので、Gも真になり、Gの定義から、Gは証明できない。よって、矛盾となって仮定が否定される。次に、Gが反証された。つまりGの否定が証明されたとして、矛盾を導く。健全な公理系ではGの否定は真となる。すると、Gが証明できることになり、健全性からGは真となる。他方、Gの否定も真なので、矛盾が導かれた。よって、Gは反証できない。

【補足説明】ゲーデルの不完全性定理の原論文においては、形式体系に対する仮定は「健全性」より少し弱い「ω無矛盾性」という条件で、体系がω無矛盾であるとは「どの論理式A(𝑥 )についても、𝑥 A(𝑥 )が証明できれば、¬A(n*)が証明されない自然数nがある」ことをいう。ここで、n*は自然数nを形式的に表現する記号列で、例えば 3*は「1+1+1」などとする。そして、ゲーデルの結果を厳密に述べれば、1) 無矛盾な体系では、Gは証明できない。(2ω無矛盾な体系では、¬Gは証明できない。となる。(2)の仮定を「無矛盾」に弱めたのはロッサーの仕事(1936年)である。

<さらに知りたい方へ>
ゲーデルの結果を導くために重要になるのが、「形式体系の中で自然数の和積演算が正しく行える」という条件の分析である。まず、𝑥 s (s 以下のすべての𝑥 について) や y t (t 以下のy が存在して)のような量化子を有界といい、すべての量化子が有界であるような論理式を有界な論理式と呼ぶ。また、有界な論理式 A(𝑥 ) を使って、𝑥 A(𝑥 ) と書けるもの(「A(𝑥 )を満たす𝑥 が存在する」の意)を Σ1論理式と呼ぶ。そうすると、Σ1命題は(自然数の標準構造で)真であれば証明できることが「和積演算が正しく行える」ことから導けて、この性質をΣ1完全という。また、Σ1の否定¬𝑥 A(𝑥 )(≡𝑥 ¬A(𝑥 ))はΠ1といい、Σ1論理式でΠ1論理式とも同値になる(ことが示せる)ものはΔ1と呼ばれる。Δ1命題については、真であることと証明可能であることが同値になり、これがゲーデルの証明の核になる「表現定理」である。この定理がなぜ重要かというと、メタ数学の概念を算術式で表すと多くの場合にΔ1になり、体系外の概念と体系内の形式表現が一致するからだ。ただし、証明可能性はΣ1で、ゲーデル文GΠ1である。

(1)の証明に戻る。Π1Gが証明されたと仮定する。すると、¬G が真になる。¬GΣ1なので、上の説明から証明可能になり、体系が矛盾し、仮定に反する。よって、G は証明できない。

(2)については、上の不完全性定理の証明そのままで大丈夫だ。というのは、使われている健全性はΣ1式¬Gに関するものだけで、それはω無矛盾性の仮定からも導ける。なお、ω無矛盾性とΣ1健全性との関係は、田中一之氏の著書『ゲーデルに挑む』の補遺に説明がある。

最後に、ロッサーによる改良について、簡単に述べておく。ロッサーの議論では P′(𝑥 ) ≡ 「F𝑥 (𝑥 )が証明できれば、それより短い証明でその否定が証明できる」と置き、これに対する自己言及文をロッサー文 R と定義する。つまり、RΠ1文で、R⇔「Rが証明できれば、それより短い証明でその否定が証明できる」である。最初に、Rが証明できたと仮定する。もしRが真だとすると、Rの定義からその否定も証明でき、体系が矛盾するので、Rは偽である。つまり、¬Rは真であり、Σ1文だから証明可能になる。すると、やはり体系が矛盾するため、Rは証明できない。次に、¬Rが証明できたとして、その証明の長さをn とする。 すると、無矛盾な体系で、Rは証明できないから、とくに「Rは長さ n 以下の証明をもたない」ことは真であって、有界論理式で表現できるので、証明可能でもある。したがって、「もしRが証明できれば、(その証明は n より長いから)それより短くその否定が証明できる」が証明できる。この「 」内はRに等しいので、結局Rが証明できることになり、体系が矛盾する。ここで、「もしRが証明できれば」という仮定はナンセンスに思えるかもしれない。しかし、「Rが証明できない」が真であっても、その事実は証明できているわけではないので、証明の中の議論としては、「Rが証明できる」場合もレアケースとして考えられる。言い方を換えると、ある超準モデルにおいては、¬Rの有限の証明とRの無限大(長)の証明が両方存在し得るのである。