A Relationship Among Gentzen's Proof-Reduction, Kirby-Paris' Hydra Game and Buchholz's Hydra Game

DOI10.1002/MALQ.19970430113zbMATH Open0872.03038OpenAlexW2063421309MaRDI QIDQ4333476FDOQ4333476

Authors Masahiro Hamano, Mitsuhiro Okada

Publication date 8 April 1997

Published in Mathematical Logic Quarterly (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1002/malq.19970430113

zbMATH Keywords

arithmeticunprovabilityGentzen's proof reductionhydra gameordinal strength of Jervell's Gentzen game

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Recursive ordinals and ordinal notations (03F15)

Recommendations

• Hydra Games and Tree Ordinals
• A new proof-theoretic proof of the independence of Kirby-Paris' hydra theorem.
• A direct independence proof of Buchholz's Hydra Game on finite labeled trees
• The Hydra battle and Cichon's principle
• scientific article; zbMATH DE number 1870412

Cites work

• Note on a proof of the extended Kirby-Paris theorem on labelled finite trees

Cited in

(7)

• A new proof-theoretic proof of the independence of Kirby-Paris' hydra theorem.
• Die another day
• Current research on Gödel's incompleteness theorems
• Hydra Games and Tree Ordinals
• Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations
• On some slowly terminating term rewriting systems
• scientific article; zbMATH DE number 7577570 (Why is no real title available?)

This page was built for publication: A Relationship Among Gentzen's Proof-Reduction, Kirby-Paris' Hydra Game and Buchholz's Hydra Game

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4333476)