Abstract
Hilbert’s Program deals with the foundations of mathematics from a very special perspective; a perspective that stems from Hubert’s answer to the question “What Is Mathematics?”. The popular version of his “formalist” answer, radical at Hubert’s time and shocking to thoughtful mathematicians even today, is roughly this: the whole “thought-content” of mathematics can be uniformly expressed in a comprehensive formal theory, mathematical activity reduces to the manipulation of symbolic expressions, and mathematics itself is just “ein Formelspiel”. Hubert defended his “playful” view of mathematics against intuitionistic attack by remarking:
The formula game that Brouwer so deprecates has, besides its mathematical value, an important general philosophical significance. For this formula game is carried out according to certain definite rules, in which the Technique of Our Thinking is expressed. These rules form a closed system that can be discovered and definitively stated. The fundamental idea of my proof theory is none other than to describe the activity of our understanding, to make a protocol of the rules according to which our thinking actually proceeds. Thinking, it so happens, parallels speaking and writing: we form statements and place them one behind the another. If any totality of observations and phenomena deserves to be made the object of serious and thorough investigation, it is this one—...1
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Notes
Hubert , “Die Grundlagen der Mathematik” (1927) This paper was presented to the Mathematical Seminar in Hamburg in July 1927; it was published in: Abhandlungen aus dem mathematischen Seminar der Hamburgischen Universität 6 (1928), pp. 65–85. A translation can be found in van Heijenoort (ed.), From Frege to Gödel, Cambridge, 1967, 464–479.—Incidentally, it was Hubert who provoked— by the very formulation of the Entscheidungsproblem for predicate logic—Church’s and Turing’s work on computability, work that is central in theoretical computer science.
Those foundational issues go back to the 19th century and were discussed, in particular, during the seventies and eighties. A brief account of this history is given in my paper “Foundations for Analysis and Proof Theory”, Synthese 60(2), 1984, 159–200.
Hobbes, De Corpore, in particular the section “Computatio Sive Logica”, and Leibniz, De Arte Combinatoria.
On the more psychological side Bernays reports in C. Reid’s Hubert biography (pp. 173–174): For Hubert’s program… experiences out of the early part of his scientific career (in fact, even out of his student days) had considerable significance; namely, his resistance to Kronecker’s tendency to restrict mathematical methods and, particularly, set theory.… In addition, two other motives were in opposition to each other—both strong tendencies in Hilbert’s way of thinking. On one side, he was convinced of the soundness of existing mathematics; on the other side, he had—philosophically—a strong scepticism.… The problem for Hubert… was to bring together these opposing tendencies, and he thought that he could do this through the method of formalizing mathematics.
You may ask, can this instrumentalism (radical formalism) be reconciled with Hubert’s view of the soundness (and meaningfulness) of mathematics? My answer is “YES, somewhat plausibly, if the formal theories under consideration are complete.”—The notion of completeness figures already significantly in Hubert’s earliest foundational paper “Über den Zahlbegriff” (1899). The formalisms for elementary number theory and analysis set up in the twenties were believed to be complete in the Hubert school. If a formalism allows then, as Hilbert put it, “to express the whole content of mathematics in a uniform way”, and if it provides “a picture of the whole science”, why not make a bold methodological turn and avoid all the epistemological problems connected with the (classical treatment of the) infinite?
See e.g., Kreisel, “A Survey of Proof Theory”, Journal of Symbolic Logic 33, 1968, pp. 321–388;
Takeuti, Proof Theory (Second edition), North Holland Publishing Company, Amsterdam 1987;
Feferman, “Theories of Finite Type related to Mathematical Practice”, Handbook of Mathematical Logic, Amsterdam 1977, pp. 913–971;
Buchholz, Feferman, Pohlers, Sieg, “Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies”, Springer Lecture Notes in Mathematics 897, Berlin, Heidelberg, New York 1981.
Supplement IV (“Formalismen zur deduktiven Entwicklung der Analysis”) in volume II of Grundlagen der Mathematik (Second edition), 1970.
Most important, apart from the work of Brouwer’s, are two books: Weyl, Das Kontinuum, Leipzig, 1918;
Bishop, Foundations of Constructive Analysis, New York, 1967.
Takeuti, Two Applications of Logic to Mathematics, Princeton, 1978;
Feferman, l.c., see 6; Friedman, “A Strong Conservative Extension of Peano Arithmetic”, in: The Kleene Symposium, (Barwise, Keisler, Kunen, eds.), Amsterdam, 1980, pp. 113–122.
A (set existence) principle is called impredicative if sets, whose existence is guaranteed by the principle, are given by formulas involving quantifiers the range of which includes those very sets.
That is a result of Gödel and Gentzen mentioned below.
This distinction between foundational and computational reduction is elaborated in Sieg, “Reductions of Theories for Analysis”, in: Foundations of Logic and Linguistics, (Dorn and Weingartner, eds.), New York, 1985, pp. 199–231. There is also a discussion of the (mainly mathematical) interest of reductions of the second type.
For the detailed description of these theories I have to refer to the literature, e.g., the Lecture Notes volume listed in 6.—The reference below is to Gödel’s “Russell’s Mathematical Logic”, reprinted in Benacerraf and Putnam’s collection of selected readings Philosophy of Mathematics, Cambridge University Press, Second Edition, 1983, p. 456.
Hilbert, “On the Infinite”, in: van Heijenoort, l.c., p. 376.
Bernays, “Die Philosophie der Mathematik und die Hilbertsche Beweistheorie”, published in 1930 and reprinted in Abhandlungen zur Philosophie der Mathematik, Darmstadt, 1976, pp. 17–61, especially p. 40.
Kreisel, “Mathematical Logic”, in: Lectures on Modern Mathematics, vol.III, Saaty (ed.), New York, 1965, pp. 95–195, in particular, pp. 168–173.
Parsons, “Intuition in Constructive Mathematics”, in: Language, Mind, and Logic (Butterfield, ed.), Cambridge University Press, 1986, and other papers referred to there;
Tait, “Finitism”, Journal of Philosophy 78, 1981, pp. 524–546.
Bernays, “Die schematische Korrespondenz und die idealisierten Strukturen”, reprinted in the volume of essays mentioned in15, p. 186. This paper was published originally in 1970. I should mention that essentially the same view is expressed in Bernays’s 1930 paper mentioned above; except, that the finitist standpoint is taken as “absolute”. After the discussion of completeness (“deduktive Abgeschlossenheit”) inclusive a footnote stating (incorrectly, as we know) that completeness of a formal theory is not as far reaching as its decidability, we read (on p. 59): Im Gebiete dieser und verwandter Fragen liegt noch ein beträchtliches Feld der Problematik offen. Diese Problematik ist aber nicht von der Art, daß sie eine Einwendung gegen den von uns eingenommenen Standpunkt darstellt. Wir müssen uns nur gegenwärtig halten, daß der Formalismus der Sätze und Beweise, mit denen wir unsere Ideenbildung zur Darstellung bringen, nicht zusammenfällt mit dem Formalismus derjenigen Struktur, die wir in der Gedankenbildung intendieren. Der Formalismus reicht aus, um unsere Ideen von unendlichen Mannigfaltigkeiten zu formulieren, aber er vermag im allgemeinen nicht, die Mannigfaltigkeit gleichsam aus sich kombinatorisch zu erzeugen.
Gödel, “Eine bisher noch nicht benützte Erweiterung des finiten Standpunktes”, Dialectica 12 (1958), pp. 280–287.
There is a genuine conceptual problem for attempts to extend the reductive work concerning impredicative subsystems of analysis beyond the strongest system that has been treated: i.d. classes are provably not sufficient. We have to find a new, broader concept of “constructive mathematical object”, if there is to be any prospect for genuine advances.
That is quoted from Reid, l.c., p. 218.
One has to keep in mind that for Hubert there was only one constructive mathematics, as finitist and intuitionist mathematics were assumed to be coextensive.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1990 Kluwer Academic Publishers
About this chapter
Cite this chapter
Sieg, W. (1990). Reflections on Hilbert’s Program. In: Sieg, W. (eds) Acting and Reflecting. Synthese Library, vol 211. Springer, Dordrecht. https://doi.org/10.1007/978-94-009-2476-5_12
Download citation
DOI: https://doi.org/10.1007/978-94-009-2476-5_12
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-010-7617-3
Online ISBN: 978-94-009-2476-5
eBook Packages: Springer Book Archive