Partial Realizations of Hilbert's Program

Gödel's Theorem shows that it is impossible to reduce all of
infinitistic mathematics to finitistic mathematics. There remains the
problem of validating as much of infinitistic mathematics as possible.
In particular, what part of infinitistic mathematics can be reduced to
finitistic reasoning? Using the precise explications in
§3, we may reformulate this question as follows.
*How much of infinitistic mathematics can be developed within
subsystems of Z_{2} which are conservative over PRA with respect to
sentences?*

Recent investigations have revealed that the answer to the above
question is: *quite a large part.* The purpose of this section is
to explain these recent discoveries. I shall now do so.

First, Friedman [6] has defined a certain interesting subsystem
of *Z*_{2} known as
.
The language of
is the same as that
of *Z*_{2}. The logic of
is full classical logic including the
unrestricted law of the excluded middle. Induction is assumed only
for
formulas of the language of *Z*_{2}. The mathematical
axioms of
imply that one can obtain new functions from
arbitrary given ones by means of substitution, primitive recursion,
and minimization. In particular
includes PRA and hence all of
finitistic mathematics. In addition
includes a highly
nonconstructive axiom which asserts that any infinite tree of finite
sequences of 0's and 1's has an infinite path. This powerful
principle is known as Weak König's Lemma. Topologically, Weak
König's Lemma amounts to the assertion that the Cantor space
is compact, *i.e.* enjoys the Heine-Borel covering property for
sequences of basic open sets. Friedman pointed out that compactness
of
implies, for instance, compactness of the closed unit
interval [0,1] within
.

Second, it has been shown that
is conservative over PRA with
respect to
sentences. This result is originally due to
Friedman [7] who in fact obtained a stronger result:
*
is conservative over PRA with respect to
sentences*. This means that any
sentence which is
provable in
is already provable in PRA and hence is witnessed
by a primitive recursive Skolem function. Friedman's proof of this
result is model-theoretic and will be published by Simpson [24].
Subsequently Sieg [20] used a Gentzen-style method to give an
alternative proof of Friedman's result. Actually Sieg exhibited a
primitive recursive proof transformation. Thus the reducibility of
to PRA is itself provable in PRA. (These conclusions due to
Sieg [20] could also have been derived from work of Parsons
[19] and Harrington [12].)

The above results of Friedman and Sieg may be summarized as follows.
*Any mathematical theorem which can be proved in
is
finitistically reducible in the sense of Hilbert's Program*. In
particular, any
consequence of such a theorem is
finitistically true.

Of course all of this would be pointless if
were as weak as
PRA with respect to infinitistic mathematics. But fortunately such is
not the case. The ongoing efforts of Simpson and others have shown
that
is mathematically rather strong. *For example, the
following mathematical theorems are provable in
.*

**4.1.** The Heine-Borel covering theorem for closed bounded
subsets of Euclidean *n*-space (Simpson [21,24]) or for closed
subsets of a totally bounded complete separable metric space
(Brown-Simpson [3], Brown [2]).

**4.2.** Basic properties of continuous functions of several real
variables. For instance, any continuous real-valued function on a
closed bounded rectangle in
is uniformly continuous and
Riemann integrable and attains a maximum value (Simpson [21,24]).

**4.3.** The local existence theorem for solutions of systems of
ordinary differential equations (Simpson [21]).

**4.4.** The Hahn-Banach Theorem and Alaoglu's Theorem for
separable Banach spaces (Brown-Simpson [3], Brown [2]).

**4.5.** The existence of prime ideals in countable commutative
rings (Friedman-Simpson-Smith [8]).

**4.6.** Existence and uniqueness of the algebraic closure of a
countable field (Friedman-Simpson-Smith [8]).

**4.7.** Existence and uniqueness of the real closure of a
countable formally real field (Friedman-Simpson-Smith [8]).

These examples show that is strong enough to prove a great many theorems of classical infinitistic mathematics, including some of the best-known nonconstructive theorems. Combining this with the results of Friedman and Sieg, we see that a large and significant part of mathematical practice is finitistically reducible. Thus we have in hand a rather far-reaching partial realization of Hilbert's Program.

This partial realization of Hilbert's Program has an interesting
application to the problem of ``elementary'' proofs of theorems from
analytic number theory. Using 4.2 we can formalize the technique of
contour integration within
.
Using conservativity of
over PRA, we can then ``eliminate'' this technique. Our conclusion is
that any
number-theoretic theorem which is provable using
contour integration can also be proved ``elementarily,'' *i.e.*
within PRA.

I shall now announce some new results which extend the ones that were
discussed above. Very recently, Brown and I defined a new subsystem
of *Z*_{2}. The new system properly includes
and is properly
included in
.
For lack of a better name, we are temporarily
calling the new system
.
The axioms of
are those of
plus an additional scheme. Let
denote the set of
finite sequences of 0's and 1's. The new scheme says that, given a
sequence of dense subcollections of
which is arithmetically
definable from a given set, there exists an infinite sequence of 0's
and 1's which meets each of the given dense subcollections. This
amounts to a strong formal version of the Baire Category Theorem for
the Cantor space
.
Brown and I have used forcing to show that
is conservative over
for
sentences.
(Earlier Harrington [12] had used forcing to show that
is
conservative over
for
sentences. Harrington's proof
will appear in Simpson [24].) Combining this with a result of
Parsons [19], we see that
is conservative over PRA for
sentences and that this conservation result is itself
demonstrable within PRA. Thus we have finitistic reducibility of any
mathematical theorem which is provable in
.
The point of all
this is that
includes several highly nonconstructive theorems
of functional analysis which are apparently not provable in
.
Prominent among these are the Open Mapping Theorem and the Closed
Graph Theorem for separable Banach spaces. Thus we have a finitistic
reduction of these theorems as well. This represents further progress
in our partial realization of Hilbert's Program. There seems to be a
possibility of defining even stronger subsystems of *Z*_{2} which would
contain even more theorems of infinitistic mathematics yet remain
finitistically reducible to PRA. This would represent still further
progress.

The results announced in the previous paragraph are not yet in final form. A version of them will appear in Brown's forthcoming Ph. D. thesis which is now being written under my supervision [2].