戻る

ゲーデルの不完全性定理

このノートは、ゲーデルの不完全性定理が何を述べ、どんな考え方で証明されるのかをたどる概説である。数学の基礎をめぐる歴史から入り、具体例を通して証明の仕組みを説明する。厳密な証明の細部は省き、定理が成り立つ条件や、その意味を理解することに重点を置く。

1 自己言及は何を壊すのか

「この文は偽である」。

真なら、書いてあるとおり偽である。偽なら、書いてある内容が外れているのだから真である。どちらにしても落ち着き先がない。嘘つきのパラドックスと呼ばれる古い問題である。

長いあいだ、この種の文は数学の外に置かれていた。数学は数や図形について語るのであって、自分自身について語る文など扱わない。そう考えれば、嘘つき文は日常言語の病理であって、数学の基礎を揺らすものではない。

ところが、近代の数学基礎論はこの境界を危うくした。数、関数、図形をばらばらに扱うのではなく、できるだけ少数の論理的な原理から作り直そうとすると、「ある性質を満たすもの全体」を一つの対象として扱いたくなる。たとえば「偶数である」という性質から偶数全体の集合を作る、という発想である。これは自然に見えるが、あまり自由に許すと、自分自身を巻き込む対象まで作れてしまう。

その危険を突いたのが、ラッセルのパラドックスだった。「自分自身を要素として含まない集合」をすべて集めた集合 RR を考える。RR は RR 自身を含むだろうか。含むなら、RR の定義により含まない。含まないなら、定義により含む。嘘つき文と同じ構造が、集合の言葉で現れた。このパラドックスは、算術を論理だけから基礎づけようとしていたフレーゲの体系を直撃したが、問題はフレーゲの体系だけに限られない。数学の対象を作る原理そのものに、自己言及の入口があった。

ラッセルの応答は、自己言及を文法で禁じることだった。彼は数学者ホワイトヘッドとともに『プリンキピア・マテマティカ』を書き、そこで型という階層を式に課した。集合は自分より下の型のものしか要素にできないと定めれば、「自分自身を要素として含む集合」は、偽である以前に、そもそも正しい式として書けない。危険な文を一つずつ退治するのではなく、危険な文が最初から式にならない文法を作る。

しかし、このパラドックスを書けないようにしただけで、ほかの矛盾も起こらないと保証できるだろうか。許された式と推論を使って、ある主張とその否定が両方とも導かれることはないか。特定のパラドックスを避けるだけでなく、体系全体で矛盾が導かれないことを確かめたい。

ヒルベルトは、数学全体について、この保証を与えようとした。そこで、証明そのものを数学的に調べる対象として扱う。証明の出発点として何を認め、どんな規則で次の式を導いてよいかを明示すれば、証明を、規則に従って式を並べた有限の記号列として扱える。ヒルベルトは、そのように定めた証明のどれからも矛盾は導かれないことを、有限的な記号操作で示そうとした。

この計画の行方を大きく変えたのが、ゲーデルの不完全性定理だった。矛盾を避けて証明の規則を定めても、その規則で証明できることには限界がある。その議論を追う準備として、次節では、短い等式の証明を使って、証明の各行が規則に従っているかを調べる手続きを見ていく。

2 証明は記号列として検査できる

形式体系では、使ってよい記号がまず決められる。次に、その記号列のうち、文法に合っているものだけを式と呼ぶ。たとえば日本語でも「犬が走る」は文だが「走るが犬」は文ではない。同じように、形式体系にも、正しい式とただの記号列の区別がある。

そのうえで、出発点として無条件に認める式を公理と呼ぶ。すでに得た式から新しい式を作る規則を推論規則と呼ぶ。証明とは、各行が公理であるか、それ以前の行から推論規則で得られる式であるような有限列である。ある式を最後の行にもつ証明があれば、その式は定理と呼ばれる。

