FOM: reverse math amplification

[Harvey Friedman]

Simpson 10:25PM 9/8/98 posted an explanation of reverse math in response to
Silver 6:16AM 9/8/98. I thought it might be useful to amplify on this topic
at an elementary level. Feedback from FOM is requested as to the
appropriateness of this kind of posting, below.
**********

The use of "second order arithmetic" as a **first order formal system** to
formalize mathematics is an old idea going back to the 50's that is an
obvious outgrowth of the usual formalization of mathematics in ZFC. Second
order arithmetic is particularly convenient because the ontololgy is
extremely manageable - just natural numbers and sets of natural numbers.
The formalization of mathematics in terms of natural numbers and sets of
natural numbers does, however, require various obvious coding devices, as
in Godel's famous work on the incompleteness of Peano Arithmetic (and
extensions thereof).

Then upon examination of the formalization of classical mathematics in
second order arithmetic, one sees that only small fragments are used. This
leads to the question of what small fragments are essential. And then the
classification program of determining the exact fragment needed for any
given mathematical theorem - potentially different fragments for different
theorems.

The insight at the heart of reverse mathematics is that one can identify
these "small fragments" in an unambiguous way for a huge variety of
mathematical theorems, and that only a manageably small number of such
small fragments appear. This supports an extensive classification program
for mathematical theorems.

This is accomplished in the following way. First one identifies a
particularly weak fragment of second order arithmetic in order to get
started. (The need for this will become clear as the discussion proceeds).
This is called the base theory. The base theory is chosen so that a healthy
amount of classical mathematics is straightforwardly formalized there, but
with crucial and interesting exceptions.

The base theory is chosen so that these exceptions include many (certainly
not all) of the most important theorems of classical mathematics. It is
also important that the base theory be chosen so that it comprises a
handful of natural and easily identifiable principles that occur naturally
in the usual formalization of classical mathematics.

The theorems of classical mathematics that are not provable in the base
theory are then the subject of classification in the following way. Let B
be the base theory, and let X,Y be two classical mathematical theorems not
provable in the base theory. There is the equivalence relation: B proves X
if and only if Y. There is also the partial ordering (>=): B proves X
implies Y.

At first blush, one might think that this equivalence relation is
hopelessly sparse - very rarely does it hold, and that there are an
unmanageably large number of equivalence classes. In that case, the
classification project cannot really get off the ground in any attractive
or informative way.

But just the opposite occurs. For quite some time, only FOUR equivalence
relations were discovered to appear in actual classical mathematics.
Furthermore, four very natural "representatives" of these equivalence
classes were given. By representatives here, I mean that four fragments of
second order arithmetic (the first order system mentioned in the first
sentence above), call them T1, T2, T3, T4, were given so that all of the
theorems, X, examined in the early development of reverse mathematics have
exactly one of the following properties:

	i) X is provable in the base theory B, in which case there is
nothing more to be said in reverse mathematics about X;
	ii) B proves X if and only if T1;
	iii) B proves X if and only if T2;
	iv) B proves X if and only if T3;
	v) B proves X if and only if T4.

Furthermore, we have the proper inclusions B contained in T1 contained in
T2 contained in T3 contained in T4. And T1, T2, T3, T4, like the base
theory B, also "comprises a handful of natural and easily identifiable
principles that occur naturally in the usual formalization of classical
mathematics."

In the later development of reverse mathematics, a few additional
equivalence relations were discovered among the theorems of classical
mathematics; e.g., the classical Hilbert basis theorem for polynomial rings
of several variables over a countable field (Simpson), and others. But only
a very few. The ratio of theorems classified and equivalence classes is, to
this day, absolutely enormous. However, the linearity: B contained in T1
contained in T2 contained in T3 contained in T4, no longer holds.
Nevertheless, an important and more subtle kind of linearity still
prevails, which I will not go into in this posting.

Reverse mathematics represents a striking robust classification scheme in
which a handful of "constants of nature" emerge.