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
prosper.
-- Steve
More information about the FOM
mailing list