ゲーデルの不完全性定理入門

ゲーデルの第2不完全性定理は引用と代入という操作ができる理論ではかならず成り立つ、という話をします。

ゲーデルの第1不完全性定理と第2不完全性定理

不完全性定理には第1不完全性定理と第2不完全性定理があります。雑に言うと

第1不完全性定理：証明も否定もできない命題が存在する

第2不完全性定理：自分自身の無矛盾性は証明できない

ゲーデル自身は自然数の理論について第1不完全性定理が成り立つことを示し、さらにそのことを利用して第2不完全性定理を示しました。

ただ、この2つには大きな違いがあります。第2不完全性定理はそもそも「自分自身の無矛盾性」をその理論が表現できる、ということを前提にしています。この前提が崩れると第1不完全性定理は成り立たない（真な命題はすべて証明できる）のに第2不完全性定理は成り立つ体系があり得ます（具体例は後で紹介します）。そして、「無矛盾性」をそもそもどのように表現するか、というのも簡単ではない問題です（あとでこれも議論します）。

このノートでは第2不完全性定理に絞って話をします。

設定

不完全性定理は理論についてのものです。それをTと書くことにしましょう。

理論は（まあ普通は）言葉で語られますから、Tを表すのに使われる言語Lがあるはずです。では言語とはなんでしょうか。難しい問題ですが、とりあえず言語は文からできていると考えます。さらに、文は「〇〇は△△である」という形をしていると考えます。〇〇を項、△△を述語と呼びます。項をt、述語をPと書いた時、文をPtと書くことにします。また、ある文SやS1、S2があったとき、「S1ならばS2」や「S1かつS2」、「Sではない」も文と考えましょう。

では項とはどんなものでしょうか。ここで項が全体としてなんであるかは限定しないことにしますが、最低次のものは含まれているとします。まず、言語Lのどの文SについてもSを引用符でくくった"S"（に対応するもの）は項とします。また、単なる引用だけではなく、「空欄」つきの引用符も考えます。空欄には文を代入することができます。少しややこしいですね。Pythonぽく書いてみましょう。

format("{}は△△である", "〇〇") ="〇〇は△△である”

もっと複雑な文についてもformatを考えることができます。とくに空欄つきの文を空欄つきの文に代入できると考えます。つまり

format("{}は△△である", "{}は□□である") =""{}は□□である"は△△である”

新しい文がつくれます。もう空欄はないことに注意してください。

次に述語を考えます。述語もいろいろなものがあって良いのですが、ここでは一つだけ、「証明できる」という述語だけを考えます。「Sは証明できる」という文はTがSを証明する、ことを意味すると考えます。

では、理論Tはどんなものでしょうか。まず、普通の論理（ならば、とか、かつ、とか、または、とか等号に関する推論）ができると仮定します。さらに次の4つの条件を仮定します。文章がややこしくなるので「Tが文Sを証明する」をT┝Sと書くことにします。（但書：なにか条件を落としている気がするので、間違いがあればコメント欄でご指摘ください）

条件1：Tは矛盾していない。つまり、「Sである」も「Sでない」も証明できるような文Sは存在しない。

条件2：t1とt2が等しいとき、T┝t1が証明できるならばt2も証明できる

条件3：T┝SならばT┝"S"は証明できる

条件4：T┝"S1"は証明できる、かつT┝"S1ならばS2"が証明できる、ならばT┝”S2"は証明できる

条件5：T┝"”S"は証明できる”ならば""S"は証明できる”は証明できる

なんだかややこしいですね。ひとことでいうと、Tは自分自身が何かを証明したりしなかったりすることに言及できて、その基本的な性質を証明できる、ということになります。

ゲーデル文

つぎに「自分自身は証明できない」という文をつくります。次のような空欄付き引用文をgとします。

"format({}, {})は証明できない"

次の文をGとします。

format(g, g)は証明できない

TはGを証明することができません。もし証明できたとしましょう。条件3からTは

"G"は証明できる

を証明します。さらにこんな計算ができます。

"G" = "format(g, g)は証明できない” = format("format({}, {})は証明できない", g) = format(g, g)

よって、条件2よりTは

format(g, g)は証明できる

を証明します。よって、TはG、つまり「format(g, g)は証明できない」と「format(g, g)は証明できる」の両方を導くので矛盾しています。Tは矛盾していないのでこれはおかしいです。

第2不完全性定理の証明

上の議論をTの中で行います。つまり

1) T┝"G"が証明できたらTは矛盾している

もしTが自分自身の無矛盾性を証明できるなら、ここから

T┝"G"は証明できない

"G" = format(g, g)より

T┝format(g, g)は証明できない

つまりTはGを導きます。これは上の節の結果に反します。1)を導くために

T┝”G"が証明できたら"Gでない”も証明できる

を示します。Gは

T┝”G"は証明できればGでない

という性質を持ちます。条件3より

2) T┝"”G"は証明できればGでない"は証明できる

条件5より

3) T┝"G"が証明できたら""G"が証明できる”も証明できる

が成り立ちます。2)と条件4を組み合わせると

4) T┝”G"が証明できたら”Gでない”は証明できる

これが示すべきことでした。

議論

普通は第2不完全性定理は次のように定式化されます

定理）理論Tがロビンソン算術を含む帰納的で無矛盾な体系とする。このときTは自分自身の無矛盾性を示さない

この定理がこのノートで紹介した不完全性定理の特殊な場合であることはすぐわかります。このノートの「引用」がゲーデル数化のことです。条件2は等式公理が成り立つ（と基本的な計算ができること）を意味しています。条件3-5はLöbの条件です。

このノートのような議論ができることは、第2不完全性定理がTが自然数の理論であることにも帰納的であることにも直接依存していないことを示しています。実際、2階言語の上のω算術でも第2不完全性定理は成り立ちます。一方で、Löbの条件を満たさないような証明可能性概念を考えると帰納的な体系でも自らの無矛盾性を示すことができます。カットフリーなLK2を使った例を与えたことがあります。この例だとLöbの条件の2番目（条件4）が破られています。

まとめ

ゲーデルの第2不完全性定理はその体系が自分自身の文を引用することができ、引用に関するいくつかの性質を示すことから帰結することを示しました。