不完全性定理のすごく簡単な説明

【まえがき】

　ここでは、ゲーデルの不完全性定理の証明を専門書で読んでみたけど分かった気がしない人向けに、すごく簡単な説明を試みます。そういう私も、実は不完全性定理をよく理解しているわけではありません。しかし、とある入門書を参考に、以下で紹介する説明を考えて一応納得できました。そこで、未来の自分が忘れてしまわないように書き留めておくことにしました。

　とは言うものの、専門書で紹介されているような一般的応用の効く形で説明するのは難しいので、一階述語論理による健全な自然数論の不完全性定理に的を絞ります。あまり汎用的すぎると抽象度が高くなって難解になります。そういう場合、具体的に対象を絞った方がわかりやすくなると思うからです。その後、いろいろな話題を取り上げます。

　そんなことより、簡潔に結論だけ書いてよという人もいるかもしれないので、とりあえず不完全性定理とは何なのかを説明しておきます。不完全性定理には第一不完全性定理と第二不完全性定理があります。

　第一不完全性定理とは、ある条件を満たす自然数論は、どんなに工夫してもその中に証明も反証もできない論理式が存在するというものです。ある条件とは、感覚的に説明すると「コンピュータで扱えて矛盾がない」と思えば大体合ってます。もし、全ての論理式が証明あるいは反証できるなら完全であると言います。つまり、完全ではないから不完全性定理なのです。

　反証と言う言葉を聞き慣れないという人に説明すると、証明とは正しさの根拠を示すことで、反証とは間違いの根拠を示すことです。そして、論理式とは真か偽かを問える命題を数式に翻訳したものです。

簡単な数式を用いた第一不完全性定理の証明はをご覧ください。互換性という性質を使った非常に簡単な証明を行います。専門書等で、何やらややこしいロッサーの定理につまずいた人は是非読んでみてください。文章による概要を読みたい人は、このまま読み進めてください。

　また、第二不完全性定理とは、第一不完全性定理の条件に加えて、数学的帰納法が扱える自然数論では、論理的な飛躍を避け、証明できるという行為を人間に計算可能な形で定義すると、自分自身が無矛盾であることは証明できないというものです。つまり、第一不完全性定理の証明できない論理式の例の１つが、自分自身の無矛盾性を表す論理式ということです。

簡単な数式を用いた第二不完全性定理の証明はをご覧ください。一般の専門書とは異なる直観的な方法で証明します。文章による概要を読みたい人は、このまま読み進めてください。

　上記の不完全性定理の説明では言葉を慎重に選んでいます。一方、インターネット上には、権威ある大学のサイトでも不完全性定理を雑に説明しているページがあります。そういうページを読んだ人が、「神は存在しない」のような極端な結論に至るケースはよくあります。無矛盾かつ完全な理論が存在しないのだから神も存在しないという理屈のようです。しかし、不完全性定理は何が何でも完全なものは存在しないという主張ではありません。実際には不完全性定理があってもなお無矛盾かつ完全な理論は存在します。雑な議論で曲解すれば、これをもって神が存在すると主張することも可能です。つまり、どちらにせよ雑な説明を安易に鵜呑みにしてはいけません。前提条件や適用範囲をきちんと確認しましょう。

　結論は説明したので、以下では、それぞれ第一不完全性定理と第二不完全性定理の概要ついて説明します。不完全性定理の数学的内容のことはともかく、数学に与えた歴史的意味について知りたいという人は、一足先にをご覧ください。

【第一不完全性定理の概要】

　ここでは、第一不完全性定理の概要を体験するためのクイズをやってみましょう。クイズを解くためには、次のルールを使って良いとします。

ルール：証明できる命題は正しい。

　何だか当たり前のことのようですが、意外に重要なルールなので憶えておいてくださいね。このルールのことを健全性と呼ぶことにします。

　さらに次のような命題に名前を付けて G と呼ぶことにします。 G の中で G 自身に言及していることに注意してください。

命題 G：G は証明できない。

　準備完了しました。いよいよクイズです。命題 G は証明できるでしょうか？試しに G は証明できると仮定します。すると健全性により証明できる命題は正しいので、「G は証明できない」ことが正しいということになります。これは G は証明できることと矛盾しますので、背理法により、 G は証明できないこととなります。

　次のクイズです。命題 G は反証できるでしょうか？反証できるとは、その命題の否定が証明できることです。したがって、G が反証できると仮定すると、

命題 G の否定：G は証明できる。

　が証明できることになります。つまり、

「G は証明できる」が証明できる。

　ということになります。すると健全性により「G は証明できる」ことが正しくなります。しかし既に示したように、G は証明できるとすると矛盾が導かれます。結局、G は反証できるとしても矛盾が導かれるということです。よって背理法により、G を反証することはできません。

　以上のことにより、健全性を認めると、命題 G は証明も反証もできない命題ということになります。このような命題をゲーデル文と言います。あれ？でも今「G は証明できない」ことを証明したよね？と思った人、あなたは鋭い！その通り。この一見矛盾した状況を矛盾なく説明するには、日常言語の曖昧さでは無理です。興味のある人は、是非ともこのページの本文を読んでみてくださいね。矛盾なく説明するためのカラクリもちゃんと書いてあります。

　このクイズでは健全性が重要な役割を果たしましたが、数学を構築する基礎として、健全性が妥当な要求であることはたぶん納得していただけるでしょう。どうでしょう。第一不完全性定理の概要を体験していただけたでしょうか？実際の不完全性定理の数学的証明は、命題 G が自然数論の言葉で書き記すことができることを示すことで行います。

　第一不完全性定理を別の表現で言い換えると、自然数論には、全ての真理を書き出す有限な手続きは存在しないというものになります。あるいは同じことですが、この形式を満たせば真理であるというような有限な一般形で、全ての真理を覆いつくすことはできないということです。有限なという条件は極めて重要ですから憶えておいてくださいね。つまり、全ての真理を手に入れるためには必ず無限が必要になるということです。

【第二不完全性定理の概要】

　続いて、第二不完全性定理の概要を簡単に証明してみましょう。まず、対象となる理論は健全であり第一不完全性定理は成立するとします。次に、無矛盾性を証明するためには何を示したらよいか説明します。対象となる理論が矛盾していると、その理論の全ての命題が証明可能になります。つまり、矛盾を許せば、どんなに筋違いな主張も通ってしまうということです。よって、無矛盾ということは証明できない命題が存在するということです。

　一方、ゲーデル文 G は「G は証明できない」という意味の命題でした。したがって、G が正しければ証明できない命題が存在することになるので、その理論は無矛盾であることになります。つまり、「G は証明できない \(\Rightarrow\) 無矛盾」です。ここで、 \(\Sigma_1\)完全性という性質が成り立つと仮定すると、無矛盾ならば「G は証明できない」ことも示せます。つまり、「無矛盾 \(\Rightarrow\) G は証明できない」です。よって二つを合わせると、「G は証明できない \(\Leftrightarrow\) 無矛盾」であり、「G は証明できない」と「無矛盾であること」は論理的に同値です。

　ただし、「証明できない」という述語に論理的な飛躍があると、形式的な同値性が成り立つとは限らないので、ここでは論理的な飛躍はないという条件で考えることとします。例えば、無矛盾かどうか分からないのに無矛盾と見なしてしまうような飛躍のある述語（ロッサーの証明述語）を使うと、形式的な同値性は成り立つとは限りません。ここで、形式的に同値とは、証明できるかできないかで同値であることを指します。また、論理的に同値とは、正しいか正しくないかで同値であることを指します。

　また、G は「G は証明できない」なので、G の中身を展開してやると、「「G は証明できない」は証明できない」になります。「G は証明できない」は「無矛盾であること」と同値なので、これは、「「無矛盾であること」は証明できない」という意味になります。ところで、第一不完全性定理は成立しますから、その理論が健全なら「G は証明できない」は正しく、よって、それと同値である「「無矛盾であること」は証明できない」も正しいことになります。以上により、その理論が健全ならその無矛盾性は証明できないことが示されました。これが、第二不完全性定理の証明の概要です。ただし、ここでの「証明できる」という述語は\(\Sigma_1\)完全性を満たすとします。

　\(\Sigma_1\)完全性という仰々しい名前が付いていますが、 \(\Sigma_1\)完全性とは、

その命題が証明できるなら、証明できることも証明できる。

　という健全性と同様に割と当たり前そうな性質です。しかし案外難しく、「証明できる」という述語を論理的な飛躍を避けて適切に定義しないと成り立つとは限りません。そして、適切に定義しないと第二不完全性定理も成り立ちません。例えば、論理的な飛躍のある証明述語であるロッサーの証明述語を用いて定義したりすると成り立ちません。

　\(\Sigma_1\)完全性と健全性の両方が成り立つと、「「G は証明できない」は証明できない」と入れ子にしたときに、「証明できない」の意味が変わらないことが保証できます。一方、通常の第二不完全性定理では、健全性の代わりに可導性条件という面倒な条件を仮定します。

　締めくくりに、\(\Sigma_1\)完全性を仮定すると、その理論が無矛盾ならば「G は証明できない」ことを示しましょう。まず、G の否定を考えて「G は証明できる」が正しいとします。すると、\(\Sigma_1\)完全性より、「「G は証明できる」は証明できる」となります。「G は証明できる」は G の否定だったので、「G の否定は証明できる」となります。つまり、G も証明できるし G の否定も証明できるとなってその理論が矛盾します。まとめると、G が証明できるならばその理論は矛盾します。よって対偶を考えると、その理論が無矛盾ならば G は証明できないことになります。

　ところで、第二不完全性定理を根拠として、決して自分の無矛盾性は証明できないという言説をよく目にします。しかし、第二不完全性定理で言えるのは、「証明できる」という述語が\(\Sigma_1\)完全性の対象となるのなら無矛盾性は証明できないということです。 \(\Sigma_1\)という制限は、要するに人間に計算可能という制限です。人間の能力を超える計算能力を仮定すれば、必ずしも不完全性定理は成り立ちません。実際、\(\Sigma_2\)の計算能力を使えるなら必ずしも不完全性定理は成り立ちません。したがって、第二不完全性定理を根拠として、決して自分の無矛盾性を証明できないと言うのは論理的な飛躍です。有限な方法である再帰的に公理化可能な理論では証明できないとしか言えません。ただ、そのような完全な自然数論は風変わりな超準モデルしかモデルを持たず、控えめに言っても自然な理論とは言い難いものになります。

　ちなみに、概要ではなく比較的簡単な数式による第二不完全性定理の証明を知りたいという人は、を参照してみてください。自分で言うのもなんですが、通常の専門書とは異なる、なかなか画期的な証明ではないかと思っているので、これまで他の証明にはイマイチ納得できなかったという人におススメです。ただし、使っている記号の意味等についてはこの文書の前半を参照してください。

【宣伝】

　ひと段落したところで、私が執筆している別のページの宣伝を少々。一般の人々の意見が真っ二つに割れる定番の数学ネタとして、 0.999... < 1 は正しいかどうかを考察したページもあります。たぶん、他の Web サイトでは見かけない説明を書いていますので、この手のネタに興味のある人はをご覧ください。0.999... = 1 で間違いないと信じて疑わない人は、その常識がくつがえされるカモしれませんよ。

　さて、インターネット上には、嘘つきのパラドクスなどを用いた日常言語による不完全性定理の解説が多数あります。確かにそれでも分かった気になれるかもしれませんが、私は何だか誤魔化されているような気がして、今一つ数学した気分になれません。かと言って、バリバリに専門的な説明を展開されてもチンプンカンプンです。

　日常言語で誤魔化されたくはないけれど、専門的な説明も勘弁。そんなニッチな要望に応えるために、このページは書かれました。まあ、そのニッチは主に私なんですけどね。私以外でも、不完全性定理にそのような思いを抱える人がいるなら、このページを是非参考にしてみてください。

　本ページの本文では数式をたくさん使います。数式は直観の通用しない問題を考えるときに強力な武器になってくれますが、問題の全体構造をとらえるような場合には文章による説明が適しています。まず、不完全性定理の全体構造を理解したいという人は、を読んでみてください。第一・第二不完全性定理の理解のかなめとなるアイディアが簡潔に解説されています。その他の話題も、面白そうなものを盛り込んであります。例えば、神様と不完全性定理の関係が気になる人も必見です。不完全性定理とAI(人工知能)との関係などについても解説しています。

【余談】

　日常言語で誤魔化されたくないとか書いておきながら、その後、正直者のパラドクスを用いた、日常言語による不完全性定理の超簡単な証明を思いついてしまいました。第一不完全性定理のみならず第二不完全性定理までズドンと証明してしまいます。証明した本人ですらマジか？と思っていますが、だまされたー！と全力で後悔する覚悟のある方はをご覧ください。

　順番に読むのが面倒くさいという方へ。このページのコンテンツ一覧はボタンから確認できます。

【不完全性定理に至る歴史】

　まず簡単に、不完全性定理がどのような経緯で登場したのか触れておきます。不完全性定理登場前夜の19世紀に、それまでの数学からそれ以後の数学へと、その性格を一変させる大発明がカントールさんによってなされました。集合論と呼ばれる数学分野の登場です。

　私は小学生のころに集合を習いましたが、何のためにこんなことをするのか理解できませんでした。いや、問題を解くことはできましたけどね。しかし、実のところ集合論はあらゆる数学の基礎であり、集合という概念のみで現代数学の全ての概念を説明できる画期的な理論だったのです。集合を使ってありとあらゆる数学上の構造を作り出し説明できる。数学者の喜びは大きなものでしたと、竹内外史さんの著書「集合とはなにか」に書かれています。このことを聖書になぞらえてカントールの楽園と呼ぶそうです。

　ところが、しばらくして集合論におかしなことが見つかり始めます。例えば、全ての集合の集合 S を考えると、 S も集合なので S 自身が S の要素になります。つまり自分自身を含んでいます。このような集合があちこちで矛盾を生じ始めたのです。なら、自分自身を含まない集合だけ考えれば良いのではと思うかもしれません。しかし、自分自身を含まない集合の集合 R を考えると、 R は自分自身を含むとしても含まないとしても矛盾してしまうのです。これをラッセルのパラドクスと言います。

　集合論で数学の全てが説明できますから、集合論の矛盾はそのまま数学の矛盾と考えられました。そう、数学は深刻な危機に陥ってしまったのです。数学者たちはカントールの楽園から出ていかねばならなくなりました。まさしく失楽園というわけです。

　この危機的状況を打開するために、ヒルベルトさんがある計画を提案します。曖昧だった集合論の公理系を整備して、形式的体系と呼ばれる体系を構築し、以下の２つの目標を達成しようとしたのです。

全ての命題を証明あるいは反証できると証明しよう。(完全性)
どれだけ推論しても決して矛盾が導かれないと証明しよう。(無矛盾性)

　これをヒルベルト・プログラムと言います。

　当時のトップランナーの数学者たちが数学の危機を救おうと、ヒルベルト・プログラムに取り組みました。あるいはヒルベルト・プログラムとは別の方法で矛盾の克服を目指しました。そしてその時、ゲーデルさんが不完全性定理を証明してしまったのです。つまり、ある条件を満たす形式的体系は不完全であり無矛盾性は証明できないと。ヒルベルト・プログラムは大きな痛手を負ってしまいました。

