形式システムにおける証明の概念

『ゲーデル、エッシャー、バッハ』（ダグラス・Ｒ・ホフスタッター著、白揚社）という本の第２章「数学における意味と形」に「ｐｑシステム」と呼ばれる形式システムが紹介されている。この本は、ゲーデルの不完全性定理の「うまい説明」を語るものだが、そのためには７００ページ以上の文章を必要としている。この形式システムの説明では、形式システムにおける「証明」ということが、一般的に日常言語で語られている「証明」とどのように違っているかが説明される。ゲーデルの不完全性定理の理解には、この区別を理解することが必要なのだ。

この章では、普通の意味での「証明」の例として素数が無限に存在するということを証明する「ユークリッドの定理」が紹介されている。これとの比較で形式システムの「証明」を考えると分かりやすいかもしれない。素数というのは中学校程度の数学の知識で理解できるし、ユークリッドの証明もおそらく中学程度の数学の理解があれば判ると思うからだ。

素数は「１とその数自身以外に約数を持たない数」と定義される。具体的には

　　２，３，５，７，１１，１３，１７，１９，２３，２９，……

というような数が素数になる。１は素数の中に入れない。これは素因数分解の一意性を保証するためである。１を素数に入れてしまえば、因数としての１は何回でも使えるので素因数分解がただ一つに決定しなくなってしまう。

さて、この素数はこのようにして具体的に探していけばいくらでも見つかる。しかし、いくらでも見つかるという事実をもって、それが無限に存在するという結論を導くことはは出来ない。ユークリッドの証明は、最大の素数というものはないということを主張する。最大のものが無いので、ある素数が見つかれば、それより大きなものが必ず存在する。その発見はいつまでも続けられるので、このことから無限に存在するということが結論される。

それは、発見された最も大きな素数をＮとするとき、次のような数を作ることから、Ｎより大きな素数の存在が導かれる。

　　　２×３×５×…（Ｎより小さな素数をすべてかける）…×Ｎ＋１

この数は

２で割ると１余る　すなわち　２では割り切れない
３で割ると１余る　すなわち　３では割り切れない

　（以下同様）

Ｎで割ると１余る　すなわち　Ｎでは割り切れない

という数になっている。このＮ自身が素数であれば、これはＮよりも大きい数になっているので、Ｎよりも大きな素数の存在を主張できる。また、Ｎが素数でなかった場合は、Ｎを素因数分解したときに、Ｎ以下のどの素数とも違う素数が見つかる。なぜなら、Ｎ以下のどの素数も上の数を割ることが出来ないので素因数にならないからだ。いずれにしてもＮよりも大きな素数が見つかることになる。

上記の本では、この証明によって「素数は無限にたくさんある」ということが正しいということつまり「真である」ということが確かめられると書いてある。この命題は、事実として直接確かめることが出来ないにもかかわらず、証明されることによってその真理性が主張される。まさに、証明されるからこそ「真である」ということが言えるものになるわけだ。

これが普通の数学における「真なる命題」の定理と「証明」との関係になる。「ゲーデルの不完全性定理に関する疑問」というブログ・エントリーに書かれていたように、「普通の現場の数学研究者は、「真であること」と「証明可能であること」の差異に感度を持たない。要するに、ある数学的命題が真であるというのは、その命題が公理系から証明可能であることに他ならない、と思っている」という印象に結びつくのではないかと思う。

この普通の数学における「証明」は、その証明された事柄（定理）が正しいことと深く結びついている。しかし、形式システムで「証明」と呼ばれているものは、実は「真である」というような性質とは全く無関係に定義されている。形式システムにおいては「真である」ということは、その形式に何らかの意味を与えたときに初めて生じてくる性質となる。そのあたりの「証明」という言葉の違いを「ｐｑシステム」について見ることで理解を図ってみたいと思う。

「ｐｑシステム」は、

　　　ｐ、ｑ、−（ハイフン）

の３つの記号からなるもので、この記号がある規則の下に並べられる。つまり、ある規則によって秩序だって記号列が生み出されるというシステムになっている。まず、どのような記号列がそのシステムに属するかということで、ある形を持った記号列が提示される。システムの出発点となるような記号列の指定をするものは「公理」と呼ばれている。この「公理」の使い方も、日常言語とはちょっと違うものになっているだろう。公理の定義は次のようになされる。

　定義　ｘがハイフンだけの列であるとき、
　　　　　　ｘｐ−ｑｘ−
　　　　は公理である。

ｘはハイフンだけの列であれば何でもいい。たとえば、ｘとして３つハイフンが並んだものを取れば、次の記号列が出発点としての公理になる。

　　　−−−ｐ−ｑ−−−−

これはシステムとして、この出発点から生成される記号列を持つ。その生成規則は次のように語られる。

