Acting and Reflecting pp 171-182 | Cite as

# Reflections on Hilbert’s Program

## Abstract

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}

## Keywords

Proof Theory Intuitionistic Theory Generate Clause Consistency Proof Elementary Number Theory## Preview

Unable to display preview. Download preview PDF.

## Notes

- 1.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.Google Scholar - 2.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.Google Scholar - 3.Hobbes,
*De Corpore*, in particular the section “Computatio Sive Logica”, and Leibniz,*De Arte Combinatoria*. Google Scholar - 4.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.Google Scholar
- 5.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?Google Scholar
- 6a.See e.g., Kreisel, “A Survey of Proof Theory”,
*Journal of Symbolic Logic*33, 1968, pp. 321–388;CrossRefGoogle Scholar - 6b.Takeuti,
*Proof Theory*(Second edition), North Holland Publishing Company, Amsterdam 1987;Google Scholar - 6c.Feferman, “Theories of Finite Type related to Mathematical Practice”,
*Handbook of Mathematical Logic*, Amsterdam 1977, pp. 913–971;Google Scholar - 6d.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.Google Scholar - 7.Supplement IV (“Formalismen zur deduktiven Entwicklung der Analysis”) in volume II of
*Grundlagen der Mathematik*(Second edition), 1970.Google Scholar - 8a.Most important, apart from the work of Brouwer’s, are two books: Weyl,
*Das Kontinuum*, Leipzig, 1918;Google Scholar - 8b.Bishop,
*Foundations of Constructive Analysis*, New York, 1967.Google Scholar - 9a.Takeuti,
*Two Applications of Logic to Mathematics*, Princeton, 1978;Google Scholar - 9b.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.Google Scholar - 10.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.Google Scholar
- 11.That is a result of Gödel and Gentzen mentioned below.Google Scholar
- 12.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.Google Scholar - 13.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.Google Scholar - 14.Hilbert, “On the Infinite”, in: van Heijenoort, l.c., p. 376.Google Scholar
- 15.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.Google Scholar - 16a.Kreisel, “Mathematical Logic”, in:
*Lectures on Modern Mathematics*, vol.III, Saaty (ed.), New York, 1965, pp. 95–195, in particular, pp. 168–173.Google Scholar - 16b.Parsons, “Intuition in Constructive Mathematics”, in:
*Language, Mind, and Logic*(Butterfield, ed.), Cambridge University Press, 1986, and other papers referred to there;Google Scholar - 16c.Tait, “Finitism”,
*Journal of Philosophy*78, 1981, pp. 524–546.CrossRefGoogle Scholar - 17.Bernays, “Die schematische Korrespondenz und die idealisierten Strukturen”, reprinted in the volume of essays mentioned in
^{15}, 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.Google Scholar - 18.Gödel, “Eine bisher noch nicht benützte Erweiterung des finiten Standpunktes”,
*Dialectica*12 (1958), pp. 280–287.CrossRefGoogle Scholar - 19.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.Google Scholar
- 20.That is quoted from Reid, l.c., p. 218.Google Scholar
- 21.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.Google Scholar