FOM: what is the value of reverse mathematics?

[Stephen G Simpson]

In his angry posting of 2 Aug 1999 12:54:07, Robert Soare asks a lot
of hostile questions about my major f.o.m. research area, reverse
mathematics.  Here I want to attempt to present a partial answer or at
least an orientation that may be useful to some FOM readers.

To begin with, Soare angrily points out

 > the HUGE GAPS in philosophy, approach, and value of mathematical
 > items, between the REVERSE MATHEMATICIAN and the ACTIVE RESEARCHER
 > in mathematics from TOPOLOGY to COMPUTABILITY THEORY.
 > The former is eager to analyze the proof strength, axiomatic
 > necessity, etc. of hypotheses but of mostly EXISTING theorems,
 > while the working mathematician wants to get on with proving NEW
 > theorems, (with as little TIME wasted on EMAIL and INTERNET LIST
 > FORUMS as possible).

 [ Soare's emphasis ]

If I were thin-skinned, I might take this remark as an insult implying
that researchers in reverse mathematics and FOM participants are not
``active researchers''.  But I am thick-skinned, and anyway, there is
a valid general point lurking here.

The general point is that f.o.m. is not part and parcel of core
mathematics, but rather a different subject, with its own methods,
values, and goals.  In my FOM posting of 15 Jul 1999 22:33:53 I have
said the same thing in a different way, commenting on the Two
Cultures: the f.o.m. culture and core math culture.  My web page on
foundations <http://www.math.psu.edu/simpson/foundations.html> may
also provide some guidance.

Anyway, Soare continues in his hostile vein, trying to compare reverse
mathematics unfavorably to pure mathematics and especially his own
area, recursion (computability) theory.

 > Here are some questions for Mr. Simpson about the value and
 > applications of Reverse Mathematics.
 > 
 > QUESTION. what are the APPLICATIONS of REVERSE MATHEMATICS to computer
 > science?  
 
 [ Soare's emphasis]

Answer: none that I know of.

 > QUESTION 1-R/M.  When has REVERSE MATHEMATICS (R/M) SOLVED a
 > problem on UNDECIDABILITY (such as Hilbert's 10 problem, or the
 > word problem for finitely presented groups, where priority
 > arguments were used by Boone to get such a word problem of EVERY
 > C.E. DEGREE, ...
 
 [ Soare's emphasis]

Answer: never.

Et cetera, et cetera.

But questions such as this entirely miss the point.

The point is that reverse mathematics does not *need* such
``applications'' in order to indirectly justify itself.  That is
because reverse mathematics deals *directly* with issues that are of
obvious foundational importance and general intellectual interest.

Specifically, Reverse mathematics is a *direct* assault on the
following foundational question: 

   ``What are the appropriate axioms for mathematics?''

It attacks this question directly, by classifying mathematical
theorems according to the axioms needed to prove them.  When this is
done scrupulously and systematically, it turns out that the axioms are
equivalent to the theorems -- hence the name reverse mathematics.  And
then, a remarkable pattern emerges: the five ``basic systems'' (RCA0,
WKL0, ACA0, ATR0, Pi11-CA0) come up over and over again as being
logically equivalent to many, many theorems from diverse mathematical
areas.  This remarkable pattern is documented in my book
<http://www.math.psu.edu/simpson/sosoa/>.  And all this in the space
of only a few decades!  Reverse mathematics is just getting started.

Soare continues:

 > QUESTION 2-R/M
 ...
 > >   "What's the point in RM to prove reversals for the next 100 theorems
 > >   after you've seen 500? ... Is there a program, or is it just "take
 > >   your favorite math book and reverse"?

The answer is, both.  

First, there are definitely some grand programs in reverse
mathematics, of which we have only begun to scratch the surface.  One
of these is to weaken the base theory, thereby greatly extending the
scope of reverse mathematics.  This is discussed in my CTA talk
<http://www.math.psu.edu/simpson/cta/>.  There are others, some of
them elaborated in Harvey Friedman's CTA talk.  I'll let Harvey pick
this up.

Second, you can ``take your favorite math book and reverse''.  If you
do this with wit and skill, it leads to a huge number of fascinating
f.o.m. problems at all levels of difficulty, from routine to almost
impossibly difficult.  The *methods* are extremely interesting (inner
models, forcing, coding arguments, compactness arguments,
pseudohierarchies, etc etc), but more importantly, the *results* keep
mounting up and forming these remarkable patterns, which are of great
foundational significance ....

No time to say more now.  I am going away for a long weekend.  I will
post more on this later.

-- Steve