# FOM: How natural is RCA_0 ???

Stephen G Simpson simpson at math.psu.edu
Tue Apr 9 20:31:18 EDT 2002

```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

```