FOM: What's so good about reverse mathematics?
Stephen G Simpson
simpson at math.psu.edu
Tue Sep 8 22:25:33 EDT 1998
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
More information about the FOM