第二不完全性定理の証明の素案

【section1】

　このページの証明は、思いついたアイディアを次から次へと放り込んだため、 非常に見通しが悪くぐつぐつとしたごった煮のような証明になっています。 しかしそうしたごった煮も、より深く理解するためには有用かもしれないと思ったので、 このページに残しておくこととしました。 興味のある人は解読に挑戦してみてくださいね。

　ここでは、私が独自に解釈した第二不完全性定理を説明します。 それは、再帰的に公理化可能で無矛盾なペアノ算術の拡大理論 \(T\) の最も基本的な証明関数 \(p(x)\) を用いた無矛盾性を表す論理式 \(p(|1=0|)=0\) は、 ペアノ算術では形式的に証明も反証もできない。 もしくは、\(p(x)\) は無矛盾性を表現し得ないというものになります。

　つまり、\(T\) で矛盾 \(1=0\) が証明できないという論理式は、 \(T\) が無矛盾なら正しいが、 そのことはペアノ算術では形式的に証明することはできない。あるいは、 無矛盾性それ自身を形式的には表現し得ないので証明できないというものになります。

　私が独自に思いつた証明なので、間違っている可能性も大いにあります。 参考にする人は自分で検証してくださいね。 各種記号の意味等については こちらのページ を参照してください。

【section2】

　それでは証明を始めましょう。まず、証明関数の定義から確認します。 証明関数 \(p(x)\) は、 ゲーデル数が \(x\) の閉論理式の形式的証明のゲーデル数は \(y\) であるという原始帰納的述語 \(P(x,y)\) を用いて以下のように定義できます。

　\(P(x,y)\) を証明述語と言います。 ここで、\(P(x,y)\) が最も基本的な証明述語とすると、 ゲーデル数が \(x\) の閉論理式が形式的に証明可能であるなら \(p(x)=1\) であり、有限な \(y\) で計算終了します。 しかし、形式的に証明不能ならば \(p(x)=0\) であり、 \(y\) の取り得る範囲は全ての自然数ということになります。 つまり、\(y\) の探索範囲は有限にはなりません。

　証明関数がこの形になることは第一不完全性定理から導かれます。つまり \(p(x)\) は、任意の閉論理式が有限時間で証明あるいは反証できると決定可能ではありません。 \(p(x)\) が決定可能になるには、 証明能力を有限な範囲(例えば原始帰納的)に制限しても完全である必要があります。 完全なら証明能力は制限された範囲で足りていることになります。 しかし、実際には不完全なので、 有限という制限を外して全能力を使う必要があります。 要するに、有限な範囲では証明能力はぜんぜん足りていない可能性が高いので、 制限を加えるわけにはいかないということです。 よって、上記の条件を満たす理論 \(T\) の証明関数は決定可能にはできません。

　これは、証明できないことの確認、つまり \(p(x)=0\) と確認することが、 いわゆる悪魔の証明になっていて、\(\forall y.\lnot P(x,y)\) の \(y\) の探索範囲が自然数全体にならざるを得ないということです。 すなわち \(p(x)=0\) の基本的な形は自然数全体に対する全探索であり、 特定の条件下で探索を途中で打ち切る（ショートカットする）ような仕組みはオプションだということです。

　このように、証明できないことの確認が自然数全体に対する全探索であることを、 定理でない閉論理式の集合は再帰的可算ではないと言います。 後で使いますから憶えておいてくださいね。

　実は、探索範囲を有限に制限しても、つまり探索をショートカットしても、 偶然、\(p(x)\) の結果は変わらないということも有り得ます。 例えば、偶然、帰納法が通ってしまったなどです。証明関数が扱うゲーデル数は、 純粋に論理的な存在ではなく必ず自然数としての側面が付きまとうので、 そういうことも有り得ます。

　しかし、無矛盾性を証明するような場合、 そのような \(p(x)\) で計算した結果には、何等かの論理的な飛躍があります。 つまり、ショートカットのある \(p(x)\) という隠れた情報を無矛盾性の証明に用いています。 この情報を隠して結果に言及するなら、それは論理的な飛躍です。 かと言って、ショートカットという情報に依存するのは適切ではありません。 本当の無矛盾性は公理系と推論規則のみに依存して決まるからです。 偶発的な帰納法によるショートカットという概念には依存しません。 なので以下の証明では、ショートカットのある \(p(x)\) は除外していくこととします。

　また、ペアノ算術の中に \(p(c)=0\) に相当する公理があれば、 一部の閉論理式に対して論理的な飛躍無しに探索範囲を有限にすることができますが、 \(p(x)\) はペアノ算術の拡大理論の証明関数なので、 ペアノ算術の公理系が完成する前に \(p(x)\) を決めることはできません。 ペアノ算術は再帰的に公理化可能でなければならないからです。よって、 ペアノ算術の公理系に \(p(c)=0\) に相当する公理が含まれることもありません。 ただし、\(c\) は証明も反証もできない閉論理式のゲーデル数とします。

【section3】

　ここで注意しなければいけないのは、 \(P(x,y)\) が最も基本的な証明述語ではない場合です。 ロッサーさんが定義した証明述語を用いた場合、 ゲーデル数が \(x\) の閉論理式が反証できるときは、 有限な \(y\) で証明不能と判定できるショートカットがあります。 これは、証明関数に以下の仮の無矛盾性が組み込まれていることに相当します。