数論の形式体系の代表例として、ペアノ算術を考える。これは自然数の足し算と掛け算を扱う標準的な公理体系である。00 はゼロ、SS は次の数を表し、0,S0,SS0,…0,S0,SS0,\ldots が 0, 1, 2, … に対応する。∀a\forall a は「すべての aa について」と読む。SaSa は aa の次の数である。ペアノ算術では、足し算や掛け算の振る舞いが、たとえば次のような公理で決められる。

たとえば、二つ目の式は、a+(b+1)a+(b+1) を (a+b)+1(a+b)+1 に戻す規則である。つまり、右側の数を一つずつ減らしていけば、足し算の値を決められる。掛け算の公理も同じ発想で、a⋅(b+1)a\cdot(b+1) を a⋅b+aa\cdot b+a に戻している。

この体系で「1+1=2」を示すには、意味を理解する必要はない。公理

∀a∀b(a+Sb=S(a+b))\forall a\forall b(a+Sb=S(a+b))

の aa に S0S0、bb に 00 を代入すれば、

S0+S0=S(S0+0)S0+S0=S(S0+0)

が得られる。別の公理 ∀a(a+0=a)\forall a(a+0=a) から S0+0=S0S0+0=S0 が得られるので、右辺を書き換えて

S0+S0=SS0S0+S0=SS0

となる。ここで使ったのは、式の形の照合と置換だけである。++ が足し算を意味することを知らなくても、各行が規則どおりかどうかは検査できる。

このように、証明の各行が規則に従っているかどうかは、解釈や直観に頼らず確認できる。形式化によって、証明の検査を機械的な手続きにできるのである。

ただし、機械的に検査できることと、機械的に見つけられることは同じではない。証明を一つ渡されれば、その列が正しい証明かどうかは確かめられる。しかし、ある式について証明がまだ見つかっていないとき、どこかに証明があるのか、それとも存在しないのかは、結論の式だけからは読めない。

3 数について語る言語で、証明をどう扱うか

前節では、私たちが体系を外から見て、記号列が式になっているか、各行が証明の規則に従っているかを調べた。ここで、検査する側が使っている言葉と、検査される式の言語を区別しておこう。

S0+S0=SS0S0+S0=SS0 は、自然数の足し算と等号を使った式である。0=S00=S0 も、自然数の等号についての式である。後者は自然数については偽だが、文法に合っていないわけではない。式として正しく書かれていることと、その内容が真であることは別である。

数論の言語で直接扱う対象は自然数である。足し算や掛け算を使って数どうしの関係を述べられるが、記号列を直接引用して「これは式である」「これは証明である」と述べるための記号は用意されていない。私たちが外から行っている証明の検査を、そのまま数論の式として書けるわけではない。

それでも、記号列を自然数で表せれば、記号列についての問いを数についての問いに変えられるかもしれない。まず必要なのは、式や証明に番号をつけ、その番号からもとの記号列を復元できるようにすることである。

4 数が文の名前になる

各記号に番号を割り振る。たとえば 00 に 6、SS に 7、== に 5、という具合でよい。記号列の各記号の番号を順に c1,c2,…,cnc_1,c_2,\ldots,c_n とし、それを

2c13c25c3⋯pncn2^{c_1}3^{c_2}5^{c_3}\cdots p_n^{c_n}

という一つの自然数に変える。pnp_n は nn 番目の素数である。たとえば S0S0 なら、最初の記号 SS の番号 7 を 2 の指数に、次の記号 00 の番号 6 を 3 の指数に使う。素因数分解は一意なので、この数から指数を読み出せば、もとの記号列を復元できる。式も、式の列である証明も、同じように一つの自然数にできる。

これがゲーデル数化である。

式 φ\varphi に対応する自然数を、その式のゲーデル数と呼ぶ。体系の中でこの番号を使うには、自然数として書き表せばよい。たとえば 3 を SSS0SSS0 と書くように、ある自然数を形式言語の中で表す記号列を数項と呼ぶ。以後、φ\varphi のゲーデル数を表す数項を ⌜φ⌝\ulcorner\varphi\urcorner と書く。文字列を直接引用しなくても、その番号を数として書ける。