　規則　ｘ、ｙ、ｚはどれもハイフンのみからなる特定の列を表すとする。もし
　　　　　　　ｘｐｙｑｚ
　　　　が定理であれば、
　　　　　　　ｘｐｙ−ｑｚ−
　　　　も定理である。

公理は出発点としての定理であるから、上の公理の例を、この規則に当てはめると、

　　　−−−ｐ−−ｑ−−−−−

という記号列が新たな定理として生成される。この形式システムが、形式システムであることを出なければ、「証明」とは、それが「定理」であることを示すことになるから、その記号列が出発点としての「公理」から、生成規則を何回か使って変形したものであることを示すということになる。この形式システムにおける「証明」とはそれ以上の意味はない。

この形式システムには、「真である」という概念もない。もし「証明」と結びつけるなら、証明された定理を「真である」と呼んでもいいが、そう呼ぶことによって何か事情が変わるかといえば、何ら事情が変わることはなく、そういわなくても何ら問題はない。「真である」という言葉は、この形式システムには必要ないと言える。

しかし、この形式システムに何らかの「解釈」が出来ると、その解釈から得られる意味によって形式システムは、形式以上の何かを持つことになる。「ｐｑシステム」は、二つの数の加法という意味を持たせることが出来る。ハイフンの数を正の整数に対応させれば公理は次のように表現されるだろう。

　　　ｘ＋１＝（ｘ＋１）

これは数式で書くとわかりにくいが、要するに、１を加えるという計算の答えは、次の整数になるということを公理は表している。上の例を数式にすると

　　　３＋１＝４

となる。また規則の方は、次のようなるだろうか。

　　　ｘ＋（ｙ＋１）＝（ｘ＋ｙ）＋１

これは、ｙに当たる数の次の数を加えれば、それは答えだった数の次の数になると解釈できる。例に当てはめると、「３＋１＝４」という式から

　　　３＋２＝５

という式が求められる。このように、「ｐｑシステム」は、二つの数の加法という解釈が出来るが、それは加法として正しいものが定理になっている。つまり、加法として正しい解釈が出来るということを「真である」と定義すれば、「ｐｑシステム」は真である加法の式を生成する。

このように意味を読み取ることの出来る解釈をすると、システムの「証明」とは別に「真である」という定義をすることが出来る。そうすると、「真である」数式がすべて「証明」出来るかという完全性の問題もそこに提示することが出来る。

「ｐｑシステム」では、加法のすべての正しい式を生成することは出来ない。この公理と規則からは、３つの数の加法は生成できないからだ。だから、加法のすべてに対しては「ｐｑシステム」は完全性を持たない。つまり不完全だ。しかし２つの数の加法に限るなら、「１＋１＝２」という式を最も小さい数式の出発点として、すべての正の整数の二つの数の加法においては、正しい式はすべて生成することが出来るだろう。つまり、対象を二つの数の間の加法に限れば、このシステムの完全性をいうことが出来る。

「真である」という概念は、形式システムにおいてはその解釈と意味づけに関係して定義される。それに対して「証明される」という概念は、単に生成規則に従って生み出されるという現象に関してのみ定義される。形式システムにおいては、この両者に絶対的な結びつき、あるいは論理的な関連性はないといっていいのではないだろうか。それは、ある解釈を選び取り、意味を選択したときに関係が生じてくるのだ。

命題論理を形式システムとして捉えたときも、そこで「真である」ということの定義は、命題の意味を考えたときに定義される。その意味は、命題の内容にかかわるものと、論理結合子と呼ばれる記号の意味（かつ、または、ならば、〜でない、など）にかかわるものとで若干の違いはあるものの、「真である」ということを考えるときは、意味というものが深く関わってくる。

しかし、命題論理を公理的に構築しようとすると、そこにはもう意味というものは捨象される。それは、意味を無視した記号列として考えられている。問題は、出発点としての公理としての記号列（命題を表現する列）と、そこから生み出される記号列の生成の規則とで、どのような記号列が定理として生み出されるかということだけだ。規則に従って生み出された記号列が定理と呼ばれるのは、上で紹介した「ｐｑシステム」と変わりはない。

命題論理においては、意味論的に定義された「真である」命題が、構文論的（生成規則によって生み出されるという考え方）に「証明された」命題と完全に一致することが証明されている。つまり、完全性が確かめられている。

ゲーデルの不完全性定理では、自然数論を形式システムとして構築したときに、意味論的に「真である」にもかかわらず、その形式システムでは記号列の生成として「証明できない」命題が存在するということが語られている。だからこそ不完全だといわれている。形としては、上のような単純な「ｐｑシステム」と同じだ。しかし自然数論における意味論的な「真である」という概念はやはりわかりにくい。これが、果たしてうまく説明できるだろうか。