FOM: How natural is RCA_0 ???
mfrank at math.uchicago.edu
Tue Apr 2 19:30:30 EST 2002
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.
More information about the FOM