数学基礎論講義をこっそり読む（その３）

引き続きこっそり読んでいます。この本の冒頭に挙げられた問いの一つは

問1　ある形式体系Tにおいて、が証明できても、が証明できるような、あるが存在するとは限らない。その例を挙げよ。

で、直観には真っ向反していますが、こういうことが起こりうるのが形式体系の面白さなのか、わけわからなさなのか。

テキストではp.34において、この問題に関する概略の解答が提示されています。まだ、テキストにはでてきませんが、ある算術の公理系Tでは、証明も反証もできない命題が存在し、これを使って上記の問題に対する例を作ります。その証明をすこし丁寧にたどってみます。突然、論理記号やらが使われていますが、まあ、ここは目をつぶります。

をとします。

より、.　さらに

より、。

さて、もし が証明できるような、あるが存在したとして、が変数を含む場合は適当に定数を代入したものをとすると、も証明できる。ここで、もしまたはが証明できる場合は、たとえばが証明できる場合、

とが証明できることになり、矛盾です。

これで問題の解答ができたように見えますが、一点だけちょっと気になる点があります。かなり病的なケースとは思われますが、もも証明できない場合はちと困ります。が証明できるとが証明できるので、結局 とら自身が証明も反証もできない命題になっている場合です。ある特定の項が0か1かどうかすら証明も反証もできないというどうしようもない体系なのですが、算術の体系から公理を取り除いてしまうとそんなものができそうな気配もします。

このあたりのことを考えていてふと疑問がわいたのは、まともな体系でも、任意の２つの定項,（変数を含まない項）を持ってきたときに、もしくはのどちらかが証明できるという保証はあるのか？という点です。体系が演算や関数を持っている場合、それにかかわる公理がうまく作られていないと、この保証はないし、もちろん自明でもなく、（メタ）証明が必要であると思います。

それはさておき、ここまで読んで以前から気になっていたことのひとつが解消しました。前回の記事で前原昭二著『数学基礎論入門』を紹介しましたが、この本のp.39に『が自由変数を含む場合には、は一般には証明できない』とあります。左向き矢印は公理なので、問題はなのですが、推論規則 があるのになんで？という感じです。演繹定理から一発で出るのでは？… いや、もちろんだめです。演繹定理にはは文との制限があるからです。しかし、以前にこの注意書きを読んだときから、なんとなく気持ちが悪いままでした。

しかし、『数学基礎論講義』の問１からこれに対する例が作れます。
として、と取ります。もしが証明できたとすると、その対偶 すなわち が証明でき、は証明できるので、が証明でき、特にすなわちが証明できることになり、矛盾です。

最後にエルブランの定理の短い証明を。
全ての項tについて和集合 を考える。もし、の有限集合でモデルを持たないものがあると仮定する。すると、。すなわち 、となり、完全性定理より 。これが求める結果である。そこで、の有限集合が全てモデルを持つとする。コンパクト性定理よりがモデルを持つ。しかし、このモデルにおいては は真とはならず、、 すなわち に矛盾する。