- 596 名前：スレタイスレ446 [2011/11/29(火) 20:50:01.89 ]
- >>594
そんな感じですね。
カントール対関数でユニークにエンコード、
β関数でユニークにデコード、
両方とも可証性述語の定義に必要。
指数関数というか原始再帰的関数とそれに関する公理を
すべてぶっこんだPAの保存拡大はPRAとかよく言われます。
余談：ところで不完全性定理はT|-/-Con(T)でしたが、
Π1^0文に関してはWKL0|-φ⇒PRA|-φとなり、
ヒルベルト・プログラムの断片的実現と呼ばれます。
ですからケーニッヒ補題が超越的とかいう書き込みが上の方にありますが、
ケーニッヒ補題を使った文は有限の立場の文に置き換えれますね。