ただし、番号をつけることと、その記号列の性質を数論の式で述べることは別の作業である。たとえば、ある数が式の番号だと分かっても、「その式には証明がある」という性質を、足し算や掛け算を使ってどう書くかは、まだ分からない。数と記号列の対応を使って、式の形や証明の規則についての条件を、数についての条件へ翻訳する必要がある。

この翻訳を考えるために、「この記号列は式か」という形の検査と、「この式は定理か」という証明の探索を比べてみよう。対応する自然数についての問いとして見ると、この違いは次の二つの例に重なる。

一つは、調べる範囲が最初から限られている問いである。たとえば 691 が素数かどうかを調べるなら、691\sqrt{691} まで割ってみれば足りる。691 が二つの数の積なら、少なくとも片方は 691\sqrt{691} 以下だからである。そこまで割って約数が見つからなければ、691 は素数だと分かる。

もう一つは、出発点と操作が決まっていて、そこから目標の数に到達できるかを問うものである。証明探索では、公理から出発し、許された推論規則だけで目標の式を導けるかを問う。出発点と許された操作を決め、目標に到達できるかを問う問題は、数に対する操作でも作れる。たとえば次の問題である。出発点は 1、目標は 27。許される操作は二つだけで、数を 2 倍すること、そしていまの数が 3k+13k+1 の形なら kk へ戻ることである。これはコラッツ予想に対応する到達問題で、この規則で 27 へ到達する経路のひとつは、途中で 9232 まで大きくなる。規則が短くても、探索しやすいとは限らない。

ある数が整形式を表すかどうかは、前者の種類の問いである。記号列を復元し、その形を分解していけばよい。ある数が定理を表すかどうかは、後者の種類の問いである。その数が表す式を導く証明の列を探すことになる。見つかれば確認できるが、見つからない間は、存在しないのか、まだ十分に長い証明を調べていないだけなのか分からない。

5 証明可能性は算術で語れる

式 φ\varphi について、「番号 mm の記号列は φ\varphi の証明である」という関係を考える。正確には、mm を復号すると式の列になり、その列が φ\varphi の正しい証明になっている、という関係である。式の側は、先ほどの記法 ⌜φ⌝\ulcorner\varphi\urcorner を使えば番号で指定できる。

この関係は機械的に判定できる。mm を復号し、各行が公理か、前の行から推論規則で得られているかを順に調べればよい。証明の意味を理解する必要はない。必要なのは、有限の記号列の照合である。

ゲーデルの論文の大部分は、この機械的な検査を自然数の性質として書き下す作業に費やされている。現代風に言えば、ソースコードを読んで、括弧の対応や式の形や一行ごとの変形が規則どおりかを調べる検査器を、文字列ではなく自然数の上で動くように作り直すようなものである。

たとえば、ゲーデル数を素因数分解すれば、三番目の素数の指数から三番目の記号番号を読み出せる。すると「三番目の記号が == である」のような構文上の条件は、「その数が 5k5^k でちょうど割り切れ、その指数 kk が == の番号である」のような算術的条件に翻訳できる。この発想を積み重ねて、「この列は式か」「この行は公理の形をしているか」「この行は前の二行から規則で得られるか」といった条件を、足し算、掛け算、割り切れることなどの言葉へ移す。

翻訳の結果、証明の番号と式の番号を受け取る数論の式が得られる。これを Proof\mathrm{Proof} と書くと、Proof(m,⌜φ⌝)\mathrm{Proof}(m,\ulcorner\varphi\urcorner) は「番号 mm の記号列は φ\varphi の証明である」と述べている。

ここから

