Abstract
The story of Gentzen’s original consistency proof for first-order number theory [9], as told by Paul Bernays [1, 9], [11, Letter 69, pp. 76–79], is now familiar: Gentzen sent it off to Mathematische Annalen in August of 1935 and then withdrew it in December after receiving criticism and, in particular, the criticism that the proof used the Fan Theorem, a criticism that, as the references just cited seem to indicate, Bernays endorsed or initiated at the time but later rejected. That particular criticism is transparently false, but the argument of the paper remains nevertheless invalid from a constructive standpoint. In a letter to Bernays dated November 4, 1935, Gentzen protested this evaluation; but then, in another letter to him dated December 11, 1935, he admits that the ‘critical inference in my consistency proof is defective’.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
Could Bernays’ references to the “Fan Theorem,” all over 30 years later, have been the result of a confusion of the Fan Theorem with the Bar Theorem?
- 3.
See [2] for a detailed description of the relation between Gentzen’s 1938 consistency proof and Schütte’s 1951 result.
- 4.
The rule is, in itself, just a rule for constructing a certain tree—I call it a “pre-reduction rule” below. It is a reduction rule in virtue of the tree being well-founded. So, to know that A is true would mean, not simply to possess the rule, but also to know that the tree is well-founded. One might have some difficulty in labelling knowledge of this kind as “finitary.”
- 5.
That Gödel had anticipated the no-counterexample interpretation in these notes was first noticed by C. Parsons and W. Sieg in their introductory note.
- 6.
When in [7] he comes to the problem of determining the bound on the provable ordinals, he needs to essentially redo the argument for the case that the atomic formulas also include t ∈ V, where V stands for an indeterminate set of numbers and t a numerical term. But it is obvious how to treat this extension. The atomic sentences must be extended to include the expressions n ∈ V and the axiom sets, defined below, has to be extended to include sequents of the form \(\Gamma,n \in V \vdash n \in V\).
- 7.
It is not excluded that some premise of an inference is identical with the conclusion. Therefore, we have to distinguish the node of a deduction tree from the sequent attached to it. For simplicity, I have defined the nodes of deduction trees to be in general infinitary objects. The finitist will want to replace these with suitable codes.
References
P. Bernays, On the original Gentzen consistency proof for number theory, Intuitionism and Proof Theory, ed. by A. Kino, J. Myhill, R. Vesley (North-Holland, Amsterdam, 1970), pp. 409–418
W. Buchholz, Explaining Gentzen’s consistency proof within infinitary proof theory, in Computational Logic and Proof Theory. Fifth Kurt Gödel Colloquium, KGC ’97, ed. by G. Gottlob, A. Leitsch, D. Mundici. Lecture Notes in Computer Science, vol. 1298 Springer, Berlin (1997)
T. Coquand, A semantics of evidence for classical arithmetic. J. Symb. Log. 60, 325–337 (1995)
G. Gentzen, Untersuchungen über das logische Schliessen I, II. Math. Z. 39, 176–210, 405–431 (1935). English translation in [8, pp. 68–131]
G. Gentzen, Die Widerspruchfreiheit der reinen Zahlentheorie. Math. Ann. 112, 493–565 (1936) English translation in [8, pp. 132–213]
G. Gentzen, Nue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie, in Forschungen zur Logik und der Grundlagen der exakten Wissenschaften, New Series, No. 4 (1938), pp. 5–18. English translation in [8, pp. 252–286]
G. Gentzen, Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie. Math. Ann. 119, 140–161 (1943). English translation in [8, pp. 287–308].
G. Gentzen, The Collected Papers of Gerhard Gentzen (North-Holland, Amsterdam, 1969). Translated and edited by M. E. Szabo
G. Gentzen, Der erste Widerspruchsfreiheitsbeweis für die klassische Zahlentheorie. Archiv für Mathematische Logik und Grundlagenforschung 16, 97–118 (1974). Edited with a brief introduction by P. Bernays
K. Gödel, Lecture at Zilsel’s, in Collected Works, vol. III (Oxford University Press, Oxford, 1938), pp. 87–113.
K. Gödel, Collected Works, vol. IV (Oxford University Press, Oxford, 2003)
G. Kreisel, On the interpretation of non-finitist proofs—part i. J. Symb. Log. 16, 241–267 (1951)
G. Kreisel, On the interpretation of non-finitist proofs—part ii. interpretations of number theory, applications. J. Symb. Log. 17, 43–58 (1952)
P. Lorenzen, Algebraische und logistische Untersuchungen über freie Verbände. J. Symb. Log. 16, 81–106 (1951)
K. Schütte, Beweisetheoretische Erfassung der unendlichen Induktion in der Zahlentheorie. Math. Ann. 122, 369–389 (1951)
K. Schütte, Beweistheoretische Untersuchung der verzweigten Analysis. Math. Ann. 124, 123–147 (1952)
K. Schütte, Eine Grenze für die Beweisbarkeit der transfinitien Induction in der verzweigten Typenlogik. Archiv für mathematische Logik und Grundlagenforschung 7, 45–60 (1964)
W. Tait, Normal derivability in classical logic, in The Syntax and Semantics of Infinitary Languages, ed. by J. Barwise (Springer, Berlin, 1968), pp. 204–236
W. Tait, Gödel’s unpublished papers on foundations of mathematics. Philos. Math. 9, 87–126 (2001). Reprinted in [21], pp. 276–313
W. Tait, Gödel’s reformulation of Gentzen’s first consistency proof for arithmetic. Bull. Symb. Log. 11(2), 225–238 (2005)
W. Tait, The Provenance of Pure Reason: Essays in the Philosophy of Mathematics and Its History (Oxford University Press, Oxford, 2005)
Acknowledgements
My understanding of the philosophical background of Gentzen’s work on consistency was enhanced by reading the unpublished manuscript “On the Intuitionistic Background of Gentzen’s 1936 Consistency Proof and Its Philosophical Aspects” by Yuta Takahashi.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Tait, W.W. (2015). Gentzen’s Original Consistency Proof and the Bar Theorem. In: Kahle, R., Rathjen, M. (eds) Gentzen's Centenary. Springer, Cham. https://doi.org/10.1007/978-3-319-10103-3_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-10103-3_8
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10102-6
Online ISBN: 978-3-319-10103-3
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)