論理学者のytb先生にask.fmで質問をしてみたら回答があった。
照井先生の著書を読んでいたら、ロビンソン算術QにΣ1式の帰納法を足した体系では原始再帰的関数が定義可能になる、… — いい質問ですね！それは、何をメタ理論とするかという、論理学における本質的な問題に関わる話です。
— ytb (@ytb_at_twt) 2016年3月10日
まず、メタの立… https://t.co/UdoKiohZFA
「いい質問」と褒められた上に丁寧なコメントまでいただいて、嬉しい。論理学に関しては筋金入りの素人を目指しているので、これは励みになるわ。
ytb先生に質問してから回答いただくまでの間に自分でも少し調べてはいた。菊池誠『不完全性定理』を見ると、表現可能性と可証再帰性を分けており、原始再帰的関数がIΣ1で可証再帰的な関数と一致するということと、再帰的関数がQで表現可能ということは両立する、ということまでは分かった。とはいえ重要なのは、なんで表現可能性と可証再帰性などという紛らわしい概念を区別して立てる必要があるのかを考えることで、ytb先生の回答はそこに向けられている、と理解した。
素人考えだが、「メタ理論も形式化して、表現可能性定理みたいなメタ定理を証明するプロセスを論理学的に分析してみよう」という動機はやはり第二不完全性定理に由来するのだろうか。第一不完全性を証明するプロセスを形式的にもう一度繰り返すことで第二不完全性は証明される。第一不完全性を証明する際には、原始再帰的関数を算術理論が表現できるということをメタ理論で示すので、第二不完全性の証明ではこれも形式化する必要がある。それはたぶんQみたいなヘボヘボな算術理論ではダメで、ある程度の帰納法を使える算術理論を必要とする。じゃあ、その理論はどのくらい弱くできるの？という疑問に対する答えがIΣ1で、これはQより強いがペアノ算術PAと比べればはるかに弱い。
こんなところで合っているかな。まぁ当たらずとも遠からずだろう。
ゲーデルの定理は奥が深く、勉強していると素人的な質問がいろいろと思い浮かんでくる。そして、こういう疑問を一つ一つ丁寧に潰していかないと、なかなか先に進めない。それは骨の折れる作業だが、理解が進んだときには喜びもある。まだまだ先は長そうだ。
