A relationship among Gentzen's proof-reduction, Kirby-Paris' hydra game and Buchholz's hydra game

Masahiro Hamano, Mitsuhiro Okada

Research output: Contribution to journalArticle

11 Citations (Scopus)

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 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.

Original languageEnglish
Pages (from-to)103-120
Number of pages18
JournalMathematical Logic Quarterly
Volume43
Issue number1
Publication statusPublished - 1997

Fingerprint

Game
Combinatorial Games
Relationships
Ordinals
Imply

Keywords

  • Combinatorial independent game
  • Cut elimination
  • Hydra game
  • Peano arithmetic
  • Proof-theoretic independence result

ASJC Scopus subject areas

  • Logic

Cite this

A relationship among Gentzen's proof-reduction, Kirby-Paris' hydra game and Buchholz's hydra game. / Hamano, Masahiro; Okada, Mitsuhiro.

In: Mathematical Logic Quarterly, Vol. 43, No. 1, 1997, p. 103-120.

Research output: Contribution to journalArticle

@article{2876a47ce05b4dcfb782a5b83a308d44,
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 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.",
keywords = "Combinatorial independent game, Cut elimination, Hydra game, Peano arithmetic, Proof-theoretic independence result",
author = "Masahiro Hamano and Mitsuhiro Okada",
year = "1997",
language = "English",
volume = "43",
pages = "103--120",
journal = "Mathematical Logic Quarterly",
issn = "0942-5616",
publisher = "Wiley-VCH Verlag",
number = "1",

}

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.

KW - Combinatorial independent game

KW - Cut elimination

KW - Hydra game

KW - Peano arithmetic

KW - Proof-theoretic independence result

UR - http://www.scopus.com/inward/record.url?scp=0031538704&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0031538704&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0031538704

VL - 43

SP - 103

EP - 120

JO - Mathematical Logic Quarterly

JF - Mathematical Logic Quarterly

SN - 0942-5616

IS - 1

ER -