Gödel's Reformulation of Gentzen's First Consistency Proof For Arithmetic: The No-Counterexample Interpretation
W. W. Tait · Bulletin of Symbolic Logic · 2005
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 forPA[8], reformulating it as what has come to be called theno-counterexample interpretation. I will describe Gentzen's result (in game-theoretic terms), fill in the details (with some corrections) of Gödel's reformulation, and discuss the relation between the two proofs.