FOM: How natural is RCA_0 ???

[Matthew Frank]

Peter Smith recently asked (excerpted from his Apr 1 post):

> The background is Simpson's wonderful SOSOA, and the qn is "How 
> natural is his base theory RCA_0" ?
> RCA_0 marries (Comp Delta_0_1) with (Ind Sigma_0_1) and
> you might be puzzled about the apparent mismatch.
 
> Antecedently to doing the hard mathematical work and finding that 
> the (Comp Delta_0_1) married to (Ind Sigma_0_1) is particularly 
> fruitful, are there a priori/"philosophical" reasons for supposing 
> the combination is natural and well-motivated?

I suspect that RCA_0 + all arithmetic induction axioms would make a more
philosophically coherent theory than RCA_0 by itself (i.e. with only
Sigma_0^1 and Pi_0^1 induction axioms).  If one grants that all the
arithmetic induction axioms are meaningful, it's hard to see what
intuitions could separate the Sigma_0^1 and Pi_0^1 axioms from the others.
In particular I think that the higher arithmetic induction axioms are
immune from the doubts attached to set existence axioms.

On the other hand, Simpson mostly uses RCA_0 to prove various mathematical
results, and to prove the equivalence of various results with higher
subsystems of second-order arithmetic.  Both of these can be accomplished
without the extra induction axioms, so dropping the extra axioms seems to
be just a matter of economy.  Simpson also correlates RCA_0 with
Bishop-style constructive analysis, and I think that this correlation
would not be much affected by a change in which arithmetic induction
axioms get used.

--Matt