The Finite and the Infinite: On Hilbert’s Formalist Approach Before and After Gödel’s Incompleteness Theorems

Matthias Schirn


In this essay, I discuss formalist and finitist aspects of Hilbert’s proof-theoretic programme in the 1920s and 1930s. I begin by pointing out some difficulties arising from his construction of intuitive number theory in his first paper on metamathematics in the 1920s and by characterizing the nature of his metamathematics. In what follows, I argue thatHilbert’s paradigm of a transfinite axiom as well as the other “ordinary” transfinite axioms derivable from it fail to supply any formal explication of the term “infinite” or “transfinite”. On the one hand, Hilbert regards both the mathematical and the logical signs as detached from all meaning once the process of formalization of contentual mathematics has been completely carried out. On the other hand, there are several places where he characterizes the finitary or real sentences of the language of formalized arithmetic, in contrast to its transfinite or ideal sentences, expressly as meaningful. I make a proposal to explain why for Hilbert it might still be of interest to be able to rely on meaningful sentences in the language of formalized arithmetic. In section 5, I critically discuss several aspects in Hilbert and Bernays’s extension of the finitist point of view in the second volume of Foundations of Mathematics(1939). In section 6, I argue that by appreciating the distinctive character of the notion of an “approximative” consistency proof we can make good sense of the nature of the consistency proofs that Hilbert outlines both in his classical papers on proof theory in the 1920s and in the first volume of Foundations of Mathematics (1934).I further argue that a weak version of Hilbert’s programme is compatible with Gödel’s second incompleteness theorem by using only what are clearly natural provability predicates.


Ackermann, W.: 1925, ‘Begründung des “tertium non datur” mittels der Hilbertschen Theorie der Widerspruchsfreiheit’, Mathematische Annalen 93, 1-36.

Ackermann, W.: 1940 ‘Zur Widerspruchsfreiheit der Zahlentheorie’, Mathematische Annalen 117, 162-194.

Bernays, P.: 1935, ‘Hilberts Untersuchungen über die Grundlagen der Arithmetik’, in Hilbert 1935, 196-216.

Buchholz, W.: 2015, ‘On Gentzen’s First Consistency Proof for Arithmetic’, in Kahle & Rathjen, 63-87.

Cantor, G.: 1932, Gesammelte Abhandlungen mathematischen und philosophischen Inhalts. editor E. Zermelo, Berlin 1932; reprint Georg Olms Verlagsbuchhandlung, Hildesheim 1966.

Craig, W.: 1953, ‘On Axiomatizability Within a System’, The Journal of Symbolic Logic 18, 30-32.

Detlefsen, M.: 1986, Hilbert’s Program. An Essay on Mathematical Instrumentalism, Reidel, Dordrecht.

Feferman, S.: 1960, ‘Arithmetization of Metamathematics in a General Setting’, Fundamenta Mathematicae XLIX, 35-92.

Feferman, S.: 1988, ‘Hilbert’s Program Relativized: Proof-Theoretical and Foundational Reductions’, The Journal of Symbolic Logic 53, 364-383.

Ewald, W. B. & Sieg W. (editors): 2013, David Hilbert’s Lectures on the Foundations of Arithmetic and Logic, 1917 to 1933, Springer, Heidelberg.

Ganea, M.: 2010. ‘Two (or Three) Notions of Finitism’. The Review of Symbolic Logic 3, 119–144.

Gentzen, G.: 1936, ‘Die Widerspruchsfreiheit der reinen Zahlentheorie’, Mathematische Annalen 112, 493-565.

Gentzen. G.: 1938, ‘Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie’, Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften 4, 19-44.

Gentzen, G.: 1943, ‘Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie’, Mathematische Annalen 119, 140-161.

Gentzen, G.: 1969, The Collected Papers of Gerhard Gentzen, editor M. E. Szabo, North-Holland, Amsterdam.

Gödel, K.: 1931, ‘Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I’. Monatshefte für Mathematik und Physik 38, 173-198; German original and English translation in Gödel 1986, 144-195.

Gödel, K.: 1958, ‘Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes’, Dialectica 12, 280-287; German original and English translation in Gödel 1986, 240-251.

Gödel, K.: 1986, Collected Works, vol. I, Publications 1929-1936, editors S. Feferman, J. Dawson, S. C. Kleene, G. Moore, R. M. Solovay & J. van Heijenoort, Oxford University Press, Oxford.

Herbrand, J.: 1931, ‘Sur la non-contradiction de l’arithmétique’, Journal für die reine und angewandte Mathematik 166, 1-8. English translation in From Frege to Gödel. A Source Book in Mathematical Logic, 1879-1931, editor J. van Heijenoort, Harvard University Press, Cambridge, MA, 1967, 618-628.

Hilbert, D.: 1899, Grundlagen der Geometrie, Teubner, Leipzig; seventh revised and enlarged edition 1930.

Hilbert, D.: 1922 ‘Neubegründung der Mathematik’, Erste Mitteilung, Abhandlungen aus dem mathematischen Seminar der Hamburger Universität, 1, 157-177.

