A Precise Explication of Hilbert's Program

Hilbert's Program was only that: a program or proposed course of
action. Let us now ask: *To what extent can the program be
carried out?* In order to study this question fruitfully, one must
reformulate the program in more precise terms. I shall now do this.

Hilbert's description of the ``big system,'' corresponding to
infinitistic mathematics, is already sufficiently precise. For my
purposes here I shall identify the big system as *Z*_{2}, *i.e.*
*second order arithmetic*. Supplement IV of Hilbert and Bernays
[15] shows that *Z*_{2} is more than adequate for the formal
development of classical analysis, etc. It would not matter if we
replaced *Z*_{2} by *Z*_{3}, *Z*_{4}, or even ZFC.

The unacceptable imprecision occurs in Hilbert's discussion of finitism. There is room for disagreement over exactly which methods Hilbert would have allowed as finitistic. This is not a defect in Hilbert's presentation. Hilbert's plan was to carry out a consistency proof which would be obviously finitistic. Had the plan been completely successful, there would have been no need for a precise specification of the outer limits of finitism.

At this point I invoke the work of Tait [25]. Tait argues
convincingly that Hilbert's finitism is captured by the formal system
PRA of *primitive recursive arithmetic* (also known as
*Skolem arithmetic*). This conclusion is based on a careful
study of what Hilbert said about finitism in [13,14] and
elsewhere. There seems to be a certain naturalness about PRA which
supports Tait's conclusion. PRA is certainly finitistic and
``logic-free'' yet sufficiently powerful to accommodate all elementary
reasoning about natural numbers and manipulations of finite strings of
symbols. PRA seems to embody just that part of mathematics which
remains if we excise all infinitistic concepts and modes of reasoning.
For my purposes here I am going to accept Tait's identification of
finitism with PRA.

I have now specified the precise version of steps 2.1 and 2.2 of
Hilbert's Program. Step 2.3 is then to show that the consistency of
the formal system *Z*_{2} can be proved within the formal system PRA.
If this could be done, it would follow that every
sentence
which is provable in *Z*_{2} would also be provable in PRA. We would
describe this state of affairs by saying that * Z_{2} is
conservative over PRA with respect to
sentences*. This
would constitute a precise and definitive realization of Hilbert's
Program.

Unfortunately, Gödel's Theorem [9] shows that any such
realization of step 2.3 is impossible. There are plenty of sentences which are provable in *Z*_{2} but not in PRA. (An example of
such a sentence is the one which asserts the consistency of the formal
system *Z*_{1} of first order arithmetic. Other examples, with a more
combinatorial flavor, have been given by Friedman.)

Note that Gödel's Theorem does not challenge the correctness of Hilbert's formalization of infinitistic mathematics, nor does it undercut Tait's identification of finitistic mathematics with PRA. Gödel's accomplishment is merely to show that the wholesale reduction of infinitistic mathematics to finitistic mathematics, which Hilbert envisioned, cannot be pushed through.

At this point I insert a digression concerning the relationship of Hilbert's Program to other reductionist programs.

In the philosophy of mathematics, a *reductionist* is anybody who
wants to reduce all or part of mathematics to some restricted set of
``acceptable'' principles. Hilbert's plan to reduce all of
mathematics to finitism is only one of many possible reductionist
schemes. In the aftermath of Gödel's Theorem, several authors have
proposed reductionist programs which are quite different from
Hilbert's.

For instance, Feferman [5] has developed an elaborate program of predicative reductionism. (See also Simpson [22], pp. 152-154.) Certainly Feferman's predicative standpoint is very far away from finitism. It accepts full classical logic and allows the set of all natural numbers as a completed infinite totality. But it severely restricts the use of quantification over the domain of all subsets of the natural numbers. At this APA-ASL symposium, Feferman referred to predicative reductionism as a ``relativized'' form of Hilbert's Program.

Similarly Gödel [10] has proposed an ``extension'' of the finitistic standpoint, by way of primitive recursive functionals of higher type. Also Bernays [1], p. 502, has discussed a program of intuitionistic reductionism which he regards as a ``broadening'' or ``enlarging'' of proof theory. In his introductory remarks to this symposium, Sieg interpreted Bernays as calling for a ``generalized Hilbert program.''

I would like to stress that these relativizations, extensions and
generalizations are very different from the original Program of
Hilbert. Above all, Hilbert's purpose was to validate infinitistic
mathematics by means of a reduction to *finitistic* reasoning.
Finitism was of the essence because of its clear physical meaning and
its indispensability for all scientific thought. By no stretch of the
imagination can Feferman's predicativism, Gödel's higher type
functionals, Myhill's intuitionistic set theory or Gentzen's
transfinite ordinals be viewed as finitistic. These proof-theoretic
developments are ingenious and have great scientific value, but they
are not contributions to Hilbert's Program.