TY - JOUR
T1 - A relationship among Gentzen's proof-reduction, Kirby-Paris' hydra game and Buchholz's hydra game
AU - Hamano, Masahiro
AU - Okada, Mitsuhiro
PY - 1997
Y1 - 1997
N2 - We first note that Gentzen's proof-reduction for his consistency proof of PA can be directly interpreted as moves of Kirby-Paris' Hydra Game, which implies a direct inde-pendence proof of the game (Section 1 and Appendix). Buchholz's Hydra Game for labeled hydras is known to be much stronger than PA. However, we show that the one-dimensional version of Buchholz's Game can be exactly identified to Kirby-Paris' Game (which is two-dimensional but without labels), by a simple and natural interpretation (Section 2). Jervell proposed another type of a combinatorial game, by abstracting Gentzen's proof-reductions and showed that his game is independent of PA. We show (Section 3) that this Jervell's game is actually much stronger than PA, by showing that the critical ordinal of Jervell's game is φω(0) (while that of PA or of Kirby-Paris' Game is φ1(0) = ε0) in the Veblen hierarchy of ordinals.
AB - We first note that Gentzen's proof-reduction for his consistency proof of PA can be directly interpreted as moves of Kirby-Paris' Hydra Game, which implies a direct inde-pendence proof of the game (Section 1 and Appendix). Buchholz's Hydra Game for labeled hydras is known to be much stronger than PA. However, we show that the one-dimensional version of Buchholz's Game can be exactly identified to Kirby-Paris' Game (which is two-dimensional but without labels), by a simple and natural interpretation (Section 2). Jervell proposed another type of a combinatorial game, by abstracting Gentzen's proof-reductions and showed that his game is independent of PA. We show (Section 3) that this Jervell's game is actually much stronger than PA, by showing that the critical ordinal of Jervell's game is φω(0) (while that of PA or of Kirby-Paris' Game is φ1(0) = ε0) in the Veblen hierarchy of ordinals.
UR - http://www.scopus.com/inward/record.url?scp=0031538704&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0031538704&partnerID=8YFLogxK
U2 - 10.1002/malq.19970430113
DO - 10.1002/malq.19970430113
M3 - Article
AN - SCOPUS:0031538704
SN - 0942-5616
VL - 43
SP - 103
EP - 120
JO - Mathematical Logic Quarterly
JF - Mathematical Logic Quarterly
IS - 1
ER -