The Role of Reverse Mathematics

The purpose of this section is to discuss Reverse Mathematics and its relationship to our previously described partial realization of Hilbert's Program.

Reverse Mathematics is a highly developed research program whose purpose is to investigate the role of strong set existence axioms in ordinary mathematics. The Main Question is as follows. Given a specific theorem $\tau$ of ordinary mathematics, which set existence axioms are needed in order to prove $\tau$? Reverse Mathematics is a technique which frequently yields precise answers to special cases of this question.

A fairly detailed survey of Reverse Mathematics will be found in my appendix to the forthcoming second edition of Takeuti's proof theory book [23]. Here I must confine myself to a very brief summary.

Most of the work on Reverse Mathematics has been carried out in the context of subsystems of Z₂. There are a great many different subsystems of Z₂ which are distinguished from one another by their stronger or weaker set existence axioms. It turns out that almost every theorem $\tau$ of ordinary mathematics can be stated in the language of Z₂ and proved in some subsystem of Z₂. For many specific theorems $\tau$, it turns out that there is a weakest natural subsystem $S(\tau)$ of Z₂ in which $\tau$ is provable. Moreover $S(\tau)$ is often one of a relatively small number of specific systems. The specific systems which most often arise in this context are $\mathsf{RCA}_0$, $\mathsf{WKL}_0$, $\mathsf{ACA}_0$, $\mathsf{ATR}_0$ and $\Pi^1_1$- $\mathsf{CA}_0$. Of these $\mathsf{RCA}_0$ is the weakest and the others are listed in order of increasing strength. The system $\mathsf{WKL}_0$ has already been discussed in §4 above. For definitions of the other systems and an explanation of their role in Reverse Mathematics, see Simpson [23,24].

Given a mathematical theorem $\tau$, the general procedure for identifying $S(\tau)$ is to show that the principal set existence axiom of $S(\tau)$ is equivalent to $\tau$, the equivalence being provable in some weaker system in which $\tau$ itself is not provable. For instance, the way to show that $S(\tau) =$ $\mathsf{WKL}_0$ is to show that $\tau$ is equivalent to Weak König's Lemma, the equivalence being provable in the weaker system $\mathsf{RCA}_0$. Our slogan ``reverse mathematics'' arises in the following way. The usual pattern of mathematical reasoning is to deduce a theorem from some axioms. This might be called ``forward mathematics.'' But in order to establish that the axioms are needed for a proof of the theorem, one must reverse the process and deduce the axioms from the theorem. Hence ``reverse mathematics.''

As an example, consider the local existence theorem for solutions of ordinary differential equations. Given an initial value problem y' = f(x,y), y(0) = 0 where f(x,y) is defined and continuous in some neighborhood of (0,0), there exists a continuously differentiable solution $y = \phi(x)$ which is defined in some neighborhood of 0. This theorem can be formulated as a sentence $\tau$ in the language of Z₂. We may then consider the following special case of the Main Question. Which set existence axioms are needed for a proof of $\tau$?

The standard textbook proof of $\tau$ proceeds by way of the Ascoli Lemma. With some effort we can show that the Ascoli Lemma is provable in $\mathsf{ACA}_0$. We then see fairly easily that $\tau$ is provable in $\mathsf{ACA}_0$. But, in order to prove $\tau$, were the set existence axioms of $\mathsf{ACA}_0$ really needed? Motivated by this question we try to ``reverse'' both the Ascoli Lemma and $\tau$ by showing that each of them is equivalent to $\mathsf{ACA}_0$ over the weaker system $\mathsf{RCA}_0$. This attempt succeeds for the Ascoli Lemma but fails in the case of $\tau$. We therefore try to prove $\tau$ in the next system weaker than $\mathsf{ACA}_0$, namely $\mathsf{WKL}_0$. This attempt is ultimately successful, but the resulting proof of $\tau$ in $\mathsf{WKL}_0$ turns out to be much more difficult than the textbook proof. This was to be expected since we already knew that the Ascoli Lemma is not provable in $\mathsf{WKL}_0$. Finally we tie up the remaining loose ends by showing that $\tau$ is equivalent to $\mathsf{WKL}_0$ over $\mathsf{RCA}_0$. We are thus left with a precise answer to the above-mentioned special case of the Main Question. (For details see Simpson [21].) This is a solid contribution to Reverse Mathematics.

As a byproduct of this work in Reverse Mathematics, we see that $\tau$is provable in $\mathsf{WKL}_0$. Combining this with the results of §§ 3 and 4, we have a solid contribution to Hilbert's Program. Namely we see that $\tau$ is in a certain precise sense finitistically reducible.

The above example illustrates the general relationship between Reverse Mathematics and Hilbert's Program. Our method for Hilbert's Program is to prove specific mathematical theorems within certain subsystems of Z₂ such as $\mathsf{WKL}_0$ or $\mathsf{WKL}_0^{+}$. Reverse Mathematics helps us to find the theorems for which this is possible. In many cases, the failure of an attempt to ``reverse'' a theorem vis-á-vis $\mathsf{ACA}_0$ leads to the discovery that the theorem is in fact provable in one of the weaker systems $\mathsf{WKL}_0$ or $\mathsf{WKL}_0^{+}$. Thus Reverse Mathematics plays a negative yet valuable heuristic role.

More fundamentally, Reverse Mathematics helps us to uncover the subsystems of Z₂ which are relevant to partial realizations of Hilbert's Program. It is a fact that $\mathsf{WKL}_0$ and $\mathsf{WKL}_0^{+}$ were first discovered in the context of Reverse Mathematics. They arose naturally as candidates for the weakest subsystems of Z₂ in which to prove certain mathematical theorems.

I do not mean to imply that Reverse Mathematics is coextensive with partial realizations of Hilbert's Program. It certainly is not. I only assert the existence of a certain mutually reinforcing relationship between these two lines of research.

I hope that I have adequately addressed Takeuti's concerns [26] about the connection between Hilbert's Program and Reverse Mathematics.