Prov(⌜φ⌝)≔∃m Proof(m,⌜φ⌝)\mathrm{Prov}(\ulcorner\varphi\urcorner)\coloneqq \exists m\,\mathrm{Proof}(m,\ulcorner\varphi\urcorner)

と定める。これは「φ\varphi には証明がある」、つまり「φ\varphi は証明可能である」という意味になる。mm は証明の番号を動く変数であり、⌜φ⌝\ulcorner\varphi\urcorner は証明したい式の番号を表す数項である。

ここで数論の式へ翻訳したのは、与えられた記号列が証明の規則に従っているかを調べる手続きである。たとえば「1+1=2」の証明を検査するとき、調べているのは、各行が公理や推論規則に従っているかどうかである。この検査では、++ を実際の足し算として解釈して両辺の値を比べる必要はなく、使われた式と規則の照合だけでよい。数論の中に表せたのは、この証明の検査と、検査に通る証明が存在するという性質である。

ここで、文の性質を述べる述語が手に入った。しかもその述語は、体系の外から見れば文について語っているが、体系の中ではあくまで自然数について語っている。

6 代入も算術で語れる

残るのは、文に対する操作である。

自由変数 xx を一つもつ式を考える。自由変数をもつ式とは、まだ値を入れる空欄を含む文の型である。たとえば「xx は偶数である」は、xx に 4 を入れれば「4 は偶数である」という文になり、5 を入れれば「5 は偶数である」という文になる。

ここでは、式の番号を受け取り、代入後の文の番号を返す関数 sub\mathrm{sub} を作る。入力を自然数 nn とし、次の手順で出力を決める。

  1. nn をゲーデル数として復号し、元の式を取り出す。
  2. 数 nn を表す数項を作る。たとえば n=3n=3 なら S(S(S(0)))S(S(S(0))) であり、一般には 00 に SS を nn 回付ければよい。
  3. 取り出した式の自由な xx をすべて、この数項で置き換える。
  4. できた文のゲーデル数を計算し、それを出力 sub(n)\mathrm{sub}(n) とする。

ここでは、自由変数が xx だけの式を扱う。それに当たる式の番号でない入力に対しては、出力を 00 と決めておく。これで、どの自然数を入力しても出力が一つ決まる。

具体例として、⌜x=0⌝\ulcorner x=0\urcorner を入力してみよう。まず復号すると x=0x=0 が得られる。この入力番号を表す数項は、既存の記法で ⌜x=0⌝\ulcorner x=0\urcorner と書ける。これを xx の位置へ入れると、次の文になる。

⌜x=0⌝=0\ulcorner x=0\urcorner=0

ここまででは、まだ出力する番号は得られていない。最後に、この文全体にゲーデル数を付ける。その番号が、関数 sub\mathrm{sub} の返す値である。したがって、この入力に対する値は

sub(⌜x=0⌝)=⌜⌜x=0⌝=0⌝\mathrm{sub}(\ulcorner x=0\urcorner)=\ulcorner\ulcorner x=0\urcorner=0\urcorner

となる。右辺の内側の ⌜x=0⌝\ulcorner x=0\urcorner は、代入した数を表す数項である。外側の括弧は、代入後の文「⌜x=0⌝=0\ulcorner x=0\urcorner=0」全体の番号を表している。括弧の記法は略記であり、実際に番号を付ける対象では、内側の数項を SS と 00 による表記へ展開する。

このように sub(n)\mathrm{sub}(n) は、入力 nn から有限の記号操作と数の計算で求められる。前節で証明の検査を算術で表したのと同様に、この計算も算術で表せる。以下で sub\mathrm{sub} を含む式は、この入力と出力の関係を算術で表した式の略記とする。これを証明可能性の式と組み合わせよう。

まず、自由変数 xx をもつ式

F(x)≔¬Prov(sub(x))F(x)\coloneqq \neg\mathrm{Prov}(\mathrm{sub}(x))

を考える。これは「番号 xx の式に、その同じ数 xx を表す数項を代入してできる式は、証明可能でない」と読むことができる。

