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.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 107,191

External links

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

Through your library

Similar books and articles

Decoding Gentzen's Notation.Luca Bellotti - 2018 - History and Philosophy of Logic 39 (3):270-288.
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
166 (#150,503)

6 months
6 (#856,013)

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, 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 11 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