エレファント・ビジュアライザー調査記録

ビジュアルプログラミングで数式の変形を表すことを考えていくブロクです。

不完全性定理(2)

不完全性定理とはなにか (ブルーバックス)』では「チューリング機械の停止問題」を参考にして「不完全性定理」を考えるということなので、前回は「チューリング機械の停止問題」について調べてみました。チューリング機械を扱うのではなく、無限のメモリーを持つコンピューター上のプログラミング言語の関数として考えました。チューリング機械の詳細な議論はしていませんが、この本でもそう書かれているようにだいたい同じものと考えられます。この方針を継続して不完全性定理についても考えていきます。

(論理式で書かれた)命題をプログラミング言語の式と考えます。命題の証明は、(関数の実行と同様に一定の有限の時間で行われる「段階」に分けることができて、各「段階」では推論規則(複数あります)または公理(複数あります)の1つが適用されます。有限個の「段階」で「常に真である命題」に到達したとき、または逆に「常に真である命題」から出発して有限個の「段階」で命題に到達したとき、命題は証明可能となります。そうではないときは命題は証明可能ではありません。

命題は「ソースコード」(文字列)で表されているとします。任意の文字列は「構文解析」によって「ソースコード」かどうかを判定することができるとします。変数名は「リスト」になっているとします。

命題が証明可能であるとき、証明の各「段階」をすべて(構造に従って)並べて書いたものを形式証明とします。形式証明は「ソースコード」(文字列)で表されているとし、命題の一部分とすることができます。

ゲーデル数を使った証明ではないので条件は違いますが、条件が強くなっているので不完全性の証明には問題ありません。

不完全性定理の証明

この本の流れに沿って見ていきます。チューリング機械の停止問題と比較するとわかりやすいと、この本では言っているようなので、できるだけチューリング機械の停止問題の記述に合わせてみることにします。

【ステップ1】 1変数の命題  F(y) を網羅した一覧表を作る。並べ方は、その命題の番号の小さい順とする。( F_{1}(y) F_{2}(y) F_{3}(y),……)

命題や形式証明は(プログラミング言語の式のように構造を持った)「式」として表します。

「式」のソースコードから「構造の『深さ』に関する帰納法」によって「式」に番号をつけることができます。無限個使うことができる変数名はリストで表されているので、これは可能です。逆に「式」を指定すると、構造を再現することができます。番号  i に対応する「式」を 「 i 番目の『式』」 e(i) とします。

【ステップ2】「 F_k(l) の形式証明の『式』  x が存在する」という命題を考える。これを  \exists x P(x,k,l) と略記する。
【ステップ3】命題  \exists x P(x,k,l) k l を変数  y に置き換え、否定にした命題  \lnot \exists x P(x,y,y) を考える。これは1変数  y をもつ命題なので、ステップ1で作った一覧表のどこかにある。それがたまたま上から  n 番目だったので、 F_n(y) と書く。つまり、 F_n(y) = \lnot \exists x P(x,y,y)
【ステップ4】 F_n(y) = \lnot \exists x P(x,y,y) の変数  y に(自分自身の背番号) n ( n 番目の「式」を表す自然数)を代入する。すなわち、 F_n(n) = \lnot \exists x P(x,n,n)
【ステップ5】ステップ4で作った命題  F_n(n) = \lnot \exists x P(x,n,n) の右辺の内容は、(ステップ2を思い出せば)「 F_n(n) の形式証明の『式』 x が存在しない」となる。対応する「式」の自然数が存在しないのだから、それは、 F_n(n) が証明できない、ということだ。でも、左辺を見れば、それは  F_n(n) にほかならない。すなわち、「この命題は証明できません」という命題  F_n(n) ができてしまった!

これは何を言っているのか考えてみます。ゲーデル数を使った議論は一階述語論理に「ペアノ算術」の公理系を追加した体系の議論で、ここでは一階述語論理に(ここには書いていませんが)プログラミング言語の「式」の公理系を追加した体系の議論となっています。一階述語論理では変数のない命題は真であるか偽であるかのどちらかになるので、ゲーデル数の議論でも「式」の議論でもそうなります。

自然数に関する命題  F_n(n) F_n(y) の変数  y を特定の自然数  n で置き換えたものなので、変数のない命題となっています。自然数  n に関する命題  F_n(n) が偽であるとすると、「 F_n(n) の形式証明の『式』を表す自然数が存在する」ということになります。すると  F_n(n) は真ということになって  F_n(n) が偽であることに矛盾します。よって  F_n(n) は真でなければなりません。 F_n(n) は真ならば「 F_n(n) の形式証明の『式』を表す自然数が存在しない」ということになって  F_n(n) は証明できないということになります。よって  F_n(n) は真で証明できないということになります。

チューリング機械の停止問題では関数が停止するかどうか決まっていると仮定したところが、この議論では「 F_k(l) の形式証明の式が存在する」という命題を考えるようになっています。ここが異なっているため命題がわかりにくくなっていると思われるので、同じようにできないか検討してみたいと思います。