Hilbert, D.: 1923, ‘Die logischen Grundlagen der Mathematik’, Mathematische Annalen 88, 151-165; reprinted in Hilbert 1964, 33-46 (and in Hilbert 1935, vol. III, 178-191).

Hilbert, D.: (1926): ‘Über das Unendliche’, Mathematische Annalen 95, 161-190; reprinted in Hilbert 1964, 79-108.

Hilbert, D.: 1928, ‘Die Grundlagen der Mathematik’, Abhandlungen aus dem Mathemati- schen Seminar der hamburgischen Universität 6, 65-85; reprinted as appendix IX of Hilbert 1899, seventh edition, 289-312.

Hilbert, D.: 1931, ‘Die Grundlegung der elementaren Zahlenlehre’, Mathematische Annalen 104, 484-494 (abbreviated version in Hilbert 1935, vol. III, 192-195; complete English translation in Mancosu 1998, 266-273).

Hilbert, D. and Bernays, P.: 1934, Grundlagen der Mathematik, vol. I, Springer Verlag, Berlin, Heidelberg, New York, second edition with modifications and supplementations, 1968.

Hilbert, D.: 1935, Gesammelte Abhandlungen, vol. III, Springer Verlag, Berlin, Heidelberg, New York, 1935, 1970.

Hilbert, D. and Bernays, P.: 1939, Grundlagen der Mathematik, vol. II, Springer Verlag, Berlin, Heidelberg, second edition with modifications and supplementations, 1970.

Hilbert, D.: 1964, Hilbertiana. Fünf Aufsätze, Wissenschaftliche Buchgesellschaft, Darmstadt.

Ignjatovic, A.: 1994, ‘Hilbert’s Program and the Omega-Rule’, The Journal of Symbolic Logic 59, 322-343.

Incurvati, L.: 2015, ‘On the Concept of Finitism’, Synthese 192, 2413-2436.

Isaacson, D.: 1992, ‘Some Considerations on Arithmetical Truth and the ω-Rule’, in M. Detlefsen (editor), Proof, Logic and Formalization, Routledge, London, 94-138.

Kahle, R. & Rathjen, M., editors: 2015, Gentzen’s Centenary. The Quest for Consistency, Springer.

Kahle, R.: 2015, ‘Gentzen’s Consistency Proof in Context’, in Kahle & Rathjen 2015, 3-24.

Kant, I.: 1781/1787, Kritik der reinen Vernunft (KrV), editor R. Schmid, Felix Meiner, Hamburg 1956.

Kaye, R.: 1991, Models of Peano Arithmetic, Oxford University Press, Oxford.

Kikuchi, M. and Kurahashi, T.: 2017, ‘Generalizations of Gödel’s Incompleteness Theorems for n-Definable Theories’, The Review of Symbolic Logic 10, 603-616.

Kohlenbach, U.: 2008, Applied Proof Theory: Proof Interpretations and their Use in Mathematics, Springer Monographs in Mathematics, Springer, Berlin, Heidelberg.

Kreisel, G.: 1958, ‘Hilbert’s Programme’, Dialectica 12, 346-372; revised version in Philosophy of Mathematics. Selected Readings, editors P. Benacerraf & H. Putnam, Cambridge University Press, Cambridge 1964, second edition 1983, 207-238.

Löb, M.: 1955, ‘Solution to a Problem of Leon Henkin’, The Journal of Symbolic Logic 20, 115-118.

Mancosu, P.: 1998, From Brouwer to Hilbert. The Debates on the Foundations of Mathematics in the 1920s, Oxford University Press, Oxford.

Mancosu, P.: 2015, ‘Essay Review of W. Ewald and W. Sieg, editors, David Hilbert’s Lectures on the Foundations of Mathematics, Springer, 2013, Philosophia Mathematica 23, 126-135.

Niebergall, K.-G.: 1996, Zur Metamathematik nichtaxiomatisierbarer Theorien, University of Munich, CIS.

Niebergall, K.-G. & Schirn, M.: 1998, ‘Hilbert’s Finitism and the Notion of Infinity’, in Schirn 1998, 271-305.

Niebergall, K.-G. & Schirn, M.: 2002, ‘Hilbert’s Programme and Gödel’s Theorems’, Dialectica 56, 347-370.

Niebergall, K.-G.: 2005, ‘Natural Representations and Extensions of Gödel’s Second Theorem’, in Logic Colloquium ’01, editors M. Baaz & S. D. Friedman, Association for Symbolic Logic, Urbana, IL and Wellesley, MA, 350–368.

Niebergall, K.-G.: 2014, ‘Assumptions of Infinity’, in Formalism and Beyond. On the Nature of Mathematical Discourse, editor G. Link, Walter de Gruyter, Boston, Berlin, 229-274.

Parsons, C. : 1998, ‘Finitism and Intuitive Knowledge’, in Schirn 1998, 247-270.

Parsons, C.: 2008, Mathematical Thought and Its Objects, Cambridge University Press, Cambridge.

