カット除去法による独立性証明
スポンサーリンク
概要
- 論文の詳細を見る
投稿論文1. はじめに2. Kirby-ParisのHydra Game3. GentzenのPAのためのcut除去法4. cut除去法による定理1の証明5. まとめWe give a direct independence proof of Kirby-Paris' Hydra Game [9] from Peano Arithmetic (PA). This is done by giving a relationship between Gentzen's consistency proof [5] for PA and the Hydra Game. Compared with Kirby-Paris' and Cichon's [3] proofs, our proof is direct in that we do not use any finite characterization theorem of the PA-provably recursive functions. We prove that one step reduction of Kirby-Paris' Hydra Game corresponds to finite steps of Gentzen's proof reduction. With the help of Godel's Incompleteness Theorem, Kirby-Paris' unprovability result follows.
- 慶應義塾大学の論文