F(x)F(x) も一つの式だから、ゲーデル数をもち、その数を表す数項は ⌜F(x)⌝\ulcorner F(x)\urcorner である。そこで、F(x)F(x) の自由変数 xx にこの数項を代入した文を GG と置く。

G≔F(⌜F(x)⌝)G\coloneqq F(\ulcorner F(x)\urcorner)

右辺の FF の定義を展開すると、GG は

¬Prov(sub(⌜F(x)⌝))\neg\mathrm{Prov}(\mathrm{sub}(\ulcorner F(x)\urcorner))

という文である。ここで sub(⌜F(x)⌝)\mathrm{sub}(\ulcorner F(x)\urcorner) は、式 F(x)F(x) にその式自身の番号を表す数項 ⌜F(x)⌝\ulcorner F(x)\urcorner を代入してできる文の番号を表す。その文が GG なので、

sub(⌜F(x)⌝)=⌜G⌝\mathrm{sub}(\ulcorner F(x)\urcorner)=\ulcorner G\urcorner

となる。

したがって GG は

¬Prov(⌜G⌝)\neg\mathrm{Prov}(\ulcorner G\urcorner)

と同じ内容をもつ。つまり GG は「GG は証明可能でない」と述べている。

このように、自分の番号を自分に代入して固定点を作る方法を対角化という。自己言及する文の有名な例に、「この文は偽である」という嘘つき文がある。真だとすれば内容どおり偽になり、偽だとすれば内容が外れるので真になってしまう。ここで構成した GG は、この嘘つき文とは異なる。「私は偽である」ではなく、「私は証明できない」である。真理は体系内に入らない。証明可能性は入る。その差が、パラドックスではなく定理を生む。

7 真であるのに証明できない

TT を、初等的な算術を含み、公理が機械的に列挙できる形式体系とする。さらに、ひとまず TT は無矛盾だと仮定する。無矛盾とは、ある文とその否定の両方を証明することはない、ということである。

さきほど作った GG は、「GG は TT で証明できない」と述べている。

ここで一つだけ、前節までの翻訳作業の効き目を使う。具体的な数 m,nm,n について「mm は nn の証明である」と機械的に確認できるなら、十分な算術を含む TT は、その個別事例 Proof(m,n)\mathrm{Proof}(m,n) を証明できる。これは「証明である」という検査が数論の中に写し取られている、ということの実質である。

もし GG が TT で証明できたとする。その証明にはゲーデル数 mm がある。すると、mm は ⌜G⌝\ulcorner G\urcorner の証明であるという事実は機械的に確認できるので、TT は Proof(m,⌜G⌝)\mathrm{Proof}(m,\ulcorner G\urcorner) を証明できる。したがって TT は Prov(⌜G⌝)\mathrm{Prov}(\ulcorner G\urcorner) も証明できる。

一方、GG 自身は ¬Prov(⌜G⌝)\neg\mathrm{Prov}(\ulcorner G\urcorner) である。GG が証明できるなら、TT は Prov(⌜G⌝)\mathrm{Prov}(\ulcorner G\urcorner) と ¬Prov(⌜G⌝)\neg\mathrm{Prov}(\ulcorner G\urcorner) の両方を証明することになる。これは無矛盾性に反する。だから GG は証明できない。

すると、GG が述べていたことは実際に成り立っている。GG は「私は証明できない」と述べており、いま外からの推論で、確かに証明できないことが分かった。標準的な自然数の世界で見れば、GG は真である。

ただし、この「真」は体系の内部で得られた称号ではない。外から TT の無矛盾性を仮定して判断している。TT 自身が「GG は真である」と証明したわけではない。むしろ、無矛盾なら TT は GG を証明できない。

ここで真理と証明可能性が分かれる。証明可能なら真であってほしい、という健全性の要求は自然である。しかしその逆、真なら証明可能である、は成り立たない。少なくとも、十分な算術を含み、機械的に扱える無矛盾な体系については、真でありながらその体系では証明できない文が作れてしまう。

