FOM: What's so good about reverse mathematics?

[Stephen G Simpson]

Charles Silver writes:
 > 
 > 	I would profit from a discussion of the purposes, merits,
 > "general intellectual interest," and so forth of reverse mathematics.

These issues are discussed rather fully in my forthcoming book
"Subsystems of Second Order Arithmetic".  Chapter 1 of that book is on
line at http://www.math.psu.edu/simpson/sosoa/.

But I would also welcome a discussion of these issues here on the FOM
list.  Let me start the ball rolling now with a quick answer.

A basic f.o.m. question is: which axioms are appropriate for
mathematics.  The current importance of set-theoretic foundations
gives rise to one version of this, the so-called Main Question of
reverse mathematics: which set existence axioms are needed to prove
specific, well-known theorems of core mathematics?  The technical work
answering this question leads to a classification of many well-known
core mathematical theorems according to logical strength and/or the
set existence axioms needed to prove them.  To quote from my FOM
posting of 1 Mar 1998 19:00:15:
  
   Reverse Mathematics consists of a series of case studies in
   formalization of mathematics within subsystems of second order
   arithmetic with restricted induction.  It turns out that, for a great
   many specific key mathematical theorems t, there is a weakest natural
   system S(t) in which t is provable.  In each case, "weakest natural"
   is validated by showing that t is logically equivalent to the
   principal set existence axiom of S(t), equivalence being proved in a
   weak base system.  Furthermore, the systems S(t) that arise frequently
   are few in number, principally the following:
   
     1. RCA_0 (Delta^0_1 comprehension plus Sigma^0_1 induction)
     2. WKL_0 (RCA_0 plus weak K"onig's lemma)
     3. ACA_0 (arithmetical comprehension)
     4. ATR_0 (arithmetical transfinite recursion)
     5. Pi^1_1-CA_0 (Pi^1_1 comprehension)
   
   For example, the theorem that every continuous f:[0,1] -> R has a
   maximum is equivalent to WKL_0 over RCA_0.  Also equivalent to WKL_0
   over RCA_0 are: the Cauchy-Peano existence theorem for solutions of
   ordinary differential equations; the Heine-Borel compactness of [0,1];
   the theorem that every countable commutative ring has a prime ideal;
   the Hahn-Banach theorem for separable Banach spaces; the Brouwer and
   Schauder fixed point theorems; etc etc.  These results for WKL_0 are
   of interest with respect to Hilbert's program of finitistic
   reductionism, because WKL_0 is conservative over primitive recursive
   arithmetic for Pi^0_2 sentences.  See
   http://www.math.psu.edu/simpson/papers/hilbert/.  Moreover, just as
   WKL_0 embodies finitistic reductionism, there are similar
   correspondences to other foundational programs: ACA_0 embodies
   predicative mathematics, and ATR_0 embodies predicative reductionism.

Later I will have more to say about the goals and achievements of
reverse mathematics.  The above is only a beginning.

 > Steve and Harvey founded this list at least partly--it appears--to provide
 > a forum for reverse mathematics, ...

Not really.  We founded the FOM list in order to create an
intellectual climate in which foundations of mathematics can grow and
prosper.

-- Steve