形式システムの文字列を自然数によって表現すること　２

『ゲーデル、エッシャー、バッハ』で解説されているＭＩＵシステムについて、これを文字列ではなく数字で表現することの意味を考えてみたいと思う。これは、ゲーデルの証明におけるゲーデル数の表現の解説として受け取ることが出来る。形式システムとして文字列で表現されている自然数論を、数の間に成立する関係を文字列の表現にしてしまおうというアイデアの構造を理解するための解説として考えてみようと思う。文字列の解釈として、ある意味では自然言語での表現の意味に受け取れる自然数論を、数の間に成立する命題として解釈してしまおうというアイデアを直感的に理解するために、ＭＩＵシステムと自然数論の間に成立する同型写像を見てみよう。

さて、ＭＩＵシステムは次のように語られていた。

記号　　Ｍ，Ｉ，Ｕ
公理　　ＭＩ
規則
　１　ｘＩが定理ならば、ｘＩＵは定理である。
　２　Ｍｘが定理ならば、Ｍｘｘは定理である。
　３　任意の定理において、ＩＩＩはＵで置き換えることが出来る。
　４　任意の定理において、ＵＵは除くことが出来る。

このＭ，Ｉ，Ｕという３つのアルファベットで表現される文字列を、３つの異なる数字で表現して、数字の表現のシステムにおいても、ＭＩＵシステムが持つ構造が同じ形で反映されるように表現してみよう。Ｍ，Ｉ，Ｕの３つの異なるアルファベットに、３つの異なる数字を与えるのは、これは異なってさえいれば、つまり区別が出来れば何でもいい。これがゲーデル数に当たるものになる。

この本では

　　　Ｍ　……　３
　　　Ｉ　……　１
　　　Ｕ　……　０

の３つの数字を使っている。ＭＩＵシステムでは、使われる文字はこの３つだけなので、数字も３，１，０以外は使う必要がない。上のＭＩＵシステムの定義の中の３つの文字をこの３つの数字に置き換えると次のような表現になる。

記号　　３，１，０
公理　　３１
規則
　１　ｘ１が定理ならば、ｘ１０は定理である。
　２　３ｘが定理ならば、３ｘｘは定理である。
　３　任意の定理において、１１１は０で置き換えることが出来る。
　４　任意の定理において、００は除くことが出来る。

これは、単に文字列を書き換えただけなのでもちろん構造はＭＩＵシステムと同じになる。しかし、この表現ではゲーデルのアイデアを感じることは出来ない。なぜ文字を数字にするかということの本質がこれでは見えてこないからだ。この定義では、数字は単に文字の代わりを務めるだけのものに過ぎない。数字本来の性質は使われていない。数字本来の性質とは、それが計算できるということで、上の定義の中の文字列の表現が、数字の計算として表現できたとき，ここにゲーデルが使ったアイデアの一端が見えてくる。

上の公理を３１（さんいち）という文字列として読まずに、３１（さんじゅういち）という数字として読み、規則を文字列の書き換えとして読まずに、計算規則として書き換えると次のようになる。

１　＜１０ｍ＋１＞が作られている

　　　　　　↓
　　＜１０×（１０ｍ＋１）＞を作ることが出来る
　（文字列の後ろに１があればということが（１０ｍ＋１）で表現されている。そしてそのときに文字列の後ろに０を付け加えることが出来るということが（１０×）というかけ算で表現されている。）

２　＜３×１０＾ｍ（１０のｍ乗と読む）＋ｎ＞が作られている

　　　　　　↓
　　＜１０＾ｍ×（３×１０＾ｍ＋ｎ）＋ｎ＞を作ることが出来る
　（３の後ろに文字列がｍ個つながっているということを（３×１０＾ｍ＋ｎ）で表現している。ｎはｍ個の文字列、つまりｍ桁の数として考えられている。このｎが文字列の表現ではｘに当たるものになる。規則ではこのときさらに後ろに文字列ｘを付け加えることが出来ることを語っている。それは、ｍ桁ずらすために（１０＾ｍ×）というかけ算をし、その後ろにｍ桁の数ｎを加えることで表現している。）

３　＜ｋ×１０＾（ｍ＋３）＋１１１×１０＾ｍ＋ｎ＞が作られている

　　　　　　↓
　　＜ｋ×１０＾（ｍ＋１）＋ｎ＞を作ることが出来る
　（文字列の間に１１１があったときということを、１０＾ｍの位置にある（つまり（ｍ＋１）桁目の位置から３つ１が並んでいる）考えている。その１の前には３を先頭にするｋという数字が並んでいる。後ろにはｍ桁の数ｎが並んでいる。規則では１１１という３桁の１を取り除くので、計算としてはｍ桁の数ｎと（ｍ＋１）桁目からの数ｋとが並ぶ数字になる。）

４　＜ｋ×１０＾（ｍ＋２）＋ｎ＞が作られている

