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
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 [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*_{2}. There are a great many different
subsystems of *Z*_{2} 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 *Z*_{2} and proved in some subsystem of *Z*_{2}. For many
specific theorems ,
it turns out that there is a weakest natural
subsystem
of *Z*_{2} 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
*Z*_{2}. 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 [21].) 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 *Z*_{2} 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 *Z*_{2} 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 *Z*_{2} 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.