　そのため、 クライゼルの注意 と呼ばれる現象が起きて、\(p(|1=0|)=0\) が形式的に証明可能になります。 無矛盾性が組み込まれているのですから、無矛盾性が証明可能なのは半ば当然です。 つまり、無矛盾と仮定したのだから無矛盾ということです。身もふたもありませんね。 当然、クライゼルの注意は本当の無矛盾性の証明として適切とは言えません。

　本当の無矛盾性は公理系と推論規則のみに依存して決まります。 つまり、証明関数の形に細工をすれば証明できるようなものではなく、 本来の形式的証明の手順からその成否を判断できねばなりません。 そこでまず、本来の形式的証明の手順を忠実に実装し、 余計なことは実装していない最も基本的な証明関数は、 クライゼルの注意のような現象を起こす証明関数にならないことを確認します。

　クライゼルの注意を起こすような証明関数 \(p(x)\) には、 仮の無矛盾性をショートカットとして組み込む必要があります。 しかし、ショートカットを組み込んだ場合、 証明関数を構成する証明述語 \(P(x,y)\) が、 より基本的な証明述語に分解できることになります。 本来の機能である証明可能かどうかの判定以外に、 反証可能かどうか等を判定できないといけないからです。 これは証明関数が最も基本的であることに反します。 よって、最も基本的な証明関数にはショートカットは存在せず、 クライゼルの注意のような現象は起きません。

　問題は、ショートカットの存在しない証明関数を作れるかどうかです。 もし作れないのなら、\(p(x)\) は本当の無矛盾性を表現し得ず、 適切な無矛盾性の形式的証明はできないということになり、 証明は終わりです。つまり、\(T\) の無矛盾性は形式的には証明も反証もできません。 なので以下では、\(p(x)\) にショートカットは存在しないと仮定します。 実は、\(p(x)=1\) が可導性条件という条件を満たせば、 ショートカットは存在しないことが分かっています。 ゲーデルさんが作った可証性述語は、その条件を満たします。

【section4】

　次に、最も基本的な証明関数による無矛盾性を表す論理式 \(p(|1=0|)=0\) は、 ペアノ算術では形式的に証明できないことを確認します。

　\(p(|1=0|)=0\) を証明述語を使って表せば \(\forall y.\lnot P(|1=0|,y)\) となります。 \(1=0\) は矛盾なので、理論 \(T\) が無矛盾なら形式的に証明できません。 そして、\(p(x)\) は決定可能ではなく、 ショートカットは組み込まれていないので、\(\forall y.\lnot P(|1=0|,y)\) は全ての可能な形式的証明のゲーデル数 \(y\) を調べて、 \(1=0\) の証明になっていないことを確認することになります。 形式的証明のゲーデル数は、 対象となる理論の定理１つ１つと対応しています(多対一の関係)。 したがって、\(p(|1=0|)=0\) はその理論の定理全体に言及することになります。

　そして、 \(T\) の定理全体（すなわちペアノ算術の定理全体を含む）に言及する論理式は、 ペアノ算術においてはまだ意味が確定していません。 ペアノ算術の中ではペアノ算術の定理の集合を作っている最中であり、 \(T\) の定理全体という概念はまだ存在していないからです。 そのため、ペアノ算術の中では \(p(|1=0|)=0\) を証明することはできません。

　もし証明できたとすると、 形式的証明の仕組みから、ペアノ算術の有限個の定理に言及することで、 \(p(|1=0|)=0\) の意味が確定することになります。形式的証明では、 公理を除くあらゆる定理は、 それより基本的な有限個の定理に言及することで証明されるからです。 しかし、\(p(|1=0|)=0\) の意味を確定するのに必要な \(T\) の定理全体は有限個ではないのでこれは矛盾です。

　厳密にこれを言うには、\(p(x)\) にショートカットが組み込まれておらず、 \(T\) の定理ではない閉論理式の集合が再帰的可算ではないことが必要です。

　つまり、\(1=0\) が定理でないことの有限的な特徴が存在するということは、 証明できない閉論理式が存在するということなので、 \(T\) が無矛盾であると仮定してしまうことと同値です。 よって、\(p(x)\) にショートカットが存在することになります。しかし、 ショートカットは存在しないと仮定したので、定理でないことを有限的に判定するには、 定理であることの有限個の特徴全てに該当しないことを調べるほかありません。 すると、何らかの閉論理式がどれか一つでも定理でないと有限的に判定できるならば、 全ての定理でない閉論理式を定理でないと有限的に判定できることになります。 これは定理でない閉論理式の集合が再帰的可算でないことに反することになります。

　どうにかして有限個の定理で無矛盾性を証明するためには、 \(p(|1=0|)=0\) 相当の論理式を公理にするほかありませんが、 \(p(x)\) はペアノ算術の拡大理論の証明関数なので、 \(p(|1=0|)=0\) 相当の論理式をペアノ算術の公理とすることはできません。

　まとめると、\(p(x)\) が再帰的に公理化可能で無矛盾なペアノ算術の拡大理論 \(T\) における最も基本的な証明関数であるとき、 \(T\) の無矛盾性を表す論理式 \(p(|1=0|)=0\) は、 ペアノ算術で形式的に証明することはできません。