Title
A Relationship Among Gentzen's Proof-Reduction, Kirby-Paris' Hydra Game and Buchholz's Hydra Game
Abstract
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 independence 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 phi(omega)(0) (while that of PA or of Kirby-Paris' Game is phi(1)(0) = epsilon(0)) in the Veblen hierarchy of ordinals.
Year
DOI
Venue
1997
10.1002/malq.19970430113
MATHEMATICAL LOGIC QUARTERLY
Keywords
Field
DocType
cut elimination,combinatorial independent game,proof-theoretic independence result,Hydra game,Peano arithmetic
Combinatorial game theory,Veblen function,Discrete mathematics,Peano axioms,Combinatorics,Nim,Ordinal number,Lernaean Hydra,Bondareva–Shapley theorem,Mathematics,Extensive-form game
Journal
Volume
Issue
ISSN
43
1
0942-5616
Citations 
PageRank 
References 
4
0.65
2
Authors
2
Name
Order
Citations
PageRank
Masahiro Hamano1397.66
Mitsuhiro Okada248853.23