【注】念のため書いておくと、「証明できない」とは「正しくない」を意味しませんので注意してください。証明できなくとも正しいことはあります。なので、数学が矛盾していると証明されたわけではありません。

　その後、数学者たちは、非形式的な有限の立場やその拡張で、数学の無矛盾性の証明にチャレンジしていくことになります。そして現在、集合論の矛盾の原因などが理解されるようになり、矛盾を回避する公理系なども整備されたことにより、数学の危機はあまり心配されることはなくなったそうです。

【証明の概略】

　さて、これから不完全性定理の証明を始めますが、証明の概略を示しておきます。不完全性を証明する対象は自然数論とし、ペアノ算術を含み数学的帰納法が使えるものとします。ペアノ算術とは我々が普段使っている普通の自然数論の名前です。ペアノ算術を含むとは、ペアノ算術を拡張した自然数論も対象だということです。以下の手順で自然数論の不完全性を証明します。

【大前提】対象とする自然数論は無矛盾(健全)でなければならない。
まず、全ての１変数論理式の真偽を判定できる万能論理式の概念を定義する。
万能論理式の概念は矛盾することを示す。
矛盾の原因は万能論理式の構成要素である真理関数 \(t(z)\) にあることを示す。
矛盾を回避するために自然数論の中には真理関数は存在しないと考える。
次に、論理式の証明可能性を判定する実在して計算可能な証明関数 \(p(z)\) を定義する。
証明関数を使って完全性の概念を定義する。
自然数論が完全なら \(t(z)=p(z)\) であることを示す。
自然数論が完全なら真理関数が存在することになって矛盾する(手順4参照)。
矛盾を回避するために完全性をあきらめる。
完全性をあきらめたので自然数論は不完全である。

　上記で「無矛盾(健全)」と書いてあるのは、無矛盾性より強い健全性を仮定しているということです。健全なら無矛盾ですが、無矛盾なら健全とは限りません。無矛盾という仮定では、後の説明が複雑になってしまいます。説明を簡単にするため、より強い健全性を仮定しています。ちなにみ健全であるとは、証明できる命題は真であるということです。当たり前すぎてかえって意味がつかみにくいかもしれませんが、後で説明するので今はスルーしてください。

【万能論理式】

　それでは本題に入りましょう。ここからは、難しそうな専門用語がたくさん出てきますが、できるだけ後から説明するようにしていますので、がまんして読み進めてみてください。

　まずはじめに、自然数論に関する全ての１変数論理式に番号を振ります。例えば、論理式番号が \(1\) 番の論理式は \(x \gt 0\)、論理式番号が \(2\) 番の論理式は \(x + 1 = 2\) という風に番号を振ります。実際の番号の振り方は対応表の作り方によって変わるので、ここではあくまで一例と思ってください。後にリシャールのパラドクスという逆説を使って自然数論の不完全性を証明する際に、この論理式番号が必要になります。

　ゲーデルさんがゲーデル数という概念を使って、任意の記号列が文法的に正しい論理式かどうかを判定する原始帰納的述語を作ったので、１変数論理式に番号を振ることが可能です。

　いろいろ専門用語が出てきたので１つ１つ説明しましょう。まず、ゲーデル数とは、論理式や関数などあらゆる記号列をコード化したものです。 Shift_JIS, UTF-8 などの文字コードを想像してもらえば分かりやすいと思います。論理式や関数などの記号列も、文字コードで見れば極めて大きな１つの自然数と見なせます。それがゲーデル数です。自然数論では自然数やその関数しか扱えませんので、自然数論の中で記号列を操作して証明を行うためには、記号列をこのゲーデル数に置き換えて考える必要があります。ちょっとだけ注意点ですが、ゲーデル数と論理式番号は別物ですよ。論理式番号は１変数論理式のみに振られた番号です。ゲーデル数はあらゆる記号列に振られた番号です。

　次に、原始帰納的とは、計算に必要なステップ数の最大値を、あらかじめ有限な数値として見積もることができることを言います。つまり、必ず予定時間内に計算結果を確認できるということです。無限ループに陥って、計算が停止しないというようなことはありません。計算が必ず停止するというこの性質は、不完全性と密接な関係にあるので気に留めておいてください。

　また、述語とは、\(x + y \gt 3\) のような論理式で表され、変数 \(x\) や \(y\) に具体的数を代入すると真か偽かが判定できる式のことです。変数の数は１つ以上であればいくつでもかまいません。具体的数にゲーデル数を指定すると、ゲーデル数に対応した記号列に対して何かの性質を判定できることになります。

　さて、話を論理式番号に戻しましょう。１変数論理式に番号を振る仕組みは以下のようなものです。まず、ゲーデル数を \(0\) から始めて \(0,1,2,3,\ldots\) とカウントアップします。次にそれを、文法的に正しい１変数論理式のゲーデル数かどうかを判定する述語で判定します。何が文法的に正しいかは、自然数論の言語から決まります。判定に合格したゲーデル数を集めることで、全ての文法的に正しい１変数論理式のゲーデル数が得られます。最後に、得られたゲーデル数を大きさ順に並べれば、全ての１変数論理式に番号が振れます。判定に合格しない多くのゲーデル数は、１変数論理式でないか文法的におかしい無意味な記号列のゲーデル数です。

　コンピュータのプログラムを書いた経験のある人なら、これはコンパイラと思えば分かりやすいと思います。つまり、書いたソースコードが文法的に正しい１変数論理式かコンパイルして確かめるわけです。実行結果は実行してみないと分かりませんが、文法的に正しいかチェックするだけなら原始帰納的にできると思ってください。

　細かいことなので聞き流してかまいませんが、原始帰納的に番号が振れることを保証するためには、ここで考えている自然数論が再帰的に公理化可能である必要があります。なので、以下の議論で扱う自然数論は再帰的に公理化可能であるとします。こんな条件が必要なのだということだけ憶えておいてください。

　とりあえず説明すると、再帰的に公理化可能とは、大雑把に言って、その自然数論がコンピュータで扱えるということです。つまり、必ず有限な計算に帰着できるということです。自然数論のような理論は、公理と呼ばれるルールの集合によって定義されます。例えば、\(x(y + z) = xy + xz\) のような計算のルールの集合で定義されます。この集合を公理系とか理論と呼びます。再帰的に公理化可能とは、公理系を構成するルールの全てを有限な計算で定めることができるということです。

　ルールが有限個なら言うまでもなく再帰的に公理化可能ですが、通常の自然数論の公理系には無限個のルールがあります。無限個のルールをいかにして有限な計算で定めるかが工夫のしどころとなります。論理式番号を使って無限個のルールに番号を振るのも１つの方法です。

　続いて、万能論理式の話に入りましょう。論理式番号を \(m\) として、 \(m\) 番目の１変数論理式 \(f(y)\) と論理的に同値となる論理式を \(u(m,y)\) とします。これは、あらゆる文法的に正しい自然数論の１変数論理式を表すことができる万能論理式です。つまり、任意の論理式番号 \(m\) と入力 \(n\) に対して以下の関係が成り立ちます。

\[ u(m,n) \Leftrightarrow f(n) \]

　今のところ、万能論理式 \(u(x,y)\) が存在するかどうかはまだ分かりませんが、とりあえず一旦存在すると仮定しましょう。

　ところで、このページでは \(x,y,z\) などは変数を表し、\(a,c,g,k,m,n\) などは定数を表すとします。変数の値は具体的に定まっていませんが、定数は定まっていると考えます。つまり、定数はその値を使って具体的に計算を実行することができます。そして、変数のある論理式の変数全てに定数を代入した論理式を閉論理式と呼ぶことにします。つまり、論理式 \(A(x,y)\) の変数 \(x,y\) に定数 \(m,n\) を代入した \(A(m,n)\) のような論理式が閉論理式です。さらに、元から変数の無い論理式のことも閉論理式に含めます。また、ここでは詳しく説明しませんが、変数が全て量化子で束縛されている論理式も閉論理式です。

　変数のある論理式は変数が変数のままでは具体的な値が定まらず。 \(x = x\) のような例外を除いて真理値は定まりませんが、閉論理式なら具体的な計算が実行可能なので必ず真理値が定まっていると考えられます。以下の議論では真理値が定まっている論理式を主体的に扱います。

【リシャールのパラドクス】

　ここでは、後の説明で核心的な役割を果たすリシャールのパラドクスについて説明します。

　まず、対象とする自然数論は無矛盾で標準モデルを持つと仮定します。標準モデルを持つとは、我々が普段使っている普通の自然数論で説明できるということです。自然数論には、標準モデル以外にも超準モデルと呼ばれる普通ではない自然数論もあります。

　例えば、「ここではきものをぬいでください」と言うひらがなの文章は、「ここで履物を脱いでください」という解釈と、「ここでは着物を脱いでください」という解釈が可能です。自然数論の言葉にも、このひらがなの文章のような曖昧さがあり複数の解釈が可能です。そのうち、標準モデルとは常識的な解釈であり、超準モデルとは、ちょっと変わった解釈です。超準モデルの自然数論では無限大の大きさの自然数があったりします。とりあえず、今はそういう普通じゃない自然数論は考えないことにします。

　次に、万能論理式 \(u(x,y)\) 自体が文法的に正しい自然数論の論理式だとします。 \(u(x,y)\) は万能論理式なので、あらゆる文法的に正しい自然数論の１変数論理式 \(f(y)\) に対して \(m\) を適当に選ぶと

\[ u(m,n) \Leftrightarrow f(n) \]

　とすることができます(\(n\) は任意の定数)。ただし、\(f(n)\) が自然数論として意味がない場合、例えば \(1-2\ne 0\cdot n\) の場合、 \(u(m,n)\) は偽としておきます。ところで、\(u(x,y)\) 自体が自然数論の論理式なので、\(\lnot u(y,y)\) も自然数論の論理式です(\(\lnot\) は否定を表す)。

　よって、\(f(y)\) を \(\lnot u(y,y)\) とおけば、

\[ u(m,n) \Leftrightarrow \lnot u(n,n) \]

　という関係が成り立ちます。しかしここで、任意の定数 \(n\) を \(n = m\) となるように選ぶと以下のように矛盾します。

\[ u(m,m) \Leftrightarrow \lnot u(m,m) \]

　\(u(m,m)\) とその否定が論理的に同値になるわけです。これがいわゆるリシャールのパラドクスです。

　つまり、自然数論の中に万能論理式 \(u(x,y)\) が存在すると仮定すると、上記のような矛盾が起こります。対象とする自然数論は無矛盾と仮定したので、これは、自然数論の中には万能論理式は存在しないと考える以外にありません。

　以下は補足です。\(u(m,n) \Leftrightarrow f(n)\) という関係が成り立つために標準モデルを持つという条件が必要になります。超準モデルだと、この関係は成り立ちません。もっと面倒な数式になります。そうした複雑さを避けるために標準モデルを持つと仮定しています。ちなみに標準モデルを持つという条件は、証明の概略の所で触れた、健全であるという条件と同じことなので気に留めておいてください。健全であることの正式な定義が標準モデルを持つことです。

【パラドクスの原因】

　パラドクスが起きた原因を探ってみましょう。それには \(u(x,y)\) がどのように作られているかを分析してみます。まず、\(x\) 番目の１変数論理式に \(y\) を代入した閉論理式のゲーデル数を返す関数を \(s(x,y)\) としましょう。これを代入関数と呼ぶことにします。代入関数は自然数論で原始帰納的に書けることをゲーデルさんが証明しています。

\[ s(x,y) = x~番目の１変数論理式に~y~を代入した閉論理式のゲーデル数 \]

　ここで、\(a\) は論理式 \(A(y)\) の論理式番号であり、また、\(n\) は任意の自然数であり、 \(⌈A(n)⌉\) は \(A(n)\) のゲーデル数であるとします。すると、

\[ s(a,n)=⌈A(n)⌉ \]

　という関係が成り立ちます。あとで使いますから憶えておいてくださいね。

　\(s(x,y)\) が自然数論で原始帰納的に書けることの証明は、非常に面倒臭いものですが、プログラマなら、これが簡単な構文解析で実現できることを直感的に理解できるでしょう。また、\(x\) 個以上の文法的に正しい１変数論理式を得るまでに、最大でも何桁のゲーデル数まで計算すればよいのか見積もれるので、バグがなければ無限ループに陥るような処理でもありません。つまり、原始帰納的に書けることはほぼ明らかです。

　ただし、これは対象となる理論が再帰的に公理化可能という前提があるからです。再帰的に公理化可能でない理論を考えると、 \(s(x,y)\) は必ずしも原始帰納的に書けるとは限りません。

　感覚的に説明すると、\(s(x,y)\) は、論理式番号 \(x\) と入力 \(y\) を指定して、文法的に正しい閉論理式を全てリストアップする関数です。例えば、実際に計算が実行できる計算可能な論理式などがリストアップされます。ただし、必ずしもアルゴリズムのある論理式がリストアップされるわけではありません。真理値を具体的に判定するアルゴリズムが無い論理式なども含まれます。ここでアルゴリズムとは有限回の計算で結果に到達する手続きのことです。また、無限に長い論理式はリストアップされません。無限に長い論理式は神様には計算可能かもしれませんが、 \(s(x,y)\) では取り扱いません。\(s(x,y)\) は原始帰納的なので、計算に必要ステップ数が有限である必要があるからです。つまり、無限に長い論理式は文法的に正しいとは考えません。

　続いて、文法的に正しい閉論理式 \(f\) のゲーデル数 \(z=⌈f⌉\) を入力すると、その真理値を \(1\) か \(0\) で返す関数を真理関数と呼び \(t(z)\) で表します。ただし、\(f\) が自然数論として意味のない閉論理式の場合は、 \(0\) を返すとしておきます。\(t(z)\) は以下のように定義されます。

