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 of ordinary mathematics, which set existence axioms are needed in order to prove ? 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 . 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 Z2. There are a great many different subsystems of Z2 which are distinguished from one another by their stronger or weaker set existence axioms. It turns out that almost every theorem of ordinary mathematics can be stated in the language of Z2 and proved in some subsystem of Z2. For many specific theorems , it turns out that there is a weakest natural subsystem of Z2 in which is provable. Moreover is often one of a relatively small number of specific systems. The specific systems which most often arise in this context are , , , and - . Of these is the weakest and the others are listed in order of increasing strength. The system 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 , the general procedure for identifying is to show that the principal set existence axiom of is equivalent to , the equivalence being provable in some weaker system in which itself is not provable. For instance, the way to show that is to show that is equivalent to Weak König's Lemma, the equivalence being provable in the weaker system . 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 which is defined in some neighborhood of 0. This theorem can be formulated as a sentence in the language of Z2. We may then consider the following special case of the Main Question. Which set existence axioms are needed for a proof of ?
The standard textbook proof of proceeds by way of the Ascoli Lemma. With some effort we can show that the Ascoli Lemma is provable in . We then see fairly easily that is provable in . But, in order to prove , were the set existence axioms of really needed? Motivated by this question we try to ``reverse'' both the Ascoli Lemma and by showing that each of them is equivalent to over the weaker system . This attempt succeeds for the Ascoli Lemma but fails in the case of . We therefore try to prove in the next system weaker than , namely . This attempt is ultimately successful, but the resulting proof of in 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 . Finally we tie up the remaining loose ends by showing that is equivalent to over . We are thus left with a precise answer to the above-mentioned special case of the Main Question. (For details see Simpson .) This is a solid contribution to Reverse Mathematics.
As a byproduct of this work in Reverse Mathematics, we see that is provable in . Combining this with the results of §§ 3 and 4, we have a solid contribution to Hilbert's Program. Namely we see that 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 Z2 such as or . 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 leads to the discovery that the theorem is in fact provable in one of the weaker systems or . Thus Reverse Mathematics plays a negative yet valuable heuristic role.
More fundamentally, Reverse Mathematics helps us to uncover the subsystems of Z2 which are relevant to partial realizations of Hilbert's Program. It is a fact that and were first discovered in the context of Reverse Mathematics. They arose naturally as candidates for the weakest subsystems of Z2 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  about the connection between Hilbert's Program and Reverse Mathematics.