Hostname: page-component-586b7cd67f-t7czq Total loading time: 0 Render date: 2024-11-23T20:32:35.400Z Has data issue: false hasContentIssue false
  • English
  • Français

Gödel's Reformulation of Gentzen's First Consistency Proof For Arithmetic: The No-Counterexample Interpretation

Published online by Cambridge University Press:  15 January 2014

W. W. Tait
W. W. Tait*
Affiliation:
5522 S. Everett Ave., Chicago, Il 60637, USAE-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

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 PA [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 Gödel's reformulation, and discuss the relation between the two proofs.

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 11 , Issue 2 , June 2005 , pp. 225 - 238
Copyright
Copyright © Association for Symbolic Logic 2005

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Ackermann, W., Zur Widerspruchsfreiheit der Zahlentheorie, Mathematische Annalen, vol. 117 (1940), pp. 162–194.Google Scholar
[2] Avigad, J., Update procedures and the 1-consistency of arithmetic, Mathematical Logic Quarterly, vol. 48 (2002), pp. 3–13.Google Scholar
[3] Bernays, P., On the original Gentzen-Takeuti reduction steps, Institutionism and proof theory (Kino, A., Myhill, J., and Vesley, R., editors), North-Holland, Amsterdam, 1970, pp. 409–418.Google Scholar
[4] Buchholz, W., Explaining the Gentzen-Takeuti reduction steps, Archive for Mathematical Logic, vol. 40 (2001), pp. 255–272.Google Scholar
[5] Coquand, T., A semantics of evidence for classical arithmetic, The Journal of Symbolic Logic, vol. 60 (1995), pp. 325–337.Google Scholar
[6] Dekker, J. (editor), Recursive function theory, Proceedings of Symposia in Pure Mathematics, vol. 5, American Mathematical Society, Providence, 1962.Google Scholar
[7] Feferman, S., Dawson, J. W., Goldfarb, W., Parsons, C., and Solovay, R. M. (editors), Kurt Godel: Collected works, Vol. III, Oxford University Press, Oxford, 1995.CrossRefGoogle Scholar
[8] Gentzen, G., Die Widerspruchfreheit der reinen Zahlentheorie, Mathematische Annalen, vol. 112 (1936), pp. 493–565.Google Scholar
[9] Gödel, K., Lecture at Zilsel's, In Feferman, et al. [7], pp. 87–133.Google Scholar
[10] Hilbert, D., Die Grundlegung der elementaren Zahlenlehre, Mathematische Annalen, vol. 104 (1930), pp. 485–565, Reprinted in part in [11].Google Scholar
[11] Hilbert, D., Gesammelte Abhandlungen, vol. 3, Springer, Berlin, 1935.Google Scholar
[12] Kohlenbach, U., On the no-counterexample interpretation, The Journal of Symbolic Logic, vol. 64 (1999), pp. 1491–1511.Google Scholar
[13] Kreisel, G., On the interpretation of non-finitist proofs-Part I, The Journal of Symbolic Logic, vol. 16 (1951), pp. 241–267.Google Scholar
[14] Menzler-Trott, E., Gentzens Problem: Mathematische Logik im nationalsozialistischen Deutschland, Birkhauser Verlag, Basel, 2001.Google Scholar
[15] Schütte, K., Beweisetheoretische Erfassung der unendlichen Induktion in der Zahlentheorie, Mathematische Annalen, vol. 122 (1951), pp. 369–389.Google Scholar
[16] Spector, C., Provably recursive functionals of analysis: a consistency proof of analysis by an extension of the principles formulated in current intuitionistic mathematics, In Dekker, [6], pp. 1–27.Google Scholar
[17] Tait, W. W., Functionals definedby transfinite recursion, The Journal of Symbolic Logic, vol. 30 (1965), pp. 155–174.Google Scholar
[18] Tait, W. W., The substitution method, The Journal of Symbolic Logic, vol. 30 (1965), pp. 175–192.Google Scholar
[19] Tait, W. W., Gödel's unpublished papers on foundations of mathematics, Philosophia Mathematica, vol. 9 (2001), pp. 87–126.Google Scholar
[20] Tait, W. W., The no counterexample interpretation for arithmetic, unpublished manuscript.Google Scholar