　　　　　　↓
　　＜ｋ×１０＾ｍ＋ｎ＞を作ることが出来る。
　（４の規則では二つ並んでいる０を取り除くことが出来る。それは（１０＾（ｍ＋２））が１０＾ｍになることで１０のべき乗が二つ減ることで表現されている。上の計算の表現での前件は、ｍ桁の数ｎの前に０が二つついていると解釈することが出来る。）

このように表現を変えると、Ｍ，Ｉ，Ｕという３つの文字列を、単に数字という文字に置き換えたのではなく、自然数の計算として解釈した構造の表現になっている。つまり、ＭＩＵシステムで文字列の書き換えとして考えていたものが、数における計算として理解され、その計算結果がどうなるかということがＭＩＵシステムの構造を考えることと同じものになる。ＭＩＵシステムの構造が自然数の計算として写像されていることになる。文字列の形式システムが自然数論の中に取り込まれた。

このアイデアの解説は次のように書かれている。ここで「３１０システム」と呼ばれているのは、数の計算として表現されたＭＩＵシステムと同型のシステムを指す。

「この「３１０システム」にも、延長規則と短縮規則が絶えずつきまとっていることに注意。これらの規則はただ数の領域に移されただけなので、ゲーデル数が大きくなったり小さくなったりする。そこで行われていることを注意深く眺めれば規則を発見できるが、その着想は整数の１０進法で表示された数字を右や左にずらすことと、１０のべきの乗法や除法に結びつけるということに過ぎず、深遠なものではない。この簡単な知見は次のように一般化できる。
中心命題:
１０進法で表示されたいかなる数においても、ある数字をどのようにずらし、変更し，除去し，あるいは挿入するかを教える字形的規則があれば、加法、減法そのほか１０のべきに対する算術的演算を含み、この規則に対応する算術的規則によっても同じように表現できる。
　もっと簡単に言えば……
＜数字を処理する字形的規則は、実際は数に作用する算術的規則である。＞」

このアイデアは、ゲーデルの証明において重要な部分を占めるものとなるだろう。形式システムにおける公理や推論規則による文字列の書き換えは、「字形的規則」として語られる。その「字形的規則」において、それを数値化し（ゲーデル数化する）、数字の位置をずらしたり、書き換えるという規則にすることが出来れば、それは計算として記述できるということを上の命題は語っている。

形式システムにおける証明の問題は、文字列の書き換えの中である規則に従ったものを「証明可能である」といい、その規則に従わないものを「証明可能ではない」という。これは、文字列を数値化することが出来れば、「計算可能である」あるいは「計算可能ではない」という言い方にすることが出来る。計算体系を持つ自然数論の中に写像出来る。

ゲーデルは、このアイデアによって自然数論における「証明可能性」を自然数論の中の「計算可能性」に置き換えて、「証明可能である」ということを「計算可能だ」という命題に置き換えた。これは、実際に証明可能だということが言える文字列に関しては、その書き換えに対応する計算を記述できるので、「計算可能だ」ということが言えるようになるだろう。問題は、すべての文字列に対して「証明可能」かどうかが判定できるかどうかということが「完全性」という問題では重要になってくることだ。「証明可能である」ことが分かっている文字列に関しては「計算可能である」ことが分かる。それが任意の文字列に対して成立するかどうか。任意の数字に対して，それが計算可能であるかないかが判定できるかどうか。

この問題を考えるときに、「証明可能でない」ということが判る文字列が見つかったらどうなるだろうか。ＭＩＵシステムにおいてはＭＵは証明できないことが分かっている。３１０システムとして考えると３０は証明できない。つまり、計算規則によって算術的な計算は出来ない数字になる。

この「計算可能でない」という性質は、かけ算と足し算だけの算術的計算によって表現することは出来ない。表現できてしまうと「計算可能」になり矛盾するからだ。「計算可能でない」性質は計算として表現することは出来ないが、メタ的な命題としては表現できる。自然数論ではなく自然言語としての日本語では表現できる。これを自然数論の中に埋め込む方法があるだろうか。もしこれが出来れば、「計算可能でない」性質が「計算可能」になる。パラドックス的な状況が見えてくるだろう。そうすれば、システムに矛盾がなければ、このような状況が起こることは考えられない。そうすると、そのように「計算可能」でないことが「計算可能」になる表現は、実はどちらにも決定できないものかもしれない。

ゲーデルは、自分自身に対して「私は証明できない」と解釈できる表現を作ったと言われている。このような表現が本当に出来るのかどうか、ＭＩＵシステムでメタ的な表現を自然数論の算術的表現として作れるかどうかを考えることで比喩的に理解できないだろうかを考えたい。ＭＩＵシステムにおいて，そこでの証明可能性を算術的計算を解釈することで決定できるかどうか。そして、それが決定できたとき、証明不可能性も算術的に表現できるかどうか。そのあたりのことを考えてみたいと思う。