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

「形式システムの文字列を自然数によって表現すること　２」においてＭＩＵシステムと呼ばれる形式システムの文字列に数字を対応させて、システムの文字列の記述を算術的な計算に翻訳することを考えた。文字列の書き換えという思考の展開を数字の書き換えに置き換え、さらにその数字の書き換えが計算として記述できるということを見てきた。

これは形式システムの構造を自然数論の算術の中に写像したものになる。自然数論は非常に強力な記述能力を持っているので、システムの構造を写像することによって、そのシステム自体に言及するようなメタ数学的な命題も、自然数論の算術的命題として記述できる。つまり、算術的命題は、それがある計算を表しているという点で算術的な面を持つと同時に、その計算を解釈することによって、システム自体への言及の意味を読み取ることが出来る。

かけ算や足し算をしたりするのは算術的な計算だが、その計算がある規則に従ったものであることが分かると、それは規則に従った導出をしていると解釈され、その計算の結果得られた数字に対応する形式システムの文字列は、その形式システムでの定理であると判断される。その文字列が定理であるという判断は、形式システムの文字列の生成を語るものではなく、形式システムの全体を捉えた性質に対する言及になる。つまり、この計算はメタ的な意味を持つものとして解釈される。




前回のエントリーでは、ＭＩＵシステムを使って、形式システムの自然数論への埋め込みの雰囲気を味わったが、今回はその埋め込みによる計算がどのようなメタ的な言説の意味を持つかという、算術的な式をメタ的な命題として解釈するという意味の側面を考えてみたいと思う。さて、文字列をｑという記号で表して、次のような対応を考える。


　ｑ：ＭＩを表す　→　３１と数値化される


この３１をゲーデル数だというふうに考えて、ｇ（ｑ）で文字列ｑのゲーデル数を表す。そうすると、上の対応は次のような等式、すなわち算術的な式で書かれる。


　　　ｇ（ｑ）＝３１


この式は、ｑという文字列のゲーデル数が３１であるという数値関係を表す算術的な式である。そしてそれと同時にｑという文字列が公理であるというメタ的な言説の意味を持っている。

それでは次に、ＭＩＵシステムの書き換え規則によって生成される文字列に対応する数列について考えてみよう。前回例に出した次の文字列を考えてみよう。


１　ＭＩ　……　公理
２　ＭＩＩ　……　規則２においてｘとしてＩを用いた。
３　ＭＩＩＩＩ　……　規則２においてｘとしてＩＩを用いた。
４　ＭＵＩ　……　規則３によって最初のＩＩＩをＵで置き換えた。
５　ＭＵＩＵ　……　最後の文字がＩだったので規則１を適用してＵを付け加えた。
６　ＭＵＩＵＵＩＵ　……　規則２においてｘとしてＵＩＵを用いた。
７　ＭＵＩＩＵ　……　規則４を適用してＵＵを取り除いた。


これを数値化して計算に書き直すと、


１　３１＝１０×３＋１
２　３１１＝１０×３１＋１＝３×１０＾２＋１１
３　３１１１１＝１０＾２×３１１＋１１＝３×１０＾４＋１１１×１０＋１
４　３０１＝３×１０＾２＋１
５　３０１０＝１０×３０１＝３×１０＾３＋１０
６　３０１００１０＝１０＾３×３０１０＋１０＝３０１×１０＾４＋１０
７　３０１１０＝３０１×１０＾２＋１０


上の等式における二つの計算は、最初のものがそれ以前の数から生成規則に従って計算したことを示す計算式であり、あとのものは、次の数を生成するための根拠となる、生成規則で言えば仮言命題の前件に当たる数であることを示す等式になっている。つまり、上のような計算式が成り立つから、この数列は、形式システムにおいて正しい生成規則に従っているのだということが判る。正しい生成規則に従うというメタ的な言説が、この等式の意味として読み取れる。

この数列をメタ的な視点で眺めれば、それぞれがＭＩＵシステムでの定理であるという解釈がされる。７番目の３０１１０という数字は文字列に戻してやればＭＩＵシステムの定理であると解釈される。この数値化によってＭＩＵシステムの証明の構造も自然数論の中に埋め込まれたように感じる。しかし、上の数列はそのままでは自然数論の命題にはならない。一つ一つは自然数論の数式だが、それが並んでいるだけでは、全体としては数式とは呼べない。

自然数論の命題では、ある数が計算できて、その数が何かに等しいとか、そのような命題は直接表現できるものの、数列の前後の関係がある導出規則に従っているということを記述するような言語はない。それはメタ的な表現をする日本語の中にあるもので、上の数列のままでは、メタ的な表現は日本語に頼らなければならない。メタ的な表現までも自然数論の中に埋め込むにはどうしたらいいだろうか。

ゲーデル数を個々の記号に当てはめただけではメタ的な言説の意味をそこに読み取ることが出来ない。記号列の系列である数式の列にもゲーデル数が対応するような工夫をしなければならない。数列を、複数の数字として記述するのではなく、数列も一つの数字に対応するという写像が必要になる。それが素数のべきによって表現するというものになるのだろう。２から始めて素数を小さい方から順に７つ並べると

