2013年1月20日日曜日

ゲーデルの不完全性定理からP≠NP問題にアプローチする - その2

ゲーデルの不完全性定理からP≠NP問題にアプローチするで、限定算術の無矛盾性証明を使って計算量の問題を考えるアプローチを紹介した。また、限定算術ではほとんどの体系の無矛盾性が言えないことも紹介した。今回は、無矛盾性概念を弱めることで限定算術の分離に用いようという色々な試みを紹介し、それから私のアプローチ(Yamagata 2012)を紹介したい。

前回紹介したParis Wiklie 1987の結果によると、限定算術はロビンソン算術Q(普通のペアノ算術から数学的帰納法を除いたもの)の無矛盾性を言わない。ただし、この結果はQが任意の述語論理を使えると仮定しているので、述語論理を弱めることが考えられる。例えば出てくる論理式の複雑度(量化子の数)を制限したり、カットなしの証明に制限したりすることが行われてきた。Pudlàk 1990は$S_2$($S^i_2$をすべて合わせたもの)が、$S^1_2$の証明で現れる論理式の量化子がすべて限定されている証明の無矛盾性を言わないことを示した。また、BussとIgnjatović 1995では、$S^i_2$は$S_2$から帰納法を除いた体系で、証明に現れる量化子の数がi個以下のものの無矛盾性($S^{-1}_2-B^i$)を言わないことを示した。

また、カット無しの体系の無矛盾性をいう試みについても否定的な結果が得られていて、Adamowiczらの研究では、エルブラン無矛盾性という弱い無矛盾性を定義して、これが限定算術で言えないことを示している。また、Buss 1986ではカットルールが公理に対してだけ適応されるよう証明を制限した$S^i_2$について、その無矛盾性が$S^i_2$で言えないことを示している。

もっとも、これらは必ずしも否定的な結果とは言えなくて、例えばもし$S^{-1}_2-B^i$の無矛盾性がもっと上の階層で言えれば、限定算術の分離ができる。もちろん、まだ言えていないけど。

さて、こうした否定的結果の原因はなんだろうか。まず、限定算術が数学的帰納法をのぞいた体系の無矛盾性を言えなかったりするのは、限定算術が実は帰納法を除いた体系で(帰納的カットを使って)解釈可能なことから当然だろう。では、それらの無矛盾性が、対応する限定算術より上の方の階層の限定算術で、なかなか言えそうにないのはなぜだろうか。限定算術ではなくて$I\Sigma^n$では、$I\Sigma^{n+1}$で$I\Sigma^n$の真理定義が可能なことからその分離ができるのだった。このやり方は限定算術では使えない。というのも、項を評価する関数が限定算術では定義できないからだ。

ここから、限定算術では項の指示対象の存在していると仮定できない、と考えるというのが私の考え。なので、これまでの限定算術は不完全で、これに加えて項の存在を示すために使われる公理と推論を体系に加える必要がある。Yamagata 2012では、これを$S^i_2E$として、ここから通常と同じ限定算術が導けることを示した。もっと重要なことは、BussとIgnjatović 1995と同様の体系$S^{-1}_2E-B^i$を定義して、この無矛盾性が$S^{i+2}_2$で言えることを示した。

これで、BussとIgnjatović 1995と同様に、$S^i_2$で$S^{-1}_2E-B^i$の無矛盾性が言えないことを示せれば、限定算術の階層の分離ができるのだが、この2年くらい色々考えているけどまだ言えていない。(Yamagata 2012はだいたい2年くらいまえの考えのスナップショット)まあどこまで言えるかわからないし、名目上の本業とも違うのだけど、やれるところまでやってみるつもり。ペトロス叔父みたいになるのが怖いけどね。