\[ t(z) = \left\{ \begin{array}{cl} 1 & (~ゲーデル数が~z~の閉論理式~f~が真~) \\ 0 & (~ゲーデル数が~z~の閉論理式~f~が偽~) \end{array} \right. \]

　すると、\(F\) を自然数論として意味のある全ての閉論理式の集合とする時、以下の関係が成り立ちます。後で使いますから憶えておいてくださいね。

\[ \forall f\in F(~f ~\Leftrightarrow~ t(⌈f⌉)=1~)\tag{式★} \]

　\(\forall f\in F(...)\) という式は、集合 \(F\) に属する全ての \(f\) に対して \(...\) が成り立つという意味です。

　この \(s(x,y)\) と \(t(z)\) を使うと、万能論理式 \(u(x,y)\) は以下のように書けます。

\[ u(x,y):=t(s(x,y))=1 \]

　「\(:=\)」は左辺を右辺で定義するの意味です。先のコンパイラの例え話で言うと、\(s(x,y)\) が返すゲーデル数(実行ファイル)を \(t(z)\) という処理系で実行すると解釈できます。

　\(s(x,y)\) は、ゲーデルさんが自然数論で原始帰納的に書けることを証明しているので、何か間違いがあるとは思えません。すると、問題があるのは \(t(z)\) と言うことになります。つまり、\(F\) に属する任意の閉論理式のゲーデル数を与えると、その真理値を \(1\) あるいは \(0\) と判定するアルゴリズムのある \(t(z)\) は自然数論の中には存在しないということです。これをタルスキの定理と言うんだそうです。もし、そのような \(t(z)\) が存在すると、 \(t(z)=1\) は当然文法的に正しい自然数論の論理式になるので、 \(u(x,y)\) が文法的に正しい自然数論の論理式で書けることになり、リシャールのパラドクスが起こります。

　ただし、アルゴリズムの無い \(t(z)\) は存在します。しかしその場合、リシャールのパラドクスは起こりません。 \(t(z)=1\) が無限に長い論理式になって、文法的に正しい自然数論の論理式では書けないからです。つまり、\(t(s(y,y))=1\) は文法的に正しい自然数論の論理式にならないので、 \(\lnot u(y,y)\) も文法的に正しい自然数論の論理式にはなりません。したがって、万能論理式と同値とすることができないのです。よって、リシャールのパラドクスは回避されます。

【証明可能と証明関数】

　次に、「証明可能」という概念を説明します。以下の説明では、証明可能なこと自身を証明するというようなメタな議論をしますので、証明される証明のことを形式的証明と呼び、メタな証明と区別します。そして、「形式的に証明される」のように表現することとします。ただし、文脈から明らかな時は、形式的という言葉は省略することとします。

　専門書では、ここで数項だの表現定理だのを用いて自然数論を形式化しますが、はっきり言ってわけが分からないので、本ページではアバウトに行きます。感覚的には形式化とは、論理式をゲーデル数で表して数値計算することで証明を行うことです。また、表現定理というのは、我々が普段使っている自然数論で計算可能な関数や述語は、形式化された自然数論の中にも存在することを言います。

　それでは、証明関数から定義しましょう。そのゲーデル数が \(z\) であるような文法的に正しい閉論理式 \(f\) が、形式的に証明可能な時に \(1\)、証明不能な時に \(0\) を返す関数を証明関数と呼び \(p(z)\) で表します。ただし、\(f\) が自然数論として意味のない閉論理式の場合は \(0\) を返すとしておきます。\(p(z)\) は以下のように定義されます。

\[ p(z) = \left\{ \begin{array}{cl} 1 & (~ゲーデル数が~z~の閉論理式~f~は形式的に証明可能~) \\ 0 & (~ゲーデル数が~z~の閉論理式~f~は形式的に証明不能~) \end{array} \right. \]

　気持ちとしては、反証可能なときに \(p(z)=0\) としたいところですが、そうすると \(p(z)=1\) の否定を \(p(z)=0\) と簡単に表すことが出来なくなります。よって、反証可能は \(p(\ng(z))=1\) で表します。ただし、\(\ng(⌈f⌉)=⌈\lnot f⌉\) であるとします。

　「証明可能」と「真」という概念は似ていますが別物であることに注意してください。

　真偽の概念は、閉論理式を実際に値から計算して決定します。そのため、無矛盾な理論の場合、真偽は原理的に必ずどちらかに定まっています。ただし、全ての自然数に対してホニャララが成り立つのような閉論理式の場合、自然数１つ１つを全て計算するので無限の計算能力が必要になります。つまり、神様でないと真か偽かは分からないことがあります。すなわち、真か偽、どちらになるかは人間には分からない場合はあるけれど、どちらかにはなることは原理的に決まっています。

　一方、証明可能は、あらかじめこれは正しいと決めておいた公理系の論理式から推論規則で変形を繰り返し、目的の論理式にたどり着いた場合に証明可能と判定します。推論規則による変形は正しさを保存しますので目的の論理式も正しいことになります。目的の論理式の否定にたどり着いた場合は反証可能と言います。概念的には、「証明可能」と「真」「反証可能」と「偽」が対応しています。重要なことは変形の回数は有限でなければならないということです。これは、証明という行為が人間に計算可能であると考えるからです。つまり、無限に変形を繰り返せば目的の論理式やその否定にたどり着くという場合は、正しい証明とは認めません。形式的証明は必ず有限でなければならないのです。

　そのため、公理系に公理が足りていないと、有限回の変形では目的の論理式やその否定にたどり着かない場合が出てきます。このような場合は証明も反証もできません。もし、無限回の変形を許せば、無限回の計算が可能ということになり、ある程度の公理がそろっていれば、真偽の概念と同様に必ず証明か反証ができることになりますが、変形は必ず有限回なので、そういうことは起こりません。

　また、あらかじめ正しいと決めておく公理系の選択がまずいと、証明可能であり反証可能でもあるという状態になることがあります。このような状態を形式的に矛盾すると言います。要するに、形式的には公理系が無矛盾である保証は実はどこにもないのです。

　このように、「証明可能」と「真」という概念は原理が異なります。証明可能は有限な概念であり、真とは無限を含む概念です。そして、少し先走って結論を書いてしまうと。ある条件を満たす理論の証明関数では、ある種の閉論理式が証明も反証もできないことは避けられないというのが不完全性定理の結論です。

　ところで、ここで考える証明関数は計算可能であるとします。大雑把に言えば結果を計算するプログラムが存在するということです。プログラムは、コンピュータを操作する有限な長さの記号列でなければなりません。したがって、プログラムが存在すれば、それは文法的に正しい論理式に翻訳することが可能です。プログラムが存在しないような証明関数を考えると、以下の議論は成り立ちませんので注意してください。理由についてはこちらに書いてあります。

　証明関数の具体的プログラムの１つは、ゲーデル数のカウントアップを使ってあり得る形式的証明の全てを生成して、ゲーデル数が \(z\) の閉論理式の証明になっていないかチェックするというものです。形式的証明も記号列で表されますからゲーデル数で表すことができます。よって、形式的証明が存在するならカウントアップでいずれは到達します。したがって、このプログラムでは形式的証明が存在するなら必ず証明できます。問題が難しいから証明できないということはありません。逆に、形式的証明が存在しない場合は計算が終了しません。

【証明関数の不完全性】

　さて、ここからいよいよ不完全性の話です。上記で定義した証明関数を用いて形式的完全性を定義しましょう。自然数論のような理論が形式的に完全であるとは、 \(F\) に属する任意の閉論理式 \(f\) に対して、少なくとも \(p(⌈f⌉)\) あるいは \(p(⌈\lnot f⌉)\) が必ず \(1\) を返すことを言います。 \(F\) に属する閉論理式は、少なくとも形式的に証明あるいは反証できるということです。つまり、以下の条件を満たすとき形式的に完全であると言います。

\[ \forall f\in F(~p(⌈f⌉)=1 \lor p(⌈\lnot f⌉)=1~) \]

　「\(\lor\)」は「または」の意味の論理演算子です。また、まともな理論の証明関数は、 \(p(⌈f⌉) = 1\) のとき閉論理式 \(f\) は真となり、 \(p(⌈\lnot f⌉) = 1\) のとき閉論理式 \(f\) は偽となるという条件も満たしていないと意味がありません。つまり、「証明可能なら真」「反証可能なら偽」ということです。これを健全性と言います。証明可能な論理式の真理値が偽だったら、そんな証明に意味はありませんよね？まともな理論において健全性は証明関数が証明関数であるために譲れない条件です。ここは重要ですから憶えておいてくださいね。つまり、まともな理論では

\[ \forall f\in F(~p(⌈f⌉)=1 ~\Rightarrow~ f~) \tag{式※} \]

　が成り立ちます。上記の関係が成り立つとき、 \(f\) が証明可能なら \(f\) は真になることはすぐに理解できると思いますが、反証可能なら偽となることはすぐには分からないかもしれません。今、\(f\) が反証可能として \(f_n:=\lnot f\) とします。 \(f\) は反証可能なので \(p(⌈\lnot f⌉)=1\) です。つまり、\(p(⌈f_n⌉)=1\) です。よって、\(p(⌈f_n⌉)=1\Rightarrow f_n\) より \(f_n\) は真です。\(f_n:=\lnot f\) ですから \(f\) は偽となります。したがって、\(f\) が反証可能なら \(f\) は偽です。

　ここで、もし対象となる理論が形式的に完全かつ健全だとすると、完全性より、\(F\) に属する任意の閉論理式 \(f\) は必ず証明あるいは反証できます。このとき、もし \(f\) が真であれば、健全性より、\(p(⌈f⌉)=1\) でなければなりません。 \(p(⌈\lnot f⌉)=1\) だとすると \(f\) は偽でないとつじつまが合わないからです。したがって、

\[ \forall f\in F(~f ~\Rightarrow~ p(⌈f⌉)=1~) \]

　が成り立ちます。よって、(式※)と合わせると、 \(p(z)\) は以下の関係を満たします。

\[ \forall f\in F(~f ~\Leftrightarrow~ p(⌈f⌉)=1~) \]

　すると、\(p(z)\) は先の \(t(z)\) そのものとなり（ (式★)参照）、 \(t(z)=p(z)\) となるので、万能論理式 \(p(s(x,y))=1\) が作れることになります。 \(p(z)\) にはプログラムがあると仮定したので、 \(p(z)=1\) は文法的に正しい自然数論の論理式になります。よって、そのままではリシャールのパラドクスが起きてしまいます。したがって、矛盾を回避するには完全性をあきらめる必要があります。健全性は譲れない条件ですからあきらめるわけにはいきません。

　まとめると、健全性が成り立ち、代入関数 \(s(x,y)\) が原始帰納的で証明関数 \(p(z)\) が計算可能であるような数学的理論において、リシャールのパラドクスを回避したければ、その理論は不完全になるということです。つまり、その理論に形式的完全性の条件を満足する証明関数は存在しません。

　通常の自然数論では代入関数が原始帰納的に書けますので、その自然数論が健全で証明関数が計算可能なら、その自然数論は不完全ということになります。

　我々が普段使う通常の自然数論はペアノ算術と呼ばれていますが、ペアノ算術の証明関数は計算可能です。つまり、ペアノ算術の証明関数をコンピュータで計算するためのプログラムが存在します。興味のある方はペアノ算術の公理系について調べてみるといいでしょう。よって、ペアノ算術は健全なら不完全ということになります。普通はペアノ算術は健全であると仮定してしまうので、これにより自然数論の不完全性が証明できました。

　ところで、アルゴリズムと計算可能という言葉の使い方が気になった人もいるかもしれません。自然数論は不完全で \(p(z)\) は特定の \(z\) に対して証明あるいは反証するアルゴリズムが無いのに、 \(p(z)\) を計算可能と言ってもいいのかと。私もこの言葉の使い方は気持ち悪いんですが、計算理論では、このような部分的にアルゴリズムが無い、つまり、有限回の計算で結果にたどり着かないことがある関数も、全体としてプログラムで記述できる場合は計算可能とみなします。

【補足】

　最後に、証明関数 \(p(z)\) に関して注意すべき点が１つあります。 \(p(z)\) の値を計算するとき、計算が永遠に終わらない場合があるのです。つまり、\(p(z)\) は原始帰納的ではありません。そして、計算が終わらないときは \(p(z)=0\) であると考えます。何故ならば、計算が終了しないのなら証明も終了しないからです。証明が終了しないのなら証明不能です。つまり、値は \(0\) でなくてはなりません。しかし、実際には \(0\) であることを確認することはできません。終了しないのですから。

　この点は結構重要で、もし１日コンピュータで \(p(z)\) を動かせば必ず終了するのだとするとすごいことが起こります。例えば、数学上の未解決な問題を１つ持ってきて \(A\) という論理式で表すとします。すると、\(p(z)\) に \(⌈A⌉\) および \(⌈\lnot A⌉\) を入力すれば、それが肯定的に解決されるのか否定的に解決されるのか、もしくは証明も反証もできない類の問題なのか１日あれば判明することになります。これでは数学者は全員失業ですね。

　実際には、太陽が赤色巨星になるまで \(p(z)\) を動かし続けても結果が \(1\) か \(0\) か分からないかもしれません。このページではいとも簡単に \(p(z)=0\) のように計算が終了したかのように書いてますが、場合によっては、ある意味これは神の視点と言えるでしょう。

【ゲーデル文】

　今までの説明で、不完全性は証明されましたが、まだ具体的に形式的証明も反証もできない閉論理式は構成していません。ここでは、実際に証明も反証もできない閉論理式がどんなものか確認してみましょう。以下では、対象となる理論は健全であると仮定します。

　まず、以下のような１変数論理式 \(G(y)\) を定義します。

\[ G(y):=\lnot(p(s(y,y))=1) \]

　ただし、\(p(z)\) は計算可能な証明関数であり自然数論で書けるとします。 \(s(x,y)\) は代入関数で原始帰納的に書けるとします。つまり、自然数論で書けるとします。

　\(G(y)\) は自然数論の１変数論理式なので、論理式番号が対応しています。仮にその論理式番号を \(g\) とすると、\(G(g)\) が目的の閉論理式になります。この \(G(g)\) のことをゲーデル文と呼びます。

　本当に証明も反証もできないか確認してみましょう。まず、\(G(g)\) が形式的に証明可能と仮定してみます。すると、以下のようになります。

\[ \begin{eqnarray} p(⌈G(g)⌉)=1 &\Rightarrow & G(g) ~~\cdots 証明可能なら真(式※)より\\ &\Leftrightarrow& \lnot(p(s(g,g))=1) \\ &\Leftrightarrow& \lnot(p(⌈G(g)⌉)=1)~~\cdots s(g,g)=⌈G(g)⌉~より \end{eqnarray} \]

　証明可能、つまり \(p(⌈G(g)⌉)=1\) と仮定したのに、\(\lnot(p(⌈G(g)⌉)=1)\) が導かれ矛盾します。

　今度は、\(G(g)\) が形式的に反証可能と仮定してみましょう。すると、以下のようになります。

\[ \begin{eqnarray} p(⌈\lnot G(g)⌉)=1 &\Rightarrow & \lnot G(g) ~~\cdots 反証可能なら偽(式※)より\\ &\Leftrightarrow& p(s(g,g))=1 \\ &\Leftrightarrow& p(⌈G(g)⌉)=1 \end{eqnarray} \]

　反証可能、つまり、\(p(⌈\lnot G(g)⌉)=1\) と仮定したのに、 \(p(⌈G(g)⌉)=1\) が導かれ、形式的に矛盾します。健全なら形式的に無矛盾のはずなので、これも矛盾です。証明可能と仮定しても反証可能と仮定しても矛盾するため、 \(G(g)\) は証明も反証もできません。すなわち、\(p(⌈G(g)⌉)=0\) かつ \(p(⌈\lnot G(g)⌉)=0\) です。これを第一不完全性定理と言います。

　少し補足しておきますと、ここでは形式的矛盾とメタな矛盾の両方が出てきました。メタな矛盾は我々が普段使っている論理の矛盾ですから、あり得るはずがないと強く信じられています。ゆえに、背理法が意味を持ちます。一方で、形式的に矛盾する形式的理論はあり得ます。ただ、そのような理論では、どんな間違った定理でも証明できるので、あまり役には立ちません。上記の証明では、健全と仮定した理論が、つまり形式的に無矛盾なはずの理論が形式的に矛盾するという結論を導いたので、メタな証明においても矛盾なわけです。

　ここでは、第一不完全性定理の条件として健全性を仮定しましたが、これを無矛盾という仮定に弱めたロッサーの定理について興味のある人はをご覧ください。専門書で紹介されているような込み入った証明ではなく、簡単な仮定から導く独自の証明を紹介しています。

【\(\Sigma_1\)完全性】

　専門書で紹介される第一不完全性定理では、ゲーデル文が証明できないことを示すのに、健全性ではなく\(\Sigma_1\)完全性が用いられています。これは、後の第二不完全性定理への応用を考えると必要になることです。 \(\Sigma_1\)完全性を用いる方法では、形式的に無矛盾という仮定でゲーデル文が証明できないことが示せます。なので一応、\(\Sigma_1\)完全性版の証明も示しておきます。

　まず、\(\Sigma_1\)完全性を説明します。それは、もし \(p(x)=1\) が\(\Sigma_1\)論理式なら、「\(p(a)=1\) が真ならば \(p(a)=1\) は形式的に証明できる」という性質です。ただし、\(a\) は任意の定数です。 \(\Sigma_1\)論理式というのは、大雑把に言って計算可能な論理式ということです。コンピュータを用いて有限的に計算できる論理式が\(\Sigma_1\)論理式です。

　\(\Sigma_1\)論理式が真なら、真という結果に至るアルゴリズムがあります。アルゴリズムが無ければ偽と考えます。よって、真ならコンピュータの計算手順をたどることにより、有限的に真であることが証明できます。直観的には明らかですね。

　では、その理論が無矛盾ならゲーデル文が証明できないことを示しましょう。 \(p(x)=1\) は\(\Sigma_1\)論理式とします。もし、ゲーデル文 \(G(g)\) が証明できると仮定すると、

\[ \begin{eqnarray} p(⌈G(g)⌉)=1 &\Leftrightarrow& p(s(g,g))=1 \\ &\Leftrightarrow& \lnot G(g) ~~\cdots~ \lnot G(g)~は\Sigma_1論理式 \\ &\Rightarrow & p(⌈\lnot G(g)⌉)=1 ~~\cdots~ \Sigma_1完全性より \end{eqnarray} \]

　となり、\(G(g)\) が証明できれば \(\lnot G(g)\) も証明できます。よって、ゲーデル文が証明できるならその理論は形式的に矛盾します。つまり対偶を考えると、その理論が無矛盾ならゲーデル文は証明できません。

【ゲーデル文の真理値】

　その理論が健全なら、ゲーデル文は形式的に証明も反証もできないことが分かりました。では、ゲーデル文の真理値はどうなっているのでしょうか？

　とある入門書によると、ゲーデル文もゲーデル文の否定も自然数論と矛盾しないそうです。ただし、その理論が健全なら、標準的な解釈の下でゲーデル文は真になるそうです。そのため、不完全性定理は「正しいのに証明できない閉論理式がある」と説明されるようです。このざっくりとした説明が結構曲者なんです。ちょっと確認してみましょう。

　ゲーデル文は、その理論が健全なら形式的に証明も反証もできませんでした。つまり、健全なら \(p(⌈G(g)⌉)=0\) かつ \(p(⌈\lnot G(g)⌉)=0\) です。よって、健全なら \(p(⌈G(g)⌉)=0\) は真です。そこからたどると、

\[ \begin{eqnarray} p(⌈G(g)⌉)=0 &\Leftrightarrow& \lnot(p(⌈G(g)⌉)=1) \\ &\Leftrightarrow& \lnot(p(s(g,g))=1) \\ &\Leftrightarrow& G(g) \end{eqnarray} \]

　のようになります。つまり、\(G(g)\Leftrightarrow p(⌈G(g)⌉)=0\) であり、その理論が健全ならゲーデル文は真だと分かります。

　ちょっと待った！その理論が健全ならゲーデル文は証明も反証もできないはず。しかしここでは、ゲーデル文が真であることが証明されているじゃないか！と言いたくなるでしょう。はい、確かにゲーデル文が証明されてしまってますが、この証明は証明関数 \(p(z)\) の扱う証明の対象外なんです。不完全性定理を、どんな方法を使っても証明できない閉論理式があると誤解している人もいるかもしれませんが、実はそうではないのです。自然数論からはみ出してよいのなら、つまり形式的証明でないのならゲーデル文も証明できます。

　そのカラクリを説明しましょう。上記の証明は、\(G(y)\) の論理式番号 \(g\) を使っています。 \(g\) はもう少し正確に書けば、以下のような

\[ \newcommand{\fton}{\mathrm{fton}} g = \fton(G) \]

　論理式 \(G\) を自然数の論理式番号 \(g\) へ対応させる関数 \(\fton(x)\) の \(x = G\) の場合です。しかし、自然数論の中には自然数を自然数に対応させる関数しか含まれていません。つまり、\(\fton(x)\) のような関数は自然数論の中には存在しません。上記の証明は自然数論の体系外にはみ出しているのです。 \(G(g)\) のゲーデル数 \(⌈G(g)⌉\) を表す \(⌈~x~⌉\) なども自然数論の関数ではないですね。

　もちろん、\(g\) や \(⌈G(g)⌉\) が論理式と対応しているなどと考えず、単に何らかの自然数であるとみなせば、

\[ G(m) \Leftrightarrow p(n)=0\ \]

　という関係を満たす自然数 \(m\) と \(n\) があるということは自然数論の中の話です。ただしその場合、\(G(g)\) が形式的に証明できないという結果は導けません。ゲーデル数が解釈できない場合、健全性を前節の証明に使うことはできないからです。つまり、\(p(⌈G(g)⌉)=1\Rightarrow G(g)\) が使えません。

　また、健全なら \(p(⌈G(g)⌉)=0\) という閉論理式は標準モデル（標準的解釈）で成立しています。標準モデルとは何ぞやという人もいると思いますが、モデルについては後で詳しく説明します。とりあえず簡単に説明すると、論理式の意味はそれを解釈する世界に応じて複数の意味があり、標準モデルというのは、我々が普段用いている自然数論の解釈を用いる世界です。

　標準モデルでは、論理式番号やゲーデル数の中身を解釈すれば、普通の意味を考えることができて、 \(p(⌈G(g)⌉)=0\) という論理式の意味は、その理論が健全なら「 \(G(g)\) は形式的に証明できない」というものになります。しかし、\(G(g)\Leftrightarrow p(⌈G(g)⌉)=0\) であり、健全なら \(p(⌈G(g)⌉)=0\) は成立しているので、これは同時に標準モデルで、健全なら \(G(g)\) が成立していることの証明にもなっています。「形式的に」という言葉と「標準モデルで」という言葉の違いを見落とすと、何だか矛盾しているように見えます。

　実は、\(p(z)\) が行う証明は形式的証明です。形式的証明は全てのモデルに共通の公理のみを用いて証明されねばならず、標準モデル以外でも成立しないといけません。しかし、健全なとき \(G(g)\) は標準モデル以外では成立している保証はありません。なので、上記の証明があっても、健全なら「\(G(g)\) が形式的に証明できる」となることはありません。つまり、標準モデルで、健全なら \(p(⌈G(g)⌉)=1\) となることはありません。

　何かだまされたような気もするでしょうが、きっとだまされてます。私の言うことなど信じてはダメですよ(と、嘘つきのパラドクス風に言ってみる)。

【モデル】

　ゲーデル文は真と仮定しても偽と仮定しても自然数論と矛盾しないそうですが、これは、モデルの概念を使って、次のようなアナロジーを考えると納得できると思います。思いっきり簡単な例として、以下の串団子の公理系というものを考えます。

串団子とは、串に団子を三つ刺したものであり、それに限る。
団子の種類は白玉団子か抹茶団子である。
見た目が同じ串団子は同じである。
見た目が異なる串団子は同じではない。

　串団子作りが自然数論に対応すると考えてください。すると「全ての串団子は同じである」という文が、真と仮定しても偽と仮定しても矛盾しない文に該当します。つまり、ゲーデル文に対応します。全ての串団子が同じになるモデルもならないモデルも考えることができます。

　まず、団子が白玉団子しかないモデルを考えてみます。どんな串団子の作り方をしても、白玉団子が三つの串団子になりますので、このモデルでは「全ての串団子は同じである」は正しく、その真理値は真です。

　次に、白玉団子と抹茶団子があるモデルを考えてみます。明らかに、白玉と抹茶の組み合わせにより見た目が異なる串団子が作れますので、このモデルでは「全ての串団子は同じである」は正しくなく、その真理値は偽です。

　これに対して「串に団子を一つ刺したものは串団子ではない」は、全てのモデルで正しい真なる命題となります。え？団子が一つでも串団子だろって？いやいや、ここでは公理で団子を三つ刺したものだけが串団子と約束したので、団子が一つの場合は串団子とは認めません。

　さて、様々なモデルを考えると、ゲーデル文の真偽は定まっていないというのなら、ゲーデル文かゲーデル文の否定を公理として自然数論に付け加えてやれば、完全な理論が得られるのではないでしょうか？残念ながら、そうして得られた新しい理論でも新しいゲーデル文（正確にはロッサー文）が作れます。なら、それも公理に付け加えてといくら繰り返しても、新しいゲーデル文は尽きることがありません。結局、自然数論を含むような理論は、ゲーデル文を有限な方法で次々と加えるというやり方で拡大する限り、全て不完全ということになります。正確には、ゲーデル文の否定を公理系に追加すると\(\Sigma_1\)健全性が破れるので、このお話はゲーデル文ではなくロッサー文と呼ばれるその親戚に関して成り立ちます。

【完全な自然数論】

　不完全性定理から、通常の自然数論を有限な方法で拡大した理論は全て不完全です。すると、完全な自然数論というものは存在しないのでしょうか？いえ、実は通常の自然数論でなければ完全な自然数論もあり得ます。そのような完全な自然数論は、真の算術(TA)と呼ばれています。

　真の算術は、自然数論の標準モデルで真となる閉論理式全てからなる理論です。つまり、標準モデルで正しい閉論理式の全てを公理にしてしまった理論です。ですから当然、全ての閉論理式が形式的に証明あるいは反証可能ということになります。全ての閉論理式は、それ自身かその否定が必ず公理系の中にリストアップされているのですから。

　ここで、真の算術が不完全性定理の対象から外れる理由を見ていきましょう。真の算術は形式的に完全ですから、任意の閉論理式のゲーデル数 \(z\) に対して、その閉論理式が形式的に証明可能なら証明関数 \(p(z)\) が 1 を返し、反証可能なら 0 を返します。真の算術の公理は全ての正しい閉論理式の集まりですから、証明される閉論理式は全て真であり、反証される閉論理式は全て偽です。そして、全ての閉論理式は必ず証明あるいは反証できます。よって、\(p(z) = t(z)\) とおけば、\(p(z)\) は真の算術の証明関数になります。真の算術の場合、\(t(z)=1\) は無限に長い論理式となって自然数論では書けません。したがって、\(p(z)=1\) は自然数論では書けなくなります。言い換えると \(p(z)\) はプログラムで書けなくなります。ゲーデル文は \(p(z)=1\) を使って作りましたから、真の算術では、ゲーデル文が自然数論では書けないことになります。つまり、真の算術の中にはゲーデル文が存在しないというわけです。

　なんだ、完全な自然数論もあるんじゃないか。なら、それを使えばいいじゃない。と思うかもしれませんが、それには大きな困難が立ちはだかります。証明関数 \(p(z)\) が計算可能であることを、その理論が再帰的に公理化可能と言います。しかし、真の算術の場合、 \(p(z)=1\) は無限に長い論理式となって \(p(z)\) が計算可能となりません。つまり、真の算術は再帰的に公理化可能ではありません。何か神ががった力で計算することが可能なのかもしれませんが、普通のやり方では、真の算術は人間には取り扱い不能ということです。

【ゲーデル文は論理的帰結か？】

　ゲーデル文は、様々な自然数論のモデルを考えると、真にも偽にもなるはずなんですが、上記では標準モデルにおいて、健全ならゲーデル文の真理値が真だと証明しました。本当にゲーデル文が恒真式ではないのか心配ですよね。確認してみましょう。ちなみに恒真式とは、全てのモデルで真になる閉論理式のことです。恒偽式というものもあって、全てのモデルで偽になる閉論理式のことです。

　なお、ここでは論理的帰結のことを恒真式、その反対を恒偽式と書いています。正しい用語ではありませんが、他に適切で短い表現を思いつかなかったので、このページに限った表現ということでご理解ください。専門書を読むときは、ここでの表現は忘れてくださいね。

　ゲーデルさんは不完全性定理で有名ですが、それ以外にも、まぎらわしい名前の定理を証明しています。完全性定理と言います。完全性定理によると、一階述語論理による自然数論の恒真式は必ず形式的に証明できます。もちろん、自然数論の恒真式なら自然数論を用いて必ず証明できると言う意味です。また、その逆に、証明できれば必ず恒真式です。さらに、論理的には同じことですが、恒偽式なら必ず形式的に反証でき、反証できれば必ず恒偽式です。

　まず、ゲーデル文は恒真式だと仮定してみましょう。すると、以下のようになります。

\[ \begin{eqnarray} G(g)~は恒真式 &\Leftrightarrow& p(⌈G(g)⌉)=1 ~~\cdots 恒真式なら形式的に証明できる \\ \end{eqnarray} \]

　一方、恒真式は真なので、ゲーデル文はその定義より以下のようになります。

\[ \begin{eqnarray} G(g) &\Leftrightarrow& \lnot(p(s(g,g))=1) \\ &\Leftrightarrow& \lnot(p(⌈G(g)⌉)=1) ~~\cdots s(g,g)=⌈G(g)⌉~より \end{eqnarray} \]

　\(p(⌈G(g)⌉)=1\) かつ \(\lnot(p(⌈G(g)⌉)=1)\) となり矛盾します。以上のことよりゲーデル文は恒真式ではありません。

　次に、ゲーデル文は恒偽式だと仮定してみましょう。すると、以下のようになります。

\[ \begin{eqnarray} G(g)~は恒偽式 &\Leftrightarrow& p(⌈\lnot G(g)⌉)=1 ~~\cdots 恒偽式なら形式的に反証できる \end{eqnarray} \]

　一方、恒偽式は偽なので、ゲーデル文はその定義より以下のようになります。

\[ \begin{eqnarray} \lnot G(g) &\Leftrightarrow& p(s(g,g))=1 \\ &\Leftrightarrow& p(⌈G(g)⌉)=1 \end{eqnarray} \]

　\(p(⌈\lnot G(g)⌉)=1\) かつ \(p(⌈G(g)⌉)=1\) となり形式的に矛盾します。健全なら形式的に無矛盾のはずなので、これは矛盾です。以上のことよりゲーデル文は恒偽式でもありません。つまりゲーデル文は、モデルにより真にも偽にもなります。

　これは、不完全性定理のもう一つの証明と見ることもできます。恒真式でないものは証明できず(証明できれば必ず恒真式の対偶)、恒偽式でないものは反証もできないからです(反証できれば必ず恒偽式の対偶)。

　ただ、この証明、自分の乗っている土台の正しさを土台に乗ったまま証明するようなもので、そもそも土台が間違ってたら台無しという状態なんだそうです。不完全性定理を証明するような時は、有限の立場という制限された立場で証明しないといけないそうで、完全性定理などは贅沢すぎる道具なんだそうです。なので、ここでの証明は、あくまで検算と思ってください。

　しかし、こうして見ると、ゲーデルの不完全性定理って、モデルによって真にも偽にもなる閉論理式なんて、全てのモデルに共通の性質を定めた公理からは形式的に証明できるはずがないじゃない。と言ってるだけなんですね。

【ロッサーの定理】

　今まで、不完全性定理の前提条件として健全性を仮定してきました。健全とは、証明できる命題は真であるということです。なんだか当たり前のことのようですが、結構重要な意味を持つ条件です。

　しかし、この条件は無矛盾性にまで弱めることができます。現在、自然数論の第一不完全性定理と言えば、理論 \(T\) が無矛盾で再帰的に公理化可能なら不完全であるという形で述べられます。つまり、理論 \(T\) では証明も反証もできない論理式が存在することになります。健全性を無矛盾性にまで弱めた第一不完全性定理のことをロッサーの定理と言います。ここでは、私が独自解釈したロッサーの定理の証明を紹介します。二通りの方法で証明します。

【互換性による証明】

　まずは、簡単な方法です。簡単なのは良いのですが、私自身、細部を十分には検証できていないので、話半分で読んでください。

　始めに、第一不完全性定理の前提条件として、対象となる理論 \(T\) は再帰的に公理化可能な自然数論とします。再帰的に公理化可能とは大雑把に言って、その理論の証明が有限な方法で行えるということです。つまり、証明が自然数の有限な計算に翻訳できるということです。自然数論の中で証明を行うには、証明という行為を自然数の計算で表現する必要があります。そしてここでは、既に説明した第一不完全性定理の証明とは異なり、健全性の代わりに理論 \(T\) の無矛盾性と以下に示す互換性が成り立つと仮定します。 \[ \begin{eqnarray} p(⌈p_c(a)=1⌉)=1~\Rightarrow~p(a)=1 \\ p(⌈p_c(a)=0⌉)=1~\Rightarrow~p(a)=0 \end{eqnarray}\tag{互換性} \] 　ここで、\(p(x)\) は理論 \(T\) の証明関数です。証明関数とは、 \(x\) が理論 \(T\) で証明可能な閉論理式のゲーデル数なら \(1\) を返し、 \(x\) が理論 \(T\) で証明不能な閉論理式のゲーデル数なら \(0\) を返す関数のことです。 \[ p(x)= \begin{cases} 1 & (x~が証明可能な閉論理式のゲーデル数) \\ 0 & (x~が証明不能な閉論理式のゲーデル数) \end{cases} \] 　閉論理式とは大雑把に言って真偽の定まった論理式のことです。論理式とは真か偽かを問える命題を数式に翻訳したものです。例えば、\(1=0\) は真理値が偽の閉論理式です。ゲーデル数とは論理式に振られた番号のことで、 UTF-8 や Shift_JIS のような文字コードを想像してもらうと分かりやすいと思います。自然数論では自然数しか扱えませんので、論理式も自然数を割り当てて表現します。そして、\(f\) が任意の閉論理式のとき、\(⌈f⌉\) は \(f\) のゲーデル数を表します。例えば、\(⌈p_c(a)=1⌉\) は閉論理式 \(p_c(a)=1\) のゲーデル数です。

　ここで、\(a\) は任意の閉論理式のゲーデル数とします。また、\(p_c(x)\) を互換性のある証明関数と呼び、互換性を満たすように定義されている証明関数とします。私自身が細部を十分に検証できていないと言ったのは、この互換性のある証明関数が、どのような場合に定義できるのか十分には確認できていないからです。少なくとも、健全性が成り立つ場合は、\(p_c(x)=p(x)\) とおけば、互換性は成り立ちます。互換性が成り立つなら、その理論の中で形式的に証明するという行為に自己言及できることになります。

　これは私の推測ですが、理論 \(T\) が再帰的に公理化可能であれば互換性は成り立つと思います。ペアノ算術を健全性が成り立たない方向へ拡大するには、自然数の中に無限を表す定数を追加する必要があるのですが、少なくとも、これらの定数を再帰的に列挙できる場合は互換性は成り立ちます。つまり、無限を表す定数を明示的に導入するような場合なら互換性は成り立ちます。

　重要なことは、互換性は健全性が成り立たない場合も成り立つということです。つまり、健全性が成り立たない理論に対して不完全性定理の適用範囲を拡張できます。もし、再帰的に公理化可能であれば互換性が成り立つのならば、第一不完全性定理を無矛盾で再帰的に公理化可能な理論にまで拡張できます。

　さらに、論理式 \(G(x)\) を以下のように定義します。ただし、\(\lnot\) は否定を表す記号で、「\(\lnot A\)」は「\(A\) でない」を意味します。 \[ \begin{eqnarray} G(x) & := & p_c(s(x,x))=0 \\ \lnot G(x) & := & p_c(s(x,x))=1 \end{eqnarray} \] 　ここで、\(G(x)\) の論理式番号を \(g\) で表し、 \(G(g)\) を修正ゲーデル文と呼ぶことにします。論理式番号とは全ての１変数論理式に振られた番号のことです。 \(s(x,y)\) は代入関数であり、 \(s(g,n)=⌈G(n)⌉\) と定義されています。つまり、論理式番号に対応する論理式に自然数 \(n\) を代入してそのゲーデル数を返します。

　これで準備完了です。それでは不完全性を証明しましょう。まず、\(G(g)\) が理論 \(T\) で証明できると仮定します。つまり、\(p(⌈G(g)⌉)=1\) です。すると、 \[ p(⌈G(g)⌉)=1~\Leftrightarrow~p(⌈p_c(s(g,g))=0⌉)=1 \] となり、互換性を使うと、 \[ \begin{eqnarray} p(⌈p_c(s(g,g))=0⌉)=1 & ~\Rightarrow~ & p(s(g,g))=0 \\ & ~\Leftrightarrow~ & p(⌈G(g)⌉)=0 \end{eqnarray} \] となり、\(p(⌈G(g)⌉)=1 \Rightarrow p(⌈G(g)⌉)=0\) となって矛盾します。よって、背理法により \(p(⌈G(g)⌉)=0\) となり、 \(G(g)\) は理論 \(T\) では証明できません。

　次に、\(G(g)\) が理論 \(T\) で反証できると仮定します。つまり、\(p(⌈\lnot G(g)⌉)=1\) です。すると、 \[ p(⌈\lnot G(g)⌉)=1~\Leftrightarrow~p(⌈p_c(s(g,g))=1⌉)=1 \] となり、互換性を使うと、 \[ \begin{eqnarray} p(⌈p_c(s(g,g))=1⌉)=1 & ~\Rightarrow~ & p(s(g,g))=1 \\ & ~\Leftrightarrow~ & p(⌈G(g)⌉)=1 \end{eqnarray} \] となり、\(p(⌈\lnot G(g)⌉)=1 \Rightarrow p(⌈G(g)⌉)=1\) となって理論 \(T\) が矛盾します。\(T\) は無矛盾と仮定したのでこれは矛盾です。よって、背理法により \(p(⌈\lnot G(g)⌉)=0\) となり、 \(G(g)\) は理論 \(T\) では反証できません。

　以上により、修正ゲーデル文 \(G(g)\) は理論 \(T\) では証明も反証もできません。これで、健全性を無矛盾性まで弱めた第一不完全性定理が証明できました。

【ロッサーの方法による証明】

　次に、ロッサーの方法による証明を私の独自解釈で説明します。まず、準備をしましょう。 \(\Sigma_1\)論理式と\(\Pi_1\)論理式の概念を定義します。 \(A(x)\) を任意の原始帰納的述語とするとき、 \(\exists x.A(x)\) という論理式を\(\Sigma_1\)論理式と言い、その意味は、\(A(x)\) を成立させる自然数 \(x\) が存在するとします。 \(\forall x.A(x)\) という論理式を\(\Pi_1\)論理式と言い、その意味は、全ての自然数 \(x\) で \(A(x)\) が成立するとします。 \(\exists x.\) や \(\forall x.\) を量化子と言い、量化子を頭に付けることを量化子で変数 \(x\) を束縛すると言います。量化子が付くとその論理式は原始帰納的ではなくなります。また、量化子を含まない論理式は、\(\Sigma_1\)でもあり\(\Pi_1\)でもあると考えます。

\(\newcommand{\M}{\mathbb{M}}\)　\(\Sigma_1\)論理式や\(\Pi_1\)論理式の意味を確定させるためには、自然数の範囲を確定させる必要があります。我々が普段使っている自然数は標準モデルと呼ばれ、全ての自然数は有限です。しかし、自然数論には超準モデルと呼ばれる自然数が存在し、その中には、標準モデルの自然数のほかにも無限大の大きさの自然数がたくさん含まれています。そのため、論理式の意味を確定させるには、モデルを明示する必要があります。標準モデルを \(\N\) で表し、自然数論 \(T\) が持つ任意のモデルを \(\M\) で表すとき、標準モデルで\(\Sigma_1\)論理式が成立することを、 \(\N\vDash\exists x.A(x)\)と書き、モデル \(\M\) で成立するとき、 \(\M\vDash\exists x.A(x)\)と書きます。\(\Pi_1\)論理式に関しても同様です。今までは、標準モデルのみを考えていたので、 \(\N\vDash\) は省略して書いていたわけです。

　ちょっとした頭の体操のような補題ですが、 \(B\) を\(\Sigma_1\)論理式 \(C\) を\(\Pi_1\)論理式とするとき、以下の関係が成り立ちます。 \[ \begin{eqnarray} \N\vDash B &~\Rightarrow~& \M\vDash B \\ \M\vDash C &~\Rightarrow~& \N\vDash C \end{eqnarray}\tag{補題1} \] 　後で使いますから憶えておいてくださいね。また、ド・モルガンの法則により、 \[ \M\vDash\exists x.A(x) ~\Leftrightarrow~ \M\vDash\lnot(\forall x.\lnot A(x)) \tag{関係1} \] 　という関係が成り立ちます。

　次に、証明関数 \(p(x)\) を定義します。ゲーデル数が \(x\) である閉論理式の形式的証明のゲーデル数は \(y\) であるという最も基本的な証明述語を \(P(x,y)\) とすると、ゲーデル数が \(x\) の閉論理式が証明可能なときに \(1\) を返し、証明不能なときに \(0\) を返す \(p(x)\) は以下のように定義できます。 \[ \begin{eqnarray} p(x)=1 &~:=~& \exists y.P(x,y) \\ p(x)=0 &~:=~& \forall y.\lnot P(x,y) \end{eqnarray} \] 　\(P(x,y)\) が最も基本的とは、下記で紹介するロッサーの証明述語のような小細工はしていないという意味です。

　証明関数が定義できたので、健全性について説明しましょう。実は、健全性には２通りの健全性があります。１つ目は、\(T\) の任意のモデル \(\M\) で成り立つ健全性であり、仮に第一健全性と呼ぶことにします。 \(T\) が何らかのモデル \(\M\) を持つとき、 \(f\) を任意の閉論理式とするなら、第一健全性は以下の関係で表されます。 \[ \N\vDash p(⌈f⌉)=1 \Rightarrow \M\vDash f \] 　２つ目は、標準モデルで成り立つ健全性であり、第二健全性と呼ぶことにします。 \(T\) が標準モデル \(\N\) を持つとき、第二健全性は以下の関係で表されます。 \[ \N\vDash p(⌈f⌉)=1 \Rightarrow \N\vDash f \] 　今まで使ってきた健全性は第二健全性です。第二健全性は \(T\) が標準モデルを持つときのみ成り立ちますが、第一健全性は何らかのモデルを持ちさえすれば成り立ちます。

　次に、限定量化子を説明します。任意の原始帰納的述語 \(A(z)\) に対して、\(\forall z\lt y.A(z)\) のような論理式を限定量化子で変数を束縛された論理式と言います。その意味は、\(y\) より小さい全ての \(z\) で \(A(z)\) が成立するとします。

　次に、ロッサーの証明関数 \(r(x)\) を以下のように定義します。条件として、\(P(x,y)\) は原始帰納的であるとします。よって、\(T\) は再帰的に公理化可能でなくてはなりません。 \[ \newcommand{\trim}{\mathrm{trim}} \begin{eqnarray} P_r(x,y) &:=& P(\trim(x),y) \land \forall z\lt y.\lnot P(\trim(\ng(x)),z) \\ r(x)=1 &:=& \exists y.P_r(x,y) ~~\cdots~\Sigma_1論理式\\ r(x)=0 &:=& \forall y.\lnot P_r(x,y) ~~\cdots~\Pi_1論理式\\ &ただし、&\ng(⌈f⌉)=⌈\lnot f⌉~で、\trim(x)~は多重否定の除去 \end{eqnarray} \] 　\(P_r(x,y)\) のことをロッサーの証明述語と呼びます。多重否定の除去とは、 \(f_0\) を \(\lnot\) で始まらない閉論理式とするなら、例えば \(\trim(⌈\lnot\lnot\lnot f_0⌉)=⌈\lnot f_0⌉\) のことです。ゲーデル数の定義の方法にもよりますが、通常のゲーデル数なら、 \(\trim(x)\) や \(\ng(x)\) が原始帰納的関数にできることは明らかでしょう。よって、ロッサーの証明述語は原始帰納的な述語になります。すなわち、\(r(x)=1\) は\(\Sigma_1\)論理式となり、 \(r(x)=0\) は\(\Pi_1\)論理式となります。

　\(r(x)\) は証明関数という名前の通り、証明可能かどうかを判別できます。つまり、\(T\) が何らかのモデルを持つなら、以下の関係が成り立ちます。 \[ \N\vDash p(⌈f⌉)=1 ~\Leftrightarrow~ \N\vDash r(⌈f⌉)=1 \tag{関係2} \]

　\(p(x)\) が単純に証明を探すだけなのに対して、 \(r(x)\) はよーいドンで証明と反証を同時に探して速く見つかった方を採用します。そのため、\(\M\vDash r(⌈f⌉)=1\) と \(\M\vDash r(⌈\lnot f⌉)=1\) が同時に成り立つことはありません。パズルを解くつもりで理由を考えてみてくださいね。つまり、以下の性質が成り立ちます。 \[ \M\vDash\lnot(r(⌈f⌉)=1 \land r(⌈\lnot f⌉)=1) \tag{性質1} \] 　ただし、論理式 \(f\) は同じ意味の式でも表記が異なる式を混在させてはなりません。つまり、この性質は論理的な性質ではなく表記に対する性質です。この性質を \(r(x)\) は疑似無矛盾であると言うことにします。逆にこの性質が成り立たないときは疑似矛盾すると言うことにします。

　また、\(r(x)=0\) が\(\Pi_1\)論理式であることと(関係1)より、以下の関係が成り立ちます。 \[ \M\vDash\lnot(r(⌈f⌉)=0) ~\Leftrightarrow~ \M\vDash r(⌈f⌉)=1 \tag{関係3} \]

　次に、ロッサー文 \(R\) を以下のように定義します。条件として、\(s(x,y)\) は原始帰納的な代入関数とします。 \[ \newcommand{\Ros}{\mathrm{Ros}} \begin{eqnarray} \Ros(x) &:=& r(s(x,x))=0 \\ R &:=& \Ros(n_R) \\ &ただし、& n_R~は~\Ros(x)~の論理式番号 \end{eqnarray} \]

　このとき、ロッサー文 \(R\) は以下の関係を満たします。 \[ \M\vDash R ~\Leftrightarrow~ \M\vDash r(⌈R⌉)=0 \tag{関係4} \]

　さて、準備完了です。まずは、前提条件を満たすとき、 \(R\) が証明できないことを背理法で示します。

　条件-1：\(T\) は何らかのモデル \(\M\) を持つ。
　条件-2：\(T\) は再帰的に公理化可能である。
　条件-3：\(P(x,y)\) は原始帰納的である。
　条件-4：\(p(x)\) は第一健全性を満たす。

　仮定-1：\(\N\vDash p(⌈R⌉)=1\) つまり、\(R\) は証明できる。 \[ \begin{eqnarray} \N\vDash p(⌈R⌉)=1 ~&\Rightarrow&~ \M\vDash R ~~\cdots~第一健全性より \\ &\Leftrightarrow&~ \M\vDash r(⌈R⌉)=0 ~~\cdots~ (関係4)より \\ &\Rightarrow &~ \N\vDash r(⌈R⌉)=0 ~~\cdots~ (補題1)~r(x)=0~は\Pi_1論理式より \\ \N\vDash p(⌈R⌉)=1 ~&\Leftrightarrow&~ \N\vDash r(⌈R⌉)=1 ~~\cdots~(関係2)より \end{eqnarray} \] 　\(\N\vDash r(⌈R⌉)=0 \land r(⌈R⌉)=1\) となり矛盾する。
　よって、仮定-1が誤りである。
　したがって、\(\N\vDash p(⌈R⌉)=0\) である。
　つまり、\(R\) は証明できない。

　次に、同じ前提条件を満たすとき、 \(R\) が反証できないことを背理法で示します。

　仮定-2：\(\N\vDash p(⌈\lnot R⌉)=1\) つまり、\(R\) は反証できる。 \[ \begin{eqnarray} \N\vDash p(⌈\lnot R⌉)=1 ~&\Rightarrow&~ \M\vDash \lnot R ~~\cdots~ 第一健全性より \\ &\Leftrightarrow&~ \M\vDash \lnot(r(⌈R⌉)=0) ~~\cdots~ (関係4)より \\ &\Leftrightarrow&~ \M\vDash r(⌈R⌉)=1 ~~\cdots~ (関係3)より \\ \N\vDash p(⌈\lnot R⌉)=1 ~&\Leftrightarrow&~ \N\vDash r(⌈\lnot R⌉)=1 ~~\cdots~(関係2)より \\ &\Rightarrow &~ \M\vDash r(⌈\lnot R⌉)=1 ~~\cdots~ (補題1)~r(x)=1~は\Sigma_1論理式より \\ \end{eqnarray} \] 　\(\M\vDash r(⌈R⌉)=1 \land r(⌈\lnot R⌉)=1\) となり \(r(x)\) は疑似矛盾する。
　しかし、(性質1)より \(r(x)\) は疑似無矛盾である。
　よって、仮定-2が誤りである。
　したがって、\(\N\vDash p(⌈\lnot R⌉)=0\) である。
　つまり、\(R\) は反証できない。

　以上のことにより、ロッサー文 \(R\) は証明も反証もできないことが分かりました。つまり、自然数論 \(T\) は不完全です。ただし、不完全であることの条件が無矛盾であることではなく、何らかのモデルを持つことになっています。完全性定理を認めるなら、無矛盾ならモデルを持つことになるので、これにより、無矛盾なら不完全であることが言えます。

　実際には、不完全であることの条件として、 \(T\) が再帰的に公理化可能であることと \(P(x,y)\) が原始帰納的であること、および第一健全性も必要です。しかし、再帰的に公理化可能な理論では、原始帰納的な \(P(x,y)\) が存在することが知られており、第一健全性は証明関数が形式的証明を実現するには必要な条件なので、これにより、再帰的に公理化可能で無矛盾な自然数論は不完全であることになります。

【補足】

　注意点として、オリジナルのロッサーの定理は、超準モデル \(\M\) の存在には触れず、標準モデル \(\N\) と形式的体系 \(T\) のみを用いて証明されます。これはつまり、選択公理を必要としないということです。ここがオリジナルのロッサーの定理の重要な意義と言えます。ここでの証明には、超準モデル \(\M\) の存在証明に完全性定理を用いているので選択公理が必要です。その意味で価値は下がりますが、逆になぜ不完全になるのかはよく見えると思います。つまり私の解釈では、第一健全性と \(P(x,y)\) が原始帰納的であることが主要な要因ということがよく分かります。

　オリジナルのロッサーの定理では、第一健全性を陽には使わず\(\Sigma_1\)完全性を用いて不完全性が証明されています。一階述語論理では第一健全性は無矛盾性と等価なので陰に使われています。つまり、不完全性を証明する方法は複数あり、前提条件の選び方等により必要な性質は変化するということです。

【AIは知性を実現できるか？】

　不完全性定理によって形式的に証明できない命題がゲーデル文ですが、機械はゲーデル文が真であることを証明できないが、人間はゲーデル文が真であることを知っているので、人間と機械は同じではない。よって、人間のような AI は作ることはできないという話があるそうです。ただし、対象となる理論は健全と仮定します。

　これには色々と反論があるようですが、私も個人的には、これは構文論と意味論を意図的に混同しているのではないかと思ってます。対象となる理論が健全と仮定した場合、機械がゲーデル文を証明できないというのは構文論での話です。一方で、人間がゲーデル文を真だと知っているというのは意味論での話です。機械には構文論しか許さないのに、人間は意味論も使っていいというのは不公平ですよね。しかし、構文論の世界が意味論も含めた人間の知性の世界とどう違うのかという話題は、興味深い話題だと思いますので少し考えてみましょう。

　まず簡単に、ゲーデル文の意味論について解説しておきます。ゲーデル文は、標準モデルにおいて、この命題は形式的に証明できないという意味の命題です。そして事実、不完全性定理によってゲーデル文は形式的に証明できないのですから、標準モデルにおけるゲーデル文の真理値は真です。命題の意味を知っている人間には自明なことですよね。ただし、対象となる理論は健全と仮定しました。

　さて次に、構文論と意味論の関係について考察してみます。ここに、不完全性定理の証明が書かれた本が一冊あったとします。果たして、この本は知性を実現したものと言えるでしょうか？もし、この世界に知的存在が一人もいなかったとしたら、この本は不完全性定理の証明が書かれた本と言えるでしょうか？実際には、紙とインクの集まりでしかないのではないでしょうか。何を哲学的なことを言い出すのかと思うかもしれませんが、これは、構文論の世界である形式的体系の本質に関わる問題です。形式的体系は、意味論的な視点を一切排除してしまうと、内容の良くわからない自然数の計算ということになってしまいます。

　不完全性定理の証明が書かれた本が、不完全性定理の証明が書かれた本であるためには、それを読んで意味を解釈する知的存在がいなければなりません。それと同じで、形式的体系が何かを証明していたとしても、それを解釈する知的存在がいなければ、単なる自然数の計算に過ぎないのです。人間と機械が違うと主張する人が出てくるのも、たぶん、ここが遠因になっているのでしょう。この手の議論で機械と言えばチューリングマシンですが、数理論理学や計算可能性理論でチューリングマシンについて書かれた古典的な書籍では、チューリングマシンは比較的簡単なプログラムに従って動く、正に機械的な機械として描かれていると思います。実際には、プログラムはいくらでも高度化複雑化できるのですが、印象としては、機械自体が意味を考えるという風には感じられないのではないでしょうか？

　少し脱線すると、この話題は量子力学の観測の話と何となく似ているようにも思います。箱の中の猫は、人間が観測するまでは半分死んでいて半分生きているというあれです。形式的体系も、人間が解釈しなければ意味は定まっていないというところが似ています。

　さらに脱線すると、このページの筆者である私が人間である保証はなく、実は何等かの自然数の計算から、日本語っぽい記号列を打ち出しているだけの機械である可能性もあるわけです。そこに意味を感じるのは、最終的には読者の主観の話ということになります。ただし、ここでいう読者は複数なので、主観という表現はあまり適切ではないかもしれません。

　さて、私は AI の専門家ではありませんので、ここから先は私の空想になります。専門家から見れば的外れなことを言っているかもしれませんのでご注意ください。知性において、人間と機械は違うという主張は、現状ではそれほど外れた主張ではないでしょう。確かに、まだ機械は形式的体系の意味を理解するレベルには到達していないと思います。しかし、AI の研究は着々と進んでいますので、ひょっとすると私が生きている間に形式的体系の意味を理解する AI が登場するかもしれないと思ってます。 AI に証明とは何かをいろんな角度で質問してみたり、それこそゲーデル文の真理値について聞いてみたりして、人間と同じように答えられたら意味を理解しているとしていいと思います。つまり、あなたが納得できたら意味を理解しているとしていいと思います。もちろん、カンニングペーパーを用意しておくのは無しとして。そうなれば、不完全性定理の証明も機械によって理解され、機械の世界に閉じた形で知性が実現できるようになるのではないでしょうか。

　まあ、AI には正しいと理解できるのに、人間の方が理解できないなんてこともあるんでしょうね。その場合はどうしましょう(^^; この文章は2020年7月に書かれました。願わくば、この文章がすぐに時代遅れとなることを期待します。

【超形式的体系】

　ここでは少し上級者向けの話をします。使う記号も上級者なら既に知っているとみなして説明はしません。分からないという人は読み飛ばしてください。

　人間のようなAIを作ることは可能であると主張する人たちの中に、その理由は、形式的体系と人間の証明能力が同じであるからと説明する人たちがいます。私もたぶんそうだろうと思うのですが、その説明が不十分というか、端的に言って間違っていることがあります。某有名大学の数理論理学の先生ですら、素人向けの解説書で、その不十分な説明をしているので、その説を信じている人は相当数に上ると思われます。私のような数学の素人の指摘の方が間違っている可能性も大有りですが、ここではそのことについて述べます。

　人間のようなAIは作れないと主張する人たちは、人間はゲーデル文を真だと知っているが、形式的体系はゲーデル文を真だと証明できないので、人間と形式的体系は同じではないと指摘することがあります。

\(\newcommand{\Con}{\mathrm{Con}}\)　これに対して、人間のようなAIを作ることができるという人たちの一部はこう反論します。人間が知っているのはゲーデル文が真であることではなく、無矛盾ならばゲーデル文が真であることである。そして、無矛盾ならばゲーデル文が真であることなら形式的にも証明できる。すなわち、\(T\vdash\Con(T)\rightarrow G\) であると。ここで \(\Con(T)\) は標準モデルで理論 \(T\) の無矛盾性を表す論理式で、 \(G\) はゲーデル文です。

　しかし、この説明では不十分です。無矛盾ならゲーデル文は真であることを論理式で表すと \(\N\vDash\Con(T)\rightarrow G\) となります。このとき、\(\Con(T)\) が真なら \(G\) も真であると結論できますが、 \(T\vdash\Con(T)\rightarrow G\) で無理やり同様のことをやろうとするとこうなります。 \(\Con(T)\) が証明できるならば \(G\) も証明できると結論できる。あれ？\(G\) はゲーデル文だから証明できないはず。それ以前に、第二不完全性定理で \(\Con(T)\) は証明できないので、 \(\Con(T)\) を証明できるという仮定を置くと矛盾してしまいます。

　つまり、多くの場合 \(T\vdash\) と \(\N\vDash\) は似たようなことを表しているのですが、常に似たようなことを表しているわけではないのです。 \(T\vdash\) と \(\N\vDash\) は完全な相似形ではありません。人間が知っているのは \(\N\vDash\Con(T)\rightarrow G\) の方であり、 \(T\vdash\Con(T)\rightarrow G\) だとしても \(\N\vDash\Con(T)\rightarrow G\) と等価と考えることはできないのです。 \(\N\vDash 1+2=3\) と \(T\vdash 1+2=3\) なら等価と言えるでしょうけど。

　すると、こう反論されるかもしれません。いやいや、確かに一般の形式的体系ではそうかもしれないが、こういう場合は健全性を仮定してある。だから形式的に証明できれば十分なのだと。

　そのとおり、健全性が保証されていれば、 \(T\vdash\Con(T)\rightarrow G\) ならば \(\N\vDash\Con(T)\rightarrow G\) となります。すなわち、無矛盾ならばゲーデル文が真であることに言及できます。

　しかし、これで全て解決とはいきません。健全性を知っているのは誰でしょうか？形式的体系が知っているのでしょうか。もしそうなら、健全性を証明するためにはモデル理論の知識が必要なので、形式的体系は集合論やモデル理論の公理を含んでいなければならないはずです。しかし、入門書で紹介されるような健全性が成り立つ代表的な形式的体系である Q や PA には、そのような公理は含まれていません。つまり、通常の形式的体系は健全性を知らないのです。結局、健全性を知っているのは不完全性定理の証明を読んでいる人間ということになります。ゲーデル文の真偽に言及するには、普通は人間の手を借りているということになります。したがって、Q や PA は人間と同じではありません。

　ここまで読んだ人は、私のことを人間のようなAIは作れない論者と思ったかもしれません。いいえ、私は人間のようなAIは作れるんじゃないかと思っています。私が指摘したのは、少なくとも Q や PA は人間と同じではないということです。より大きな形式的体系を使って、集合論やモデル理論の公理を取り込み、 \(T\vdash\) や \(\N\vDash\) といった記号を取り扱える形式的体系があれば、つまり、形式的体系をさらにもう一段形式化した超形式的体系があれば、健全性を扱えるようになり、ゲーデル文の真偽も形式的に示せるのではないでしょうか。私のような半可通にはそれを示す能力はありませんけれど。

　ひょっとすると、そのような形式的体系は既にあって、専門家に言わせれば、君の言うようなことは既に証明済みだよということかもしれません。先の数理論理学の先生もそれを知っていて、素人に説明するようなことではないから、大筋だけ説明したんだよということかもしれません。そうだとすると、それを読んだ私のような半可通は誤解するよなぁ。

【補足】

　無矛盾ならゲーデル文が真であることを形式的に表した論理式 \(T\vdash\Con(T)\rightarrow G\) は正確には、 \(\N\vDash\Con(T)\rightarrow(T\vdash\Con(T)\rightarrow G)\) です。なぜかというと、\(\lnot\Con(T)\) なら \(T\vdash\Con(T)\rightarrow G\) は証明する必要のない自明な式だからです。

　また、人間が知っているのはゲーデル文が真であることではなく、その理論が無矛盾ならゲーデル文が真であることだという反論はちょっと微妙です。この反論は嘘ではありません。しかし、例えばペアノ算術に話を限定すると、ペアノ算術自身ではペアノ算術の無矛盾性は証明できないものの、それ以外の方法でペアノ算術の無矛盾性は証明可能です。そもそも、人間には意味論を使うことも認めていますしね。したがって、現代数学の正しさを信じるならばペアノ算術は無矛盾です。よって、ペアノ算術が無矛盾ならばという仮定を付けなくとも、ペアノ算術のゲーデル文は真であり、人間はそのことを知っています。つまり、人間とペアノ算術は同じではありません。

【余談】

　ところで、超形式的体系とその外側の意味論にまたがる定理とかは、超形式的体系では証明できないので、超々形式的体系が必要になります。さらにその上に超々々形式的体系があってと無限に続きそうな予感がします。機械は、どこかで形式的体系を固定しないとだめだろうと思いますが、人間なら形式化の階段をどこまでも登っていけるのでしょうか。そうだとすると人間と機械は違うのかもしれません。

　でも、人間も実際には限界があるんじゃないですかね。自然数にしたっていくらでも数えられるといいますけれど、実際には人間に数えられる自然数の大きさには限界がありますしね。

【意味論とは何か？】

　形式的体系は公理や推論規則がキッチリと定められていて、不確定な要素は無いように見えます。しかし、不完全性定理の証明は形式的体系の外に広がる意味論の世界で証明されています。形式的体系と意味論をつないでいるのは \[ p(⌈f⌉)=1~\Leftrightarrow~閉論理式~f~が形式的に証明できる \] という関係です。この \(p(⌈f⌉)=1\) が成り立つのは意味論の世界であって形式的体系ではありません。つまり、不完全性定理は意味論とは何なのかがハッキリしないと、形式的体系のようにキッチリとは理解できません。ここでは意味論の正体について、その手がかりを探ってみます。

　形式的体系は、「証明できて反証できない」「反証できて証明できない」という２つの状態以外に、「証明も反証もできない」という状態がある３値論理の世界です。つまり形式的に不完全な世界です。無矛盾性を要求しない場合は、さらに「証明も反証もできる」という状態が加わって４値論理の世界となります。まあ、意味のある体系では無矛盾性を要求しますけれど。

　これに対して意味論の世界は２値論理の世界です。つまり、真か偽の世界です。そのため、２つの世界をそのままでは同様に扱うことはできません。しかし、もし意味論の世界を形式的体系とみなすことができたならどうなるでしょう。強引に証明可能と真、反証可能と偽を同じものだとみなせば、意味論の世界では形式的完全性が成り立っているように解釈することができます。

　野崎昭弘さんの著書「不完全性定理(数学的体系のあゆみ)」には、第３不完全性定理というものが紹介されていて、無矛盾な形式的体系では自分の不完全性は証明できないのだそうです。残念ながら、間違いなく成り立つ保証はないのだそうですが、もし、第３不完全性定理が成り立つのなら、形式的体系の中では、自分は完全だと仮定して推論を進めても決して矛盾は出てこないということになります。そうでなければ、背理法で不完全であることが証明できてしまいます。つまり、自分は２値論理だと信じても矛盾しないということです。

　これらのことから、私は以下のように考えています。形式的体系の外に広がる意味論の世界も、実は形式的体系であって、２値論理であるかのように見えるのは、第３不完全性定理のおかげではないのかと。それにしても、不完全性のおかげで自分が完全であるように見えるというのは、なんとも逆説的ですね。

【真の算術と選択公理】

　こちらのセクションでは、完全な自然数論として真の算術があることを紹介しました。真の算術は標準モデルで正しい閉論理式を全て公理にした理論です。真の算術を作るには、ゲーデル数を \(z=0,1,2,3,\cdots\) とカウントアップし、それを \(t(z)=1\) で判定して真になったものを大きさ順に並べれば OK です。ただし、\(z\) が閉論理式のゲーデル数でない場合は \(t(z)=0\) とするとします。列挙されたゲーデル数に対応する閉論理式が真の算術の公理になります。判定に合格した順に番号を振れば、真の算術の公理の集合と自然数の集合 \(\N\) との間に１対１対応があることになります。

　しかし、\(t(z)\) は自然数論を使っては書けませんでした。何か超越的な方法を用いないと定義できず、具体的に構成することはできないということです。具体的に構成することができないものが存在していると言えるのでしょうか？つまり、本当に真の算術の公理を1番目、2番目、3番目と列挙することが可能なのでしょうか？もっと言うと、真の算術の公理の集合と \(\N\) との間に１対１対応はあるのでしょうか？そう、こういう時はあの有名な選択公理の出番ですね。

　まず、真の算術の公理の集合とその公理のゲーデル数の集合を同一視して TA と書きます。すると TA は \(\N\) の部分集合になっていますから、 TA の濃度は可算無限以下であることは確かです。また、標準モデルで正しい閉論理式は、\(0=0,1=1,2=2,3=3,\cdots\) のように無数にありますから、TA は有限集合ではありません。ここで選択公理を仮定すると、最も小さい無限集合の濃度は可算無限になりますので、 TA の濃度は可算無限以上可算無限以下となり、結局、可算無限ということになります。つまり、TA と \(\N\) との間に１対１対応があるということです。

　したがって、具体的に構成することはできませんが、選択公理を使うと、真の算術の公理を1番目、2番目、3番目と列挙することができるということになります。つまり、真の算術の存在は選択公理を仮定すれば保証できることになります。

　具体的に構成できないのに存在はしていると言われても納得しがたいですよね。そこで、以下のように考えてみてはどうでしょうか？コイントスを使って自然数の数列を生成することを考えます。つまり、コイントスを繰り返して、 \(n+1\) 回目に表が出れば数列に \(n\) が含まれるとします。コイントスを無限に繰り返せば、\(\N\) の部分集合が生成できます。コイントスが真の乱数なら、典型的なケースにおいて、数列の \(m\) 番目にどの自然数 \(n\) が対応するのかを決定するアルゴリズムはありません。つまりこの数列は、乱数を含まない純粋な自然数論を使って具体的に構成する方法はありません。一方で真の乱数なら、コイントスの全ての可能性の中に TA を生成する場合があるはずです。コイントスで表が出た回数 \(m\) を数えておけば、この数列に番号を振ることが可能です。したがって、TA と \(\N\) との間には１対１対応があると考えられます。

【超準モデルと数学的帰納法】

　こんなことが気になっている人いませんか？超準モデルには無限大の自然数があるのに、数学的帰納法が使える。でも、数学的帰納法が使えるためには、全ての自然数が、0 からスタートして 1 を足す操作でつながってないとダメなのでは？ 1 をいくら足しても無限大にはならないじゃないか。

　私は長いことこの疑問に悩んでいました。最近、何とか納得できる解釈を思いついたので、ここに書いておくことにします。

　まず、帰納法が使えるためには、自然数論の公理系に帰納法の公理図式が含まれていれば大丈夫です。ここが私のつまずいていた所です。そう、必ずしも全ての自然数が、 0 からスタートして 1 を足すでつながっている必要はないのです。通常の自然数論であるペアノ算術は帰納法の公理図式を含みます。そして、不完全性定理により、ペアノ算術は不完全なので、無限大の数を持つ超準モデルが存在することになります。つまり、超準モデルで帰納法が使えることは不完全性定理によって保証されるのです。

　そして、超準モデルで帰納法が使えると、無限大は実際には有限の数とはつながっていないにもかかわらず、あたかも有限と無限がつながっているかのようなファンタジーが提供されることになります。私が超準モデルにおける帰納法を長いこと理解できなかったのは、このファンタジーをどう解釈したらよいのか分からなかったからです。

\(\newcommand{\sum}{\mathrm{sum}}\)　例えば、有限和と無限和について考えてみましょう。標準モデルで、次のような有限和の関数 \(\sum(x)\) を考えます。 \[ \sum(x) = \left\{ \begin{array}{cl} 0 & (~x = 0~) \\ \sum(x - 1) + 1 & (~x \ge 1~) \end{array} \right. \] 　帰納法を適用すると、\(\sum(0) = 0\) かつ \(\forall x.(\sum(x)=x~\Rightarrow~\sum(x+1)=x+1)\) が成り立ちますので、\(\forall x.(\sum(x)=x)\) となります。これはつまり、\(\sum(2)=1+1\) であり、 \(\sum(3)=1+1+1\) であるということです。すなわち、\(\sum(n)\) は \(n\) 個の 1 の和になります。

　ここで、同じことを超準モデルで繰り返すと、 \(\sum(n)\) の \(n\) は無限大でもかまわないということになります。要するに、\(H\) が無限大の数のとき、現実には \(1\) を \(H\) 個足すことなどできないのに、 \(\sum(H)=H\) という等式が成り立ちます。よって、有限和の自然な延長で考えると、\(n\) が無限大の数の場合、仮想的に \(\sum(n)\) は無限個の 1 の和であると考えることができるということです。これがファンタジーです。

　厳密には、標準モデルの \(\sum(n)\) と超準モデルの \(\sum(n)\) は全く原理の異なる関数なので、同じとみなすのは乱暴です。事実、標準モデルの \(\sum(n)\) は具体的な実体としての 1 の和に書き下すことが可能ですが、超準モデルの \(\sum(n)\) には \(n\) が無限大の場合そのような実体は存在しません。つまり、計算の過程を無視して結果だけ見れば、形式的にというか仮想的に無限個足しているかのように見えているだけです。少なくとも再帰的な足し算では無限和は計算できません。強引に足し算とみなすのなら、選択公理のような何か超越的な足し算と考えるしかないでしょう。

　帰納法は、標準モデルで成り立つ有限な関係が、超準モデルでは無限の関係に自然に延長されることを保証します。つまり、標準モデルの有限な直観を使って無限の関係を解釈できるようになるのです。例えば、\(n\) が無限大のとき、\(\sum(n)=1+1+\cdots+1+1\) のように「\(\cdots\)」を使って解釈できます。それでも、実際には有限と無限は +1 の連鎖ではつながっておらず、あくまで計算の結果だけが無限に繰り返したかのように定まっているだけです。

【正直者のパラドクス】

　ここでは、嘘つきのパラドクスと対をなす、もう一つのパラドクスを紹介します。嘘つきのパラドクスは有名ですよね。「私は嘘つきです」という文は真と考えても偽と考えても矛盾するため真とも偽とも言えません。このパラドクスの原因は否定的自己言及にあると言われています。しかし、実際には否定的でない自己言及も病的な文となることがあります。それが正直者のパラドクスです。

　正直者のパラドクスは「私は正直者です」という文の真理値を考えると起こります。この言葉を発した者が事実正直者であれば、この文は正しいことになり何の矛盾もありません。しかし、この言葉を発した者が嘘つきだと仮定しても、嘘つきが正直に自分を嘘つきだと言うはずがありませんので、嘘つきが自分のことを正直者と嘘をつくことに何の矛盾もありません。つまり、この文は真と解釈しても偽と解釈しても矛盾せず、この文だけでは嘘つきのパラドクス同様に真とも偽とも言えないわけです。

　ところで、嘘つきのパラドクスは本当はパラドクスではないことをご存じでしょうか？嘘つきのパラドクスが想定している世界、すなわち、完全な正直者か完全な嘘つきしか存在しない世界には、「私は嘘つきです」という状況は存在しません。当たり前ですよね。正直者は自分のことを嘘つきと言うはずがないし、嘘つきも自分のことを嘘つきと言うはずがありません。この世界には完全な正直者と完全な嘘つきしかいないので、誰かが「私は嘘つきです」と発言する状況は決して起きません。つまり、真偽を判断するも何も、そもそも「私は嘘つきです」という状況は存在しないのです。存在しないものが矛盾していたとしても何も不思議ではありませんね。

　そして、完全な正直者と完全な嘘つきしかいないような不自然な世界ではなく、正直者でも嘘つきでもない人もいる通常の世界を考えても、嘘つきのパラドクスは存在しません。嘘つきのパラドクスを少し修正して、「私は正直者ではない」という文の真理値を考えてみましょう。正直者が自分を正直でないと言うことはないので、事実、この文は真です。嘘つきが自分を正直でないと言うこともないので、この「私」は、正直者でも嘘つきでもありません。つまり、この「私」が発言者であると仮定すれば、「私は嘘つきです」も「私は正直者です」も偽であり、「私は不完全な嘘つき（or 正直者）です」が真となり矛盾は存在しません。この「私」は嘘をつくことも正直に話すこともできますからね。

　一方、正直者のパラドクスは多少厄介です。完全な正直者と完全な嘘つきしかいない世界においても、「私は正直者です」という状況は存在します。したがって、その真理値を考えることは無意味ではありません。しかし、正直者であると同時に嘘つきであるはずはないので、真実はどちらかひとつです。ですが、それは判定できません。私はこれが不完全性定理の一種ではないかと思っています。

　どこで読んだか忘れてしまいましたが、この状況を解決するうまい方法が紹介されていました。それは、「あなたはカエルか？」と聞いてみることです。正直者はもちろんカエルではないと答えるし、嘘つきはカエルですと答えます。これでめでたく正直者か嘘つきか判定できるわけです。

　この方法のミソは、カエルかどうかは外見で判断できるということです。正直者かどうかが自己申告であるのに対して、カエルかどうかは第三者による判定が可能なのです。これは、第二不完全性定理の状況とよく似ています。第二不完全性定理を大雑把に説明すると、自らの無矛盾性は自分では証明できないというものです。つまり構造的には、自分が正直者であることは自分では証明できないということと同じです。しかし、無矛盾性を証明する手段が何もないかというとそうではありません。自分でなければ、つまり他人の手を借りれば無矛盾性は証明可能です。カエルを使えば正直者かどうか判断できることとよく似ていますね。

　さて、最後にさらに話をややこしくしましょう。嘘つきは魔法が使えてカエルに化けることができるという公理を追加（厳密には上書き）します。すると、先ほどの「あなたはカエルか？」という質問が通用しなくなります。カエルに化けた嘘つきが「私はカエルです」と言えば、第三者には嘘をついていることは分かりません。これは、公理を追加することで外見を偽ることが可能になり、外見が自己申告化されてしまったということです。

　正直者のパラドクスと不完全性定理の関係について、もう少し突っ込んだ解説を読みたい人は日常言語による証明をご覧ください。

【追記】

　いろいろ調べてみると、真の嘘つきのパラドクスというものがあるようです。それはこんな感じです「この発言は嘘である」。このパラドクスは、完全な正直者と完全な嘘つきしかいない世界では起きませんが、日常の世界では問題となります。

　この問題を解消するには、この世には嘘でも本当でもないことが存在すると認めるのが簡単そうです。嘘でも本当でもないことが存在する世界とはいわゆる３値論理の世界です。真・偽のほかにも例えば無意味という真理値がある世界です。まあ、確かに日常の世界は３値論理のような気もしますね。

【第二不完全性定理】

　ここでは、第二不完全性定理を私が独自に解釈した方法で証明します。つまり、健全で再帰的に公理化可能な理論 \(T\) では、論理的な飛躍を避け、証明するという行為が人間に計算可能であるように定義すると、自らの無矛盾性は証明できないことを証明します。

　従来の方法では可導性条件という条件を設定し、対象となる理論が無矛盾という仮定で証明するのですが、ここでは独自の条件を設定して対象となる理論が健全という仮定で証明します。健全とは、証明できる命題は真であるということです。なんだか当たり前のことのようですが、結構重要な意味を持つ条件です。また、健全性は無矛盾性より強い条件なので、健全なら無矛盾になります。

　そのほか、第一不完全性定理を部分的に参照するので、対象となる理論 \(T\) は再帰的に公理化可能であるものとします。再帰的に公理化可能とは大雑把に言って、その理論の証明が有限な方法で行えるということです。また、対象となる理論は自然数論に限定します。自然数論の中で証明を行うには、証明という行為を自然数の計算で表現する必要があります。つまり、証明が有限な方法で行えるということは、証明が自然数の有限な計算に翻訳できるということです。

　それでは証明を始めましょう。第二不完全性定理の証明は、以下で説明する証明関数にいくつかの条件を設定することで行います。まず、\(p(x)\) を不完全性定理の対象となる理論 \(T\) の証明関数とします。証明関数とは、 \(x\) が理論 \(T\) で証明可能な閉論理式のゲーデル数のとき \(1\) を返し、 \(x\) が理論 \(T\) で証明不能な閉論理式のゲーデル数のとき \(0\) を返す関数のことです。 \[ p(x)= \begin{cases} 1 & (x~が証明可能な閉論理式のゲーデル数) \\ 0 & (x~が証明不能な閉論理式のゲーデル数) \end{cases} \] 　閉論理式とは大雑把に言って真偽の定まった論理式のことです。論理式とは真か偽かを問える命題を数式に翻訳したものです。例えば、\(1=0\) は真理値が偽の閉論理式です。ゲーデル数とは論理式に振られた番号のことで、 UTF-8 や Shift_JIS のような文字コードを想像してもらうと分かりやすいと思います。自然数論では自然数しか扱えませんので、論理式も自然数を割り当てて表現します。

　この時、第二不完全性定理を成立させる証明関数は以下の条件を満たすとします。ごちゃごちゃしていますが、ひとつひとつ理由を説明するので我慢して読み進めてみてください。 \[ \begin{array}{lrcl} (条件1) & p(a)=1 & \Rightarrow & p(⌈p(a)=1⌉)=1 \\ (条件2) & p(\ng(a))=p(\ng(b))=1 & \Rightarrow & p(a)=p(b) \\ (条件3) & p(a)=p(\ng(a)) & \Rightarrow & p(a)=p(⌈1=0⌉) \\ (条件4) & p(a)=p(b)=0 & \Rightarrow & p(⌈p(a)=0⌉)=p(⌈p(b)=0⌉) \end{array} \] 　ここで、\(p(x)=1\) は\(\Sigma_1\)論理式であることとします。 \(\Sigma_1\)とは人間に計算可能であることを意味します。人間の能力を超える計算能力を想定すると、不完全性定理は必ずしも成り立ちません。また、\(a, b\) は任意の閉論理式のゲーデル数です。さらに、\(\ng(x)\) は \(\ng(⌈f⌉)=⌈\lnot f⌉\) という関係を満たす関数のことです。ただし、\(f\) は任意の閉論理式で、\(⌈f⌉\) は \(f\) のゲーデル数を表します。例えば、\(⌈p(a)=1⌉\) は閉論理式 \(p(a)=1\) のゲーデル数です。あるいは、\(⌈1=0⌉\) は閉論理式 \(1=0\) のゲーデル数です。 \(\lnot\) は否定を表す記号です。「\(\lnot A\)」は「\(A\) でない」の意味になります。

　それぞれの条件を説明すると、(条件1) は\(\Sigma_1\)完全性のことです。 \(\Sigma_1\)完全性とは、証明できる閉論理式は証明できることも証明できるという性質です。 \(p(x)=1\) が\(\Sigma_1\)論理式である必要があるのは、この (条件1) のせいです。この条件は、第一不完全性定理を部分的に参照しています。つまり、無矛盾ならゲーデル文が証明できないことを保証するのに必要です。ゲーデル文については後ほど説明します。また、証明関数が人間に計算可能であることも要求します。

　(条件2)(条件3) は矛盾の意味を一意にするために必要です。つまり、理論 \(T\) が矛盾すると全ての閉論理式が \(p(x)\) で証明可能になることを保証します。理論 \(T\) が矛盾するとは、ある論理式 \(A\) が証明可能かつ \(\lnot A\) も証明可能なことですが、通常、\(p(⌈1=0⌉)=1\) や後に示す \(p(⌈G(g)⌉)=1\) という論理式は矛盾を表しています。しかし、\(p(x)\) の定義の仕方によっては、これらの論理式は必ずしも論理的に同値になりません。 (条件2)(条件3) はこれらの論理式の意味を同値にするために必要です。

　(条件2)(条件3) に納得するには、矛盾する場合は各条件が混ざりあってしまって分かりにくくなるので、対偶を考えて、証明できない閉論理式が存在すれば無矛盾になること確認すれば OK です。

　(条件4) は \(p(x)\) に論理的飛躍が無いことを保証するのに必要です。つまり、ロッサーの証明述語のような論理的飛躍のある述語を避けるために必要です。証明するという行為を余計な工夫をせず素直に実装するとこの条件は満たされます。つまり、ひたすら愚直に全ての定理を探索するように証明関数を実装すれば、この条件は満たされます。反証できるときは証明できないと解釈するというような余計な工夫をすると、この条件は成り立ちません。この条件が成り立つと、無矛盾性とゲーデル文の同値性が形式的にも成り立つようになります。ここで、形式的に同値とは、証明できるかできないかで同値であることを指します。また、論理的に同値とは、正しいか正しくないかで同値であることを指します。

　(条件1～4) を満たす証明関数が存在することは簡単に確認できます。例えば、ゲーデルさんが定義した \(p(x)=1\) は、(条件1～4) の全てを満たします。

　次に、無矛盾性の表現方法を定めます。 (条件2)(条件3) により、矛盾の意味はひとつしかないので、無矛盾性を表す論理式も全て論理的に同値になります。したがって無矛盾性を \(p(⌈1=0⌉)=0\) というひとつの論理式で表すことができます。よって、これ以降、理論 \(T\) の無矛盾性のことを \(p(⌈1=0⌉)=0\) で表します。

　次に、無矛盾性とゲーデル文が論理的に同値であることを示します。 \(G(x):=p(s(x,x))=0\) と定義して、\(G(x)\) の論理式番号を \(g\) とするとき、 \(G(g)\) をゲーデル文と呼ぶことにします。論理式番号とは全ての１変数論理式に振られた番号のことです。 \(s(x,y)\) は代入関数であり、 \(s(g,n)=⌈G(n)⌉\) と定義されています。つまり、論理式番号に対応する論理式に自然数 \(n\) を代入してそのゲーデル数を返します。すると、\(G(g)\Leftrightarrow p(⌈G(g)⌉)=0\) が成り立ち、 \(\lnot G(g)\) は \(p(⌈G(g)⌉)=1\) で表されます。

　ここで、\(n_G=⌈G(g)⌉\) と定義すると (条件1) から、 \[ \begin{eqnarray} p(n_G)=1 & ~\Rightarrow~ & p(⌈p(n_G)=1⌉)=1 \\ & ~\Leftrightarrow~ & p(\ng(n_G))=1 \end{eqnarray} \] 　となります。そして、\(n_G=⌈G(g)⌉\) ですから、 \[ p(⌈G(g)⌉)=1~\Rightarrow~p(⌈\lnot G(g)⌉)=1 \] 　と書き換えられます。したがって、\(p(⌈G(g)⌉)=1\) ならば理論 \(T\) が矛盾します。よって、対偶をとれば、無矛盾なら \(p(⌈G(g)⌉)=0\) となります。つまり、 \[ p(⌈1=0⌉)=0~\Rightarrow~p(⌈G(g)⌉)=0 \] 　が成り立ちます。一方、(条件2)(条件3) を満たせば、矛盾すると全ての閉論理式が証明可能になるので、その対偶をとると、証明できない論理式が存在すれば無矛盾ということになります。したがって、 \[ p(⌈G(g)⌉)=0~\Rightarrow~p(⌈1=0⌉)=0 \] 　が成り立ちます。よって、二つを合わせると、 \[ p(⌈1=0⌉)=0~\Leftrightarrow~p(⌈G(g)⌉)=0 \] 　が成り立ちます。そして、\(G(g)\Leftrightarrow p(⌈G(g)⌉)=0\) なので、これにより、無矛盾性とゲーデル文が論理的に同値であることが示されました。

　最後に、理論 \(T\) が健全なら、その無矛盾性は、理論 \(T\) では証明も反証もできないことを示しましょう。健全なら無矛盾なので、無矛盾ならば \(p(⌈1=0⌉)=0\) は正しく、したがって、無矛盾性と論理的に同値である \(p(⌈G(g)⌉)=0\) も正しいので、 \[ p(⌈1=0⌉)=p(⌈G(g)⌉)=0 \] 　が成り立ちます。ここで、\(n_{10}=⌈1=0⌉\) と定義し、\(n_G=⌈G(g)⌉\) であることを使えば上式は、 \[ p(n_{10})=p(n_G)=0 \] 　となります。また、\(p(⌈G(g)⌉)=0\) の中の \(G(g)\) を \(p(n_G)=0\) に展開してやれば、 \(p(⌈p(n_G)=0⌉)=0\) が成り立ちます。そこで、(条件4) を使えば、\(p(⌈p(n_{10})=0⌉)=0\) が導かれます。要するに、\(p(n_{10})=0\) は \(p(x)\) では証明できません。よって、\(p(⌈1=0⌉)=0\) は理論 \(T\) では証明できません。つまり、無矛盾性は証明できません。すなわち、\(p(⌈1=0⌉)=0\) と \(p(⌈G(g)⌉)=0\) は形式的にも同値です。

　一方、\(p(⌈1=0⌉)=1\) が理論 \(T\) で証明できると、健全性より \(p(⌈1=0⌉)=1\) が正しくなります。これは無矛盾性 \(p(⌈1=0⌉)=0\) と矛盾しますので、 \(p(⌈1=0⌉)=1\) も理論 \(T\) では証明できません。すなわち、\(p(⌈1=0⌉)=0\) は反証できません。つまり、無矛盾性は反証できません。

　以上により、理論 \(T\) が健全で再帰的に公理化可能である時、その証明関数 \(p(x)\) が (条件1～4) を満たすならば、 \(\Sigma_1\)論理式で定義された \(p(x)=1\) では、無矛盾性は証明も反証もできないことが示されました。

【互換性による第二不完全性定理】

　上記の証明では、対象となる理論が健全であることを仮定していました。これを無矛盾にま弱めることはできないでしょうか？実は、 (条件1)(条件4) を互換性のある証明関数を使って書き直せば弱めることが可能です。 \[ \begin{array}{lrcl} (条件1') & p(a)=1 & \Rightarrow & p(⌈p_c(a)=1⌉)=1 \\ (条件4') & p(a)=p(b)=0 & \Rightarrow & p(⌈p_c(a)=0⌉)=p(⌈p_c(b)=0⌉) \end{array} \] 　\(p_c(x)\) は以下ので説明している互換性のある証明関数です。さらに、\(G(x):=p_c(s(x,x))=0\) と定義して、ゲーデル文を修正ゲーデル文にすることで、対象となる理論が無矛盾という仮定で第二不完全性定理が証明可能になります。ただし、 \(G(g)\Leftrightarrow p(⌈G(g)⌉)=0\) という関係が \(G(g)\Leftrightarrow p_c(⌈G(g)⌉)=0\) という関係になるので、多少、読み替えをしてやる必要はあります。

【あとがき】

　さて皆さん、不完全性定理のすごく簡単な説明はお楽しみいただけましたか？不完全性定理が分かった気になれなかった人に、少しでも分かった気になってもらえたのなら、私の企みは成功と言えます。成功してるといいなぁ(^^;

　ここでは、私が不完全性定理を勉強してみて感じたことを書こうと思います。

　まず、ある程度第一不完全性定理を理解して思ったのは、知の革命とか理性の限界とか言うのはちょっと大げさすぎると言うことです。第一不完全性定理は、ゲーデルさんのような天才でなければ思いつかない超難問というより、証明するとはどういうことかを丁寧に整理していけば、いずれは誰かがたどり着く必然的な内容のように思えるからです。

　言っていることは、ある公理系 \(T\) にはそれを解釈するモデルが複数あることがあり、ある種の論理式はモデルを指定しないと真偽が定まらないということです。つまり、モデルによって真になったり偽になったりする論理式は、全てのモデルに共通の性質を定めた公理からは証明できるはずがない。むしろ証明できたらおかしいというだけなんですね。

　私は情報工学科卒なので、数学科のカリキュラムは知りませんが、多分、第一不完全性定理は、数学科では最初の方で習う初等的な定理なのではないでしょうか？

　ひょっとしたら、ゲーデルさんが証明した時代においては、一級の数学者たちも、証明とは何かを整理しきれておらず、知の革命だったのかもしれません。現代日本に住んでいると民主主義なんて当たり前と思えますが、絶対王政を打倒した当時の西洋の人々には、正に精神的にも革命だったように。ただ、そういう歴史的文脈から外れて、知の革命とか理性の限界と語るのは、やはり大げさすぎるという印象です。

　また、第二不完全性定理の数学は数学自身の無矛盾性を証明できないという宣伝も、言葉を補わないと誤解を招くと思います。実際には、ある種の条件を満たす理論や証明関数において、形式的に証明できないということであって、形式的でない有限の立場やその拡張で証明できないとされたわけではありません。事実、不完全性定理の後に、ゲンツェンさんが有限の立場を拡張して、自然数論の無矛盾性を証明しています。

　一方で、数学自身で数学の無矛盾性が証明できたとしても、それは「私は嘘は申しません」という人を信用できるかと言うことであって、不完全性定理を持ち出すまでもなく、常識としてそんな主張は無意味です。まさに正直者のパラドクスになっています。数学の無矛盾性の保証は、あくまで現実への有益な応用を通じて保証されるもので、他者からの評判で判断するしかないわけです。そうだとすると、不完全性定理で無矛盾性の証明ができないとされたことは、数学にとって特に打撃というわけではないでしょう。実際、数学は有益な応用を多数持つわけですから。また、有限の立場とは、信用できると評判の定まった立場とも言えるかもしれません。

　問題として残るのは、現実への応用を持たない、数学のための数学みたいな分野の無矛盾性をどう保証するかなのでしょうね。

　何やら偉そうに知った風なことを書いてしまいましたが、私の感想が真実を言い当てているかどうかは、皆さんが不完全性定理を理解することでご判断ください。このページがそのきっかけになれば幸いです。