厳密には、ゲーデルの原証明で GG の否定も証明できないと言うには、無矛盾性より少し強い ω\omega無矛盾性が使われる。これは、各具体的な数については「違う」と言えるのに、「どれかの数が当てはまる」とも証明してしまうようなずれを許さない、という条件である。後にロッサーが文の作り方を改良し、通常の無矛盾性だけで、証明も反証もできない文を得た。現在「第一不完全性定理」として語られる内容は、ふつうこのロッサー改良後の形を含んでいる。

8 なぜ「私は偽である」ではないのか

ここまで見ると、こう疑いたくなる。証明可能性ではなく、真理そのものを使って「私は偽である」を作れば、嘘つき文がそのまま数論の中に戻ってくるのではないか。

その疑いは正しい方向を向いている。そして、だからこそ真理は数論の中に入らない。

仮に、自然数 nn について「nn の表す文は真である」と述べる数論の式 True(n)\mathrm{True}(n) があるとする。すると、対角化の同じ手順で「私は真でない」と述べる文を作れる。これは嘘つき文そのものであり、真なら真でなく、真でないなら真になる。体系は破綻する。

したがって、そのような真理述語は体系内には存在しない。厳密な定理としては、これはタルスキの定理である。十分な算術を表せる言語では、その言語の文全体についての真理述語を、同じ言語の中で定義できない。

ゲーデルが選んだのが「偽である」ではなく「証明できない」である理由は、ここにある。真理は内部化できない。証明可能性は内部化できる。証明とは有限の記号列が規則に従っているかどうかであり、そこには機械的な検査があるからである。

不完全性定理は、嘘つき文を乱暴に数学へ持ち込んだ結果ではない。嘘つき文が使っていた自己言及の形から、内部化できない真理を取り除き、内部化できる証明可能性に置き換えた結果である。その置き換えが、矛盾ではなく決定不能性を生む。

9 何が壊れ、何が壊れていないのか

不完全性定理が壊したのは、数学の正しさではない。既存の証明が無効になったわけでも、数学の中に矛盾が見つかったわけでもない。証明全体は、むしろ体系が無矛盾であるという仮定の上に立っている。

壊れたのは、形式体系に期待されていた一つの理想である。すなわち、十分に強い一つの体系を作れば、そこで真な算術の文をすべて証明できるという期待である。

証明不能な文が一つ見つかっただけなら、その文を公理に加えればよいと思える。実際、GG を公理に加えれば、GG はその新しい体系で証明できる。しかし、その追加で無矛盾性が保たれたとしても、新しい体系が機械的に公理を列挙でき、算術を含んでいるかぎり、同じ構成をもう一度受ける。新しい体系についての新しいゲーデル文が生まれる。

では、真な算術の文をすべて公理にしてしまえばよいか。そうすれば完全にはなる。しかし、どの文が公理かを機械的に判定できない。証明の検査が有限の記号操作で済む、という形式体系の利点を失う。形式性を保ったまま、算術的真理を一つの体系に全部回収することはできない。

第二不完全性定理は、この失敗をさらに鋭くする。十分な算術を含む無矛盾な体系 TT は、自分自身の無矛盾性 Con(T)\mathrm{Con}(T) を証明できない。ここで Con(T)\mathrm{Con}(T) とは、「矛盾、たとえば 0=10=1 を導く証明番号は存在しない」という主張を TT の言語で書いたものである。

理由の輪郭は第一定理と同じである。「TT が無矛盾ならば GG は証明できない」という外からの推論は、かなりの部分が TT の内部で形式化できる。そのため TT は「Con(T)\mathrm{Con}(T) ならば GG」を証明できる。もし TT が Con(T)\mathrm{Con}(T) も証明できるなら、TT の内部で「Con(T)\mathrm{Con}(T) ならば GG」と「Con(T)\mathrm{Con}(T)」の両方がそろうので、推論規則により GG も証明できる。これは第一定理に反する。