Peckhaus, V.: 1990, Hilbertprogramm und kritische Philosophie. Das Göttinger Modell interdisziplinärer Zusammenarbeit zwischen Mathematik und Philosophie, Vandenhoeck & Ruprecht, Göttingen.

Peckhaus, V.: 1994, ‘Hilbert’s Axiomatic Programme and Philosophy”, in The History of Modern Mathematics, vol. 3: Images, Ideas, and Communities, editors E. Knobloch and D. E. Rowe, Academic Press, Boston 1994, 91–112.

Prawitz, D.: 2015, ‘A Note on How to Extend Gentzen’s Second Consistency Proof to a Proof of Normalization for First Order Arithmetic’, in Kahle & Rathjen 2015, 131-176.

Rosser, J. B.: 1936, ‘Extensions of Some Theorems of Gödel and Church’, The Journal of Symbolic Logic 1, 87-91.

Schirn, M.: 1998, The Philosophy of Mathematics Today, Oxford University Press, Oxford.

Schirn, M. & Niebergall, K.-G.: 2001, ‘Extensions of the Finitist Point of View’, History and Philosophy of Logic 22 , 135-161.

Schirn, M. & Niebergall, K.-G.: 2003, ‘What Finitism Could Not Be’, Crítica 35, 43-68.

Schirn, M. & Niebergall, K.-G.: 2005, ‘Finitism = PRA? On a Thesis of W.W. Tait, Reports on Mathematical Logic 39, 3-24.

Schirn, M.: 2010, ‘Consistency, Models, and Soundness’, Axiomathes 20, 153-207.

Sieg, W.: 1999, ‘Hilbert’s Programs: 1917-1922’, The Bulletin of Symbolic Logic 5, 1–44. Sieg, W.: 2009, ‘Hilbert’s Proof Theory’, in Handbook of the History of Logic, vol. 5, editors D. M. Gabbay & J. Wood, Elsevier, North-Holland, Amsterdam, Boston, 321-384.

Sieg, W.: 2013, Hilbert’s Programs and Beyond, Oxford University Press, Oxford.

Sieg, W.: 2016, ‘On Tait on Kant and Finitism’, The Journal of Philosophy 113, 274-285.

Simpson, S. G.: (1988), ‘Partial Realizations of Hilbert’s Program’, The Journal of Symbolic Logic 53, 349-363.

Smorynski, C.: 1977, ‘The Incompleteness Theorems’, in Handbook of Mathematical Logic, editor J. Barwise, North-Holland, Amsterdam, 821-865.

Stenlund, S.: 2012, ‘Different Senses of Finitude: An Inquiry into Hilbert’s Finitism’, Synthese 185, 335-363.

Tait, W. W.: 1981, ‘Finitism‘, The Journal of Philosophy 78, 524-546.

Tait, W. W.: 2002, ‘Remarks on Finitism’, in Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, Lecture Notes in Logic 15, editors W. Sieg, R. Sommer & C. Talcott. A. K. Peters and the Association for Symbolic Logic, Wellesley, MA.

Tait, W.W.: 2010, ‘Gödel on Intuition and Hilbert’s Finitism’, in Kurt Gödel: Essays for His Centenial, editors S. Feferman, C. Parsons & S. Simpson. Cambridge, Association for Symbolic Logic, Lecture Notes in Logic, vol. 33, 88-108.

Tait, W.W.: 2015, ‘Gentzen’s Original Consistency Proof and the Bar Theorem’, in Kahle & Rathjen 2015, 213-228.

Tait, W. W.: 2016, ‘Kant and Finitism’, The Journal of Philosophy 113, 261-273.

Van Bendegem, J. P.: 2012, ‘A Defence of Strict Finitism’, Constructivist Foundations 7, 141-149.

Von Neumann, J.: 1927, ‘Zur Hilbertschen Beweistheorie’, Mathematische Zeitschrift 26, 1-46.

Von Neumann, J.: 2005, Selected Letters, editor M. Rédei, History of Mathematics, vol. 27, American Mathematical Society, London Mathematical Society.

Von Plato, J.: 2009, ‘Gentzen’s Logic’, in Handbook of the History of Logic, vol. 5, editors D. M. Gabbay & J. Wood, Elsevier North-Holland, Amsterdam, Boston, 667-721.

Zach, R.: 2001, Hilbert’s Finitism: Historical, Philosophical and Mathematical Perspectives, PhD thesis, University of California, Berkeley.

Zach, R.: 2006, ‘Hilbert’s Program Then and Now’, in Handbook of the Philosophy of Science, vol. 5, Philosophy of Logic, editors D. M. Gabbay and J. Wood, Elsevier North-Holland, Amsterdam, Boston, 411-447.

Zermelo, E.: 1904, ‘Beweis, daß jede Menge wohlgeordnet werden kann’, Mathematische Annalen 59, 514-516.

Zermelo, E.: 1908, ‘Neuer Beweis für die Möglichkeit einer Wohlordnung’, Mathematische Annalen 65, 107-128.


  • There are currently no refbacks.