Why restrict to $\Sigma_1^0$ formulas in $RCA_0$ induction? I recently asked this question over on math.se, warmly welcomed by crickets.  I hope it's appropriate here.
I'm reading Stillwell's Reverse Mathematics, and the induction axiom was just introduced.

For a $\Sigma_1^0$ formula $\phi$, 
\begin{equation}
  [\phi(0)\; \wedge\; \forall n\, (\phi(n) \Rightarrow \phi(n+1))] \Rightarrow \forall n\,\phi(n)
   \end{equation}

I'm wondering why we restrict to $\Sigma_1^0$.  All that he offers about the decision is in a footnote

$\Sigma_1^0$ induction is preferred because we want a base system to be as elementary as possible.

But I'm wondering what is special about $\Sigma_1^0$ formulas. We just proved that they are computably enumerable, but I can't get a good grasp of why you would only want to be able to do induction on computably enumerable formulas--does it make anything "more computable"?  Why not just $\Sigma_0^0$ or even $\Pi_1^0$? Presumably $\textit{RCA}_0$ now admits a few more models, where induction over more complex formulas fails.  What would one of those models look like?
 A: Roughly speaking, the choice of $\Sigma^0_1$ induction is a balance between (1) having enough induction to make most proofs straightforward and (2) keeping the first-order part of the theory simple.
Keeping the first-order part simple -  $\mathsf{RCA}_0$ is $\Pi^0_1$ conservative over PRA, unlike the corresponding system $\mathsf{RCA}$ with full induction.  The proof theoretic ordinals of $\mathsf{RCA}_0$ and $\mathsf{ACA}_0$ are relatively tame. So the fact that mathematical theorems can be proven in these systems with restricted induction means that those theorems don't have exceptionally high consistency strength, which is an interesting foundational aspect of Reverse Mathematics. 
Having enough induction - in many cases, $\Sigma^0_1$ induction is enough. Often, the naive proof of a theorem in $\mathsf{RCA}_0$ only uses $\Sigma^0_1$ induction. With practice, we can often find ways to reduce the induction when the naive proof doesn't work. 
Moreover, when we begin to look at stronger systems, such as $\mathsf{ACA}_0$, we get more induction "for free" - $\mathsf{ACA}_0$ proves the induction scheme for arithmetical formulas, and $\Pi^1_1$ comprehension proves induction for $\Pi^1_1$ formulas. So the effect of restricted induction is not so high once we get above $\mathsf{WKL}_0$ in the "Big 5" hierarchy. 
On the other hand, if we weaken the induction axiom to $\Sigma^0_0$ induction, we do begin to run into some issues. There are indeed weaker systems such as $\mathsf{RCA}_0^*$ and $\mathsf{WKL}_0^*$, which replace $\Sigma^0_1$ induction with $\Sigma^0_0$ induction, $\Sigma^0_0$ bounding, and axioms making exponentiation act as it should. Obviously this larger list of axioms is less "elegant".  But more importantly these systems can't prove elementary facts such as "a polynomial over a countable field has only finitely many roots" which is equivalent to $\Sigma^0_1$ induction over $\mathsf{RCA}_0^*$.  So there is some genuine utility to using $\Sigma^0_1$ induction. 
One final aspect of the choice of $\Sigma^0_1$ induction is that there are relatively few results would otherwise be provable in $\mathsf{RCA}_0$ but require more than this much induction, and particularly few results like that in countable real analysis and countable abstract algebra.  Jeffry Hirst showed in 1987 that the pigeonhole principle (i.e. if $\mathbb{N}$ is finitely colored there is an infinite homogeneous set) is not provable in $\mathsf{RCA}_0$ and is equivalent to $\mathsf{B}\Pi^0_1$. But there were few other low-level results known in the 1980s that required more induction than was present in $\mathsf{RCA}_0$, and by then the theory $\mathsf{RCA}_0$ was well established. 
There is more discussion of this in various places. I would look at these two papers first, particularly pp. 148ff. of the first. 


*

*Stephen G. Simpson, Friedman's research on subsystems of second
 order arithmetic, in Leo Harrington, Michael Morley, Andre Scedrov and 
 Stephen G. Simpson (editors), Harvey Friedman's Research in the
 Foundations of Mathematics, North-Holland, Amsterdam, 1985, pp. 137-159.

*Stephen G. Simpson, Partial realizations of Hilbert's Program,
 Journal of Symbolic Logic, 53, 1988, pp. 349-363.