ヒルベルトの計画にとって、ここが致命的だった。数学を形式化し、その無矛盾性を同じ水準かそれ以下の疑いない手段で保証する、という構想は成り立たない。ある体系の信頼性を示すには、結局その体系の外側に立つ必要がある。外側の体系を使えば証明できることはある。実際、ゲンツェンは超限帰納法、つまり自然数を越えた順序構造に沿う帰納法を用いて、PA、すなわちペアノ算術の無矛盾性を証明した。しかしそれは、より強い原理を信用するなら PA を信用できる、という形の保証であって、無前提の最終保証ではない。

10 どこまで適用できる定理なのか

不完全性定理は、何にでも当てはまる格言ではない。必要なのは大きく三つである。

第一に、体系が無矛盾であること。矛盾した体系はあらゆる文を証明できるので、不完全性を論じる対象にならない。

第二に、公理が機械的に列挙できること。証明かどうかを有限の手続きで検査できるからこそ、証明可能性を算術化できる。

第三に、十分な算術を含むこと。記号列や証明を数に符号化し、それを復元し、代入を表すだけの離散的な力が必要である。

この条件を満たすなら、体系が PA、つまり自然数の足し算・掛け算を扱う標準的体系でも、ZFC、つまり現代集合論の標準的公理系でも、同じ現象が起きる。逆に、条件を欠く体系には定理はそのまま適用されない。自然数の足し算だけを扱うプレスバーガー算術は完全で決定可能である。実数の足し算・掛け算・大小関係を一階論理で扱う理論も、タルスキにより完全で決定可能である。

自然数の理論は不完全なのに、実数の理論は完全でありうる。これは表現力の大小だけで決まる話ではない。不完全性が現れる土台は、有限の記号列を一つの対象に畳み込み、また取り出せることにある。自然数の足し算と掛け算は、その離散的な符号化を支える。実数の一階理論では、自然数全体を内部で定義することすらできず、同じ仕掛けが動かない。

よくある誤読も、ここから整理できる。

人間は GG が真だと分かるが機械には分からない、という議論は慎重に扱う必要がある。我々が GG を真だと判断したのは、TT が無矛盾であるという前提を外から置いたからである。その前提を人間が常に確実に見抜ける、という根拠はない。

物理学や法体系や人間の心が「不完全」だという主張も、定理そのものからは出ない。対象が、機械的に列挙できる公理をもつ形式体系であり、十分な算術を含んでいるのでなければ、適用条件を満たしていない。類比として語ることはできるが、それは数学的帰結ではない。

一方で、不完全性は論理学者が作った珍品だけに閉じているわけでもない。たとえば、ヒルベルトの第10問題の周辺では、整数係数の方程式に整数解がないことを特定の体系では証明できない例が現れる。組合せ論の命題であるパリス・ハリントンの定理、単純な規則で進む数列について述べるグッドスタインの定理など、ふつうの数論や組合せ論に見える場所にも、特定の体系から独立な命題が現れる。

さらに、数に簡単な規則を繰り返し適用する問題にも、同じ深さが現れる。§4では、1から出発し、2倍する操作などを使って27へ到達できるかを問う、コラッツ予想に関連する問題を見た。公理から目標の式を導く証明探索と、出発点から目標の数へ進む経路の探索を重ねた例である。コラッツ予想そのものが独立命題かどうかは分かっていない。ただし、この種の反復問題を一般化すると、計算機の動作を埋め込めるものがあり、与えられた問題の答えを一律に判定する手続きが存在しないという、停止問題と同じ意味での決定不能性が現れる。見た目の素朴さは、形式体系にとっての扱いやすさを保証しない。

ゲーデル文は人工的に見えるが、そこで露出した構造は特殊な人工例に限られない。

