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)
  Copy   BIBTEX

Abstract

The last section of “Lecture at Zilsel’s” [9, §4] contains an interesting but quite condensed discussion of Gentzen’s first version of his consistency proof for P A [8], reformulating it as what has come to be called the no-counterexample interpretation. I will describe Gentzen’s result (in game-theoretic terms), fill in the details (with some corrections) of Godel's reformulation, and discuss the relation between the two proofs.

Categories

Keywords

Reprint years

DOI

10.2178/bsl/1120231632

Other Versions

reprint Tait, W. W. (2010) "Gödel's reformulation of Gentzen's first consistency proof for arithmetic : the no-counterexample interpretation". In Gödel, Kurt, Feferman, Solomon, Parsons, Charles, Simpson, Stephen G., Kurt Gödel: essays for his centennial, pp. : Association for Symbolic Logic (2010)

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,247

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

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.
A Relationship Among Gentzen's Proof‐Reduction, Kirby‐Paris' Hydra Game and Buchholz's Hydra Game.Masahiro Hamano & Mitsuhiro Okada - 1997 - Mathematical Logic Quarterly 43 (1):103-120.
Decoding Gentzen's Notation.Luca Bellotti - 2018 - History and Philosophy of Logic 39 (3):270-288.
Extending the First Gentzen's Consistency Proof to the Intuitionistic Case.María Pallares - 2004 - Logic Journal of the IGPL 12 (6):549-560.
Review: W. W. Tait, A Nonconstructive Proof of Gentzen's Hauptsatz for Second Order Predicate Logic. [REVIEW]Moto-O. Takashaih - 1968 - Journal of Symbolic Logic 33 (2):289-290.
Tait W. W.. A nonconstructive proof of Gentzen's Hauptsatz for second order predicate logic. Bulletin of the American Mathematical Society, vol. 72 , pp. 980–983. [REVIEW]Moto-O. Takahashi - 1968 - Journal of Symbolic Logic 33 (2):289-290.
A Philosophical Significance of Gentzen’s 1935 Consistency Proof for First-Order Arithmetic.Yuta Takahashi - 2016 - Kagaku Tetsugaku 49 (1):49-66.
Gentzen’s consistency proof without heightlines.Annika Siders - 2013 - Archive for Mathematical Logic 52 (3-4):449-468.
Gentzen’s 1935 Consistency Proof and the Interpretation of its Implication.Yuta Takahashi - 2018 - Proceedings of the XXIII World Congress of Philosophy 55:73-78.

Analytics

Added to PP
2009-01-28

Downloads
165 (#141,669)

6 months
10 (#404,653)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

William W. Tait
University of Chicago

Citations of this work

Hilbert's program then and now.Richard Zach - 2002 - In Dale Jacquette (ed.), Philosophy of Logic. Malden, Mass.: North Holland. pp. 411–447.
Representation and Reality by Language: How to make a home quantum computer?Vasil Penchev - 2020 - Philosophy of Science eJournal (Elsevier: SSRN) 13 (34):1-14.
A Mathematical Model of Quantum Computer by Both Arithmetic and Set Theory.Vasil Penchev - 2020 - Information Theory and Research eJournal 1 (15):1-13.
Peano arithmetic, games and descent recursion.Emanuele Frittaion - 2025 - Annals of Pure and Applied Logic 176 (4):103550.

View all 10 citations / Add more citations

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.
The substitution method.W. W. Tait - 1965 - Journal of Symbolic Logic 30 (2):175-192.
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.

View all 8 references / Add more references