　　　　２，３，５，７，１１，１３，１７

になる。＾という記号でべきを表して、上のＭＩＵシステムの文字列に与えたゲーデル数を、この素数のべきとして用いて次の計算を考える。

　　２＾３１×３＾３１１×５＾３１１１１×７＾３０１×１１＾３０１０×１３＾３０１００１０×１７＾３０１１０

この数は、実際に計算することはたいへんだが、理論的には計算可能だし上の形のように素因数分解することも出来る。そして、素因数分解は一意性があるので、この数は上の数列に対応した唯一の数であるということも判る。つまり、この数を使えば、数列ではなく一つの数で上の証明式のＭＩＵシステムの文字列に対応した数列を表現することが出来る。ある数の解釈として、それが証明図式になっているかどうかが決定できそうだ。

ある文字列の系列としてＱが与えられたとき、つまりＱというのは次のように文字列として

　　ｑ１
　　ｑ２
　　ｑ３
　　……
　　ｑｎ

というＭＩＵシステムの文字列が並んだものと考える。このＱのゲーデル数をｇ（Ｑ）とすると、この文字列の系列がＭＩＵシステムでの正しい証明になっているというのは、ｇ（Ｑ）が算術の計算として上のような規則に従っているかどうかで決定される。それはまず

１　ｇ（Ｑ）を素因数分解する。
２　素因数分解の結果が、小さい素数から順に並んだ形になっている。
３　素数のべきがすべて３，１、０の数字からなっている。
４　小さい素数のべきから一つ大きい素数のべきにいたる計算が、計算規則を満たしている。

ということが確認されると、最後のｑｎという文字列が定理であるという判断が決定できる。これらは、すべて有限の手順で決定できるものだと思われる。なぜなら最初のゲーデル数が有限の大きさを持った具体的な数だからだ。

実際に与えられた数値が有限であっても、現実的には計算できないことがあるかもしれないが、理論的には可能だ。素因数分解は、その数よりも小さい数で順番に割っていって決定するが、それは有限の手順で終了する。

素数のべきに当たる数字が、ＭＩＵシステムの導出規則に従っているかどうかという問題は、その数が有限の大きさのものであれば、１０のべきの大きさによって、つまり対象の数を１０倍、１００倍、１０００倍などの場合に分けて導出規則を試してみることで、それに正しく従っているかが決定できるだろう。有限の大きさの数であれば場合分けは有限の個数になり、これも決定可能だと思われる。

ある文字列の系列Ｑが与えられたとき、そのゲーデル数ｇ（Ｑ）を考えることで、Ｑが証明の列であるかどうかが決定できる。そうすると、その証明の列の最後の文字列ｑｎが定理であるかどうかも決定できる。そうするとあるゲーデル数の最後のべきの指数に当たる文字列が導出規則に従った定理になっているかどうかということは、決定可能なものになる。式の系列の最後に当たるＭＩＵシステムの文字列をｑとしておくと、ｇ（Ｑ）からｇ（ｑ）を求めて、それが導出規則に従っていれば１を返し、そうでないときは０を返すような関数を考えることが出来る。


　　Ｄｅｍ（ｇ（Ｑ），ｇ（ｑ））＝１…式の系列Ｑがｑの証明になっている
　　Ｄｅｍ（ｇ（Ｑ），ｇ（ｑ））＝０…式の系列Ｑがｑの証明になっていない


この関数そのものはどのように記述されるかは具体的に示すことが出来ないが、決定可能であるということから算術の関数として定義できると思われる。素因数分解は理論的には一意に決定できるように行える。その最後のべきを指定することも算術式として存在記号を使うことで何とかなるだろう。導出規則に従っているかどうかも、存在記号の助けを借りて記述可能になるものと思われる。上の関数は、形式システムの中で記述できるものだと思われる。上の関数が１に等しければ、ここからｑが定理であることの意味を読み取ることが出来、ｑが証明可能であるというメタ的な言説を得ることが出来る。

この証明可能性を

　　　Ｐｒ（ｑ）

などというような式だと考えれば、証明可能性ということが自然数論の中に埋め込まれたと考えることが出来るだろう。ただ、この記号表現には一つ難しい問題がある。Ｑという式系列が具体的に与えられていれば、それは有限の範囲で決定可能になるのだが、Ｑが具体的に与えられていないときに、Ｑを探すことを含めてｑの証明可能性を考えると、それが無限のループになって決定できないかもしれないという心配が出てくる。具体的なＱがあればいいのだが、それが見つからないときは、いくら探しても見つからないのだというのを有限の範囲で決定できるかどうか。この証明可能性があらゆる式ｑに対して決定可能であれば、その形式システムは完全だと言えるのではないだろうか。そしてまた、決定できないｑが存在すればその形式システムは不完全だと言われるだろう。次は、このことを考察してみようと思う。