ゲーデルの定理では、証明を機械的に検査できることが、その体系の限界を示す手がかりにもなる。記号列を数で表し、証明の検査を数論の式へ翻訳し、さらに自分の番号を代入する。この手順を通じて、自然数についての文が、自分自身の証明可能性についても述べるようになる。そこから、その体系では証明できない文が得られる。

出典と文献

本稿は、証明を完全に再構成したものではなく、いくつかの標準的な解説をもとにした概説である。全体像をつかむ入口としては、ダグラス・ホフスタッターの講演 Limits of Logic: The Gödel Legacy(2016) も参考になる。

一次文献としては、K. Gödel, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I”, Monatshefte für Mathematik und Physik 38 (1931), 173-198 が原論文である。英訳で読むなら、Jean van Heijenoort 編, From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931 (Harvard University Press, 1967) 所収の訳が参照しやすい。ロッサー改良については J. Barkley Rosser, “Extensions of some theorems of Gödel and Church”, Journal of Symbolic Logic 1 (1936), 87-91。

本文の技術的骨格、すなわちゲーデル数化、表現可能性、対角化補題、第一・第二不完全性定理の標準的な整理については、Peter Smith, An Introduction to Gödel’s Theorems (Cambridge University Press) を主な確認先にした。オンラインで全体像を確認するには、Panu Raatikainen, “Gödel’s Incompleteness Theorems”, Stanford Encyclopedia of Philosophy がよい。形式体系、無矛盾性、第一・第二定理、ロッサー改良、タルスキの定理、ヒルベルトの第10問題、具体的な独立命題までを一通り整理している。

フレーゲ、ラッセル、ホワイトヘッド、ヒルベルト・プログラムという歴史的背景については、Jean van Heijenoort 編の上掲書、および Richard Zach, “Hilbert’s Program”, Stanford Encyclopedia of Philosophy を参照した。『プリンキピア・マテマティカ』については A. N. Whitehead and B. Russell, Principia Mathematica (1910-1913) が原典である。

真理述語が同じ言語内で定義できないという §8 の説明は、A. Tarski, “Der Wahrheitsbegriff in den formalisierten Sprachen”, Studia Philosophica 1 (1936) に由来する結果を、ゲーデルの構成との関係だけに絞って述べたものである。日本語で概略を追うなら、フランセーン『ゲーデルの定理: 利用と誤用の不完全ガイド』(みすず書房) が、定理の誤用も含めて読みやすい。

§9 の第二不完全性定理とゲンツェンの無矛盾性証明については、G. Gentzen, “Die Widerspruchsfreiheit der reinen Zahlentheorie”, Mathematische Annalen 112 (1936), 493-565 を原典とする。本文では、証明論上の細部、たとえば導出可能性条件や ε0\varepsilon_0 までの超限帰納法の正確な位置づけは省略している。

§10 の適用範囲について、プレスバーガー算術の完全性・決定可能性は M. Presburger, “Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen…” (1929) による。実閉体、つまり実数の一階理論の完全性・決定可能性は Tarski の量化消去の結果である。ヒルベルトの第10問題については、M. Davis, H. Putnam, J. Robinson, and Y. Matiyasevich による MRDP 定理の系として理解される。

自然な数学的命題の独立性については、Paris-Harrington の有限ラムゼー型命題、Kirby-Paris の Goodstein 定理を背景にしている。コラッツ予想そのものが独立命題だとは本文では主張していない。一般化されたコラッツ型問題に決定不能な例があるという点は、J. H. Conway の 1972 年の結果、および Jeffrey C. Lagarias, “The 3x+1 Problem: An Overview” を参照した。

入門としては、ナーゲル&ニューマン『ゲーデルは何を証明したか』、ホフスタッター『ゲーデル、エッシャー、バッハ』、フランセーン『ゲーデルの定理』が読みやすい。ただし本稿の数式部分を検証するには、入門書だけでなく Smith や Stanford Encyclopedia の該当節を併読するのが安全である。