Series: Logic Seminar
Speaker: Stephen G. Simpson (Penn State)
Title: Reverse Mathematics: an Introduction
Date: Tuesday, March 24, 1998
Date: Tuesday, March 31, 1998 (continuation)
Time: 2:30-3:45 PM
Place: 113 McAllister Building
Some relevant web pages:
http://www.math.psu.edu/simpson/sosoa/
http://www.math.psu.edu/simpson/foundations.html
http://www.math.psu.edu/simpson/papers/hilbert/
http://www.math.psu.edu/simpson/courses/math565.html
http://www.math.psu.edu/simpson/logic/seminar.html
Abstract:
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; ATR_0 embodies predicative reductionism.