Gödel's reformulation of Gentzen's first consistency proof for arithmetic: The no-counterexample interpretation
Bulletin of Symbolic Logic 11 (2):225-238 (2005)
AbstractThe last section of “Lecture at Zilsel’s” [9, §4] contains an interesting but quite condensed discussion of Gentzen’s ﬁrst version of his consistency proof for P A , reformulating it as what has come to be called the no-counterexample interpretation. I will describe Gentzen’s result (in game-theoretic terms), ﬁll in the details (with some corrections) of Godel's reformulation, and discuss the relation between the two proofs.
Added to PP
Historical graph of downloads
References found in this work
On the Interpretation of Non-Finitist Proofs—Part I.G. Kreisel - 1951 - Journal of Symbolic Logic 16 (4):241-267.
A Semantics of Evidence for Classical Arithmetic.Thierry Coquand - 1995 - Journal of Symbolic Logic 60 (1):325-337.
Functionals Defined by Transfinite Recursion.W. W. Tait - 1965 - Journal of Symbolic Logic 30 (2):155-174.
Godel's Unpublished Papers on Foundations of Mathematics.W. W. Tatt - 2001 - Philosophia Mathematica 9 (1):87-126.
Citations of this work
Hilbert's Program Then and Now.Richard Zach - 2007 - In Dale Jacquette (ed.), Philosophy of Logic. Amsterdam: North Holland. pp. 411–447.
Lieber Herr Bernays!, Lieber Herr Gödel! Gödel on Finitism, Constructivity and Hilbert's Program.Solomon Feferman - 2008 - Dialectica 62 (2):179-203.
Reading Gentzen's Three Consistency Proofs Uniformly.Ryota Akiyoshi & Yuta Takahashi - 2013 - Journal of the Japan Association for Philosophy of Science 41 (1):1-22.
On the Intuitionistic Background of Gentzen's 1935 and 1936 Consistency Proofs and Their Philosophical Aspects.Yuta Takahashi - 2018 - Annals of the Japan Association for Philosophy of Science 27:1-26.
William Tait. The Provenance of Pure Reason. Essays on the Philosophy of Mathematics and on its History.Charles Parsons - 2009 - Philosophia Mathematica 17 (2):220-247.
Similar books and articles
Proof-Theoretic Reduction as a Philosopher's Tool.Thomas Hofweber - 2000 - Erkenntnis 53 (1-2):127-146.
On the No-Counterexample Interpretation.Ulrich Kohlenbach - 1999 - Journal of Symbolic Logic 64 (4):1491-1511.
Gentzen's Proof of Normalization for Natural Deduction.Jan von Plato & G. Gentzen - 2008 - Bulletin of Symbolic Logic 14 (2):240 - 257.
Direct Consistency Proof of Gentzen's System of Natural Deduction.Andrés R. Raggio - 1964 - Notre Dame Journal of Formal Logic 5 (1):27-30.