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₂ which are conservative over PRA with respect to $\Pi^0_1$ 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₂ known as $\mathsf{WKL}_0$. The language of $\mathsf{WKL}_0$ is the same as that of Z₂. The logic of $\mathsf{WKL}_0$ is full classical logic including the unrestricted law of the excluded middle. Induction is assumed only for $\Sigma^0_1$ formulas of the language of Z₂. The mathematical axioms of $\mathsf{WKL}_0$ imply that one can obtain new functions from arbitrary given ones by means of substitution, primitive recursion, and minimization. In particular $\mathsf{WKL}_0$ includes PRA and hence all of finitistic mathematics. In addition $\mathsf{WKL}_0$ 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 $2^\mathbb{N}$is compact, i.e. enjoys the Heine-Borel covering property for sequences of basic open sets. Friedman pointed out that compactness of $2^\mathbb{N}$ implies, for instance, compactness of the closed unit interval [0,1] within $\mathsf{WKL}_0$.

Second, it has been shown that $\mathsf{WKL}_0$ is conservative over PRA with respect to $\Pi^0_1$ sentences. This result is originally due to Friedman [7] who in fact obtained a stronger result: $\mathsf{WKL}_0$ is conservative over PRA with respect to $\Pi^0_2$ sentences. This means that any $\Pi^0_2$ sentence which is provable in $\mathsf{WKL}_0$ 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 $\mathsf{WKL}_0$ 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 $\mathsf{WKL}_0$ is finitistically reducible in the sense of Hilbert's Program. In particular, any $\Pi^0_2$ consequence of such a theorem is finitistically true.

Of course all of this would be pointless if $\mathsf{WKL}_0$ 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 $\mathsf{WKL}_0$ is mathematically rather strong. For example, the following mathematical theorems are provable in $\mathsf{WKL}_0$.

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 $\mathbb{R} ^n$ 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 $\mathsf{WKL}_0$ 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 $\mathsf{WKL}_0$. Using conservativity of $\mathsf{WKL}_0$ over PRA, we can then ``eliminate'' this technique. Our conclusion is that any $\Pi^0_2$ number-theoretic theorem which is provable using contour integration can also be proved ``elementarily,'' i.e. within PRA.

$$*\quad *\quad *$$

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₂. The new system properly includes $\mathsf{WKL}_0$ and is properly included in $\mathsf{ACA}_0$. For lack of a better name, we are temporarily calling the new system $\mathsf{WKL}_0^{+}$. The axioms of $\mathsf{WKL}_0^{+}$ are those of $\mathsf{WKL}_0$ plus an additional scheme. Let $2^{<\mathbb{N} }$ denote the set of finite sequences of 0's and 1's. The new scheme says that, given a sequence of dense subcollections of $2^{<\mathbb{N} }$ 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 $2^\mathbb{N}$. Brown and I have used forcing to show that $\mathsf{WKL}_0^{+}$ is conservative over $\mathsf{RCA}_0$ for $\Pi^1_1$ sentences. (Earlier Harrington [12] had used forcing to show that $\mathsf{WKL}_0$ is conservative over $\mathsf{RCA}_0$ for $\Pi^1_1$ sentences. Harrington's proof will appear in Simpson [24].) Combining this with a result of Parsons [19], we see that $\mathsf{WKL}_0^{+}$ is conservative over PRA for $\Pi^0_2$ sentences and that this conservation result is itself demonstrable within PRA. Thus we have finitistic reducibility of any mathematical theorem which is provable in $\mathsf{WKL}_0^{+}$. The point of all this is that $\mathsf{WKL}_0^{+}$ includes several highly nonconstructive theorems of functional analysis which are apparently not provable in $\mathsf{WKL}_0$. 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₂ 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].