著者

浜野 正浩

出版者

三田哲學會

雑誌

哲学 (ISSN:05632099)

巻号頁・発行日

no.104, pp.33-44, 1999-12

---

投稿論文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.