FOM: How natural is RCA_0 ???

[Stephen G Simpson]

Peter Smith writes:
 > Apologies if the following is just dumb and/or ignorant: but here
 > goes ...!
 > 
 > The background is Simpson's wonderful SOSOA,

This comment is certainly not dumb and ignorant by my standards!  All
flattery will be cheerfully accepted.

 > and the qn is "How natural is his base theory RCA_0" ?

This is a good question.  RCA_0 is very natural from several
viewpoints, but perhaps SOSOA doesn't emphasize this enough.

A few comments, in descending order of interest.

1. It may be thought that restricting RCA_0 and WKL_0 to Sigma^0_1
   induction is mere pedantry (or "economy", to use Matt Frank's
   term).  But this is far from the case.  The restriction to
   Sigma^0_1 induction means that RCA_0 and WKL_0 are conservative
   over first order arithmetic with induction restricted to Sigma_1
   formulas (Harrington [unpublished, but see SOSOA]), which is in
   turn conservative over PRA -- Primitive Recursive Arithmetic -- for
   Pi_2 sentences (Parsons [1970]).  Since conservativity over PRA
   plays a special role in the analysis of Hilbert's program of
   finitistic reductionism (see Tait, J. Phil, 1981), the restriction
   to Sigma^0_1 induction has a serious foundational point.  See
   Remark IX.3.18 in SOSOA.  An elaboration of this remark is my paper
   in JSL vol. 53, 1988, 349-363.

2. Isolating Sigma^0_1 induction as a separate axiom makes it possible
   to consider the reverse mathematics of Sigma^0_1 induction.  It
   turns out that there are a number of mathematical statements which
   are equivalent to Sigma^0_1 induction, over a weaker system known
   as RCA_0^*.  For example, the statement that every polynomial over
   a countable field can be factored into irreducible polynomials.
   See Section X.5 of SOSOA.

3. Peter Smith correctly points out an apparent imbalance between
   Delta^0_1 comprehension and Sigma^0_1 induction.  To answer this, I
   note that one can replace Sigma^0_1 induction by Delta^0_1
   induction plus primitive recursion.  This corrects the apparent
   imbalance.  When I was writing SOSOA, it seemed more natural to
   prove primitive recursion as a theorem, assuming Sigma^0_1
   induction as an axiom, so this is what I did.  But one can do it
   the other way around.  Harvey Friedman did it this way when he
   originally introduced RCA_0, in a 1967 abstract [JSL vol. 41,
   p. 557].

4. Another way to correct the imbalance between Sigma^0_1 induction
   and Delta^0_1 comprehension is to note the following: Sigma^0_1
   induction is equivalent (over RCA_0^*, say) to an appropriate
   comprehension axiom, namely bounded Sigma^0_1 comprehension.  See
   SOSOA, Remark II.3.11.

5. Experience suggests that RCA_0 is just the right system for
   "formalized recursive mathematics".  (This formulation is from Anil
   Nerode.)  Most of the positive results of recursive mathematics are
   provable in RCA_0, but many would fail with weaker induction.

Peter Smith:

 > b) What exciting things would happen if, more generously, we
 > married (Comp Sigma_0_1) with (Ind Sigma_0_1)?

We would just get ACA_0, because Sigma^0_1 comprehension implies
arithmetical comprehension (SOSOA, Lemma III.1.3).

 > Or more meanly married (Comp Delta_0_1) with (Delta_0_1)?

This would be RCA_0^*, I guess.

-- Steve