Hilbert wanted to solve those problems via his proof theory. His proposal to carry out the program consisted of two steps: 1. to formalize mathematics, i.e., to reconstruct infinitistic mathematics as a big, elaborate formal system and 2. to give a proof of the consistency and conservativeness of mathematics. It should be done by finitistic methods, and it was possible since after formalization one could treat formulas of the system of mathematics as strings of symbols and proofs as strings of formulas (i.e., as strings of strings of symbols).
Incompleteness results
Hilbert and his school had scored some successes in realization of the program of justification of infinite mathematics. In particular, Hilbert’s student W. Ackermann showed by finitistic methods the consistency of a fragment of arithmetic of natural numbers (cf. Ackermann 1924–1925, 1940). But soon, something was to happen that undermined Hilbert’s program.
We mean here the incompleteness results of Gödel from 1930 which indicated certain cognitive limitations of the deductive methods (cf. Gödel 1931). They showed that one cannot include the whole mathematics in a consistent formalized system based on the first order predicate calculus – what more, one cannot even include in such a system all truth about natural numbers. Even more, no formal theory containing arithmetic of natural numbers can prove its own consistency.
Gödel’s results struck Hilbert’s program. The question whether they rejected it cannot be answered definitely. The reason is that Hilbert’s program was not formulated precisely enough. Hence, various opinions are formulated and defended (cf., e.g. Detlefsen 1979, 1990; Resnik 1974; Smorynski 1977, 1985, 1988). But one thing ←13 | 14→should be stressed here: the failure of Hilbert’s programme for a certain formalized system of arithmetic need not be a failure of Hilbert’s programme for elementary number theory in the informal sense. In fact, one cannot exclude the possibility that the latter can be formalized in a system which can be justified on finitistic grounds.5
Gödel’s true but undecidable (in the formal system of arithmetic) sentence had not mathematical but in fact metamathematical contents (it states: “I am not a theorem”). This diminished the meaning and significance of Gödel’s results. There arose a question: Is it possible to indicate examples of true undecidable sentences of mathematical, in particular number–theoretical, contents? Or formal mathematics is complete with respect to sentences which are interesting and reasonable from the mathematical point of view (whatever it means)?
These questions were answered by J. Paris, L. Harrington and L. Kirby who gave examples of true undecidable sentences of combinatorial contents (cf. Paris and Harrington 1977) and of number–theoretical contents (cf. Kirby, Paris 1982). They are examples of true arithmetical sentences without “pure”, i.e., arithmetical proofs. More exactly, we got sentences talking about some combinatorial properties of finite sets or properties of sequences of natural numbers but natural proofs of them use infinite sets and, since they cannot be proved in Peanoarithmetic PA, each such proof must contain something from beyond the domain of finite objects. Thus they are theorems having “impure” but no “pure” proofs.
Add that those results were used by quasi-empiricists in mathematics who argue that mathematics is not an a priori knowledge, it is not absolute and certain, but is rather quasi-empirical, probable and fallible; mathematics is in fact similar to natural sciences. The new undecidable results indicate also that, as E. Post put it, “mathematical proof is in fact a result of creative activity of reason”, it is impossible to bound a priori the invention of a mathematician.
←14 | 15→
Generalized Hilbert’s program
The natural consequence of incompleteness results was the idea of extending the admissible methods and allowing general constructive methods instead of finitistic ones only6. This led to the generalized Hilbert’s program.
Though the concept of general constructive methods is unprecise, still the idea of broadening of original Hilbert’s proof theory has become an accepted paradigm. Investigations were carried out in this direction, and several results were obtained (cf. Feferman 1988; Feferman 1964–1968; Gödel 1958; Kreisel 1958; Schütte 1977; Simpson 1985; Takeuti 1987). We want to note here only that they led to two surprising insights: (a) classical analysis can be formally developed in conservative extensions of elementary number theory and (b) strong impredicative subsystems of analysis can be reduced to constructively meaningful theories, i.e., relative consistency proofs can be given by constructive means for impredicative parts of second order arithmetic.
On the other hand, it should be stressed that all the proposed generalizations of Hilbert’s program, are in fact very different from the original Hilbert’s proposal. Hilbert’s postulate was the validation and justification of classical mathematics by a reduction to finitistic mathematics. The latter was important here for philosophical and, say, ideological reasons: finitistic objects and reasonings have clear physical meaning and are indispensable for all scientific thought. None of the proposed generalizations can be viewed as finitistic (whatever it means). Hence they have another value and meaning from the methodological and generally philosophical point of view. They are not contributing directly to Hilbert’s program, but on the other hand they are in our opinion compatible with Hilbert’s reductionist philosophy.
Reverse mathematics vs. Hilbert’s program
Another consequence of incompleteness results (besides those described above) is so-called relativized Hilbert’s program. If the entire infinitistic mathematics cannot be reduced to and justified by finitistic mathematics then one can ask for which part of it is that possible? In other words:Howmuch of infinitistic mathematics can ←15 | 16→be developed within formal systems which are conservative over finitistic mathematics with respect to real sentences? This constitutes the relativized version of Hilbert’s program. In what follows, we would like to show how the so-called reverse mathematics of Friedman and Simpson contributes to it, providing us with a partial realization of Hilbert’s original program.
To be able to consider the issue we should first specify what is exactly meant by finitistic mathematics and by real sentences. We shall follow Tait (1981) where it is claimed that Hilbert’s finitism is captured by the formal system of primitive recursive arithmetic7 (PRA, also called Skolem arithmetic). By real sentences we shall mean Πsentences of the language of Peano arithmetic PA.
It turns out that one can formalize classical mathematics not only in set theory, but most of its parts (such as geometry, number theory, analysis, differential equations, complex analysis, etc.) can be formalized in a weaker system called second order arithmetic
1 axioms of PA without the axiom scheme of induction,
2 (extensionality)