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.