第二不完全性定理が成り立つ形式的体系として,
IΣ_1 というものがあると聞きました.
最近の勉強は, IΣ_1 における第二不完全性定理の定式化です.
IΣ_1 における自然数論が, 半環の公理を満たすことの証明が,
これまたデリケートです.
数学的帰納法の適用の際に, (∀x)A(x, y) の形の論理式を,
うかつに帰納法の仮定として設定できないからです.
ここで, 論理式 A(x, y) を帰納法の仮定として設定し,
x を自由変数とみなし, y についての帰納法とみなせば良いという
ご意見があるそうですが, それはダメです.
なぜならば, A(x, y) を帰納法の仮定として設定した時点で,
x も y も定数とみなさなくてはならないからです.
この辺りの議論は, 私の書いた数理論理学入門のノートに詳しい記述があります.
一般に, 形式的体系 T 内で, A(x) → B の形の論理式を証明する際に,
T + A(x) 内で B を証明すれば良いのですが,
T + A(x) という形式的体系内では, x は定数扱いです.
このやり方ですと, ゲンツェンの LK との論理的関係性が,
以下のようにきれいになります.
T から 論理式 C が証明可能なための必要十分条件は,
T の非明示的公理の全称閉包の有限列 A_1,・・・,A_n と
T の明示的公理の有限列 B_1,・・・B_m が存在し,
sequent
A_1,・・・,A_n, B_1,・・・B_m → C
が LK provable であることです.
この定式化は, 河合文化教育出版の入門数学基礎論 (倉田先生の著書)
に, 変更を加えたものです.
