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)


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.

Download options


    Upload a copy of this work     Papers currently archived: 72,805

External links

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

Through your library


Added to PP

121 (#99,393)

6 months
1 (#386,031)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

William W. Tait
University of Chicago

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

View all 9 references / Add more references