Why restrict to $\Sigma_1^0$ formulas in $RCA_0$ induction? 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: This is a great question!
The short version in my opinion is that there is a decent argument that $\mathsf{I\Sigma_1}$ corresponds to "finitistic induction," and so is naturally philosophically motivated; and moreover it's just strong enough to prove the basic facts about the other side of reverse math, namely its computability-theoretic concerns.
I think it's instructive, even though this question is just about one, to consider both of the "logical axes" of reverse mathematics (namely computability-theoretic and inductive content) since the contrast is interesting and they have nontrivial interaction. So that's what I'll do, making apologies for the length of this answer; hopefully you (and other readers) find it intersting.

The computability-theoretic side of things is pretty simple. The structures in question should be families of sets of natural numbers closed under basic computational processes, namely joins and Turing reductions. This immediately yields the notion of Turing ideals, and we can measure the computability-theoretic content of a theorem of second-order arithmetic by asking which Turing ideals satisfy it. For example, we can confidently say that "Every infinite subtree of $2^{<\mathbb{N}}$ has an infinite path" is computationally weaker than "Every function has a range" since the set of Turing ideals satisfying the former  is a strict superset of the set of Turing ideals satisfying the latter.
We can partially axiomatize this approach: Turing ideals are exactly $\omega$-models of $P^-+\Delta^0_1$-$\mathsf{CA}$, where $P^-$ is the set of ordered semiring axioms and $\Delta^0_1$-$\mathsf{CA}$ is the $\Delta^0_1$ comprehension axiom (we can indeed capture it by a single axiom by use of a universal $\Sigma^0_1$ formula). Note that the difference between this theory and $\mathsf{RCA_0}$ is simply the inclusion of additional axioms about the first-order part.
So looking ahead, what we'll want to "first-orderize" this situation is some theory $T$ whose $\omega$-models are Turing ideals as above and whose non-$\omega$-models still "behave like" Turing ideals to a satisfying extent. This is what computability theory demands of $\mathsf{RCA_0}$, and the key thesis here is:

$\Sigma^0_1$ induction is enough to prove the basic properties of computability which are first-order expressible - e.g. the basic facts about the "local" degree structures $\{{\bf a}\le_T{\bf 0^{(n)}}\}$, which can be treated in a first-order way, for each $n\in\mathbb{N}$.

This is not obvious in my opinion. For example, the existence of a maximal c.e. set is not provable with $\Sigma^0_1$ induction alone. The general study of what induction principles are needed to prove what first-order(izable) computability-theoretic principles, especially facts about the c.e. sets, is  reverse recursion theory.

The end of the previous section indicates the first requirement we'll want $\mathsf{I\Sigma_1}$ to satisfy: that it "makes $\Delta^0_1$ comprehension behave correctly." But that's really subservient to the computability-theoretic concerns of reverse mathematics, and moreover points towards stronger systems. We also have a purely inductive interest:

How much induction is "finitistic?"

The idea of restricting attention to the finitistic part of first-order arithmetic is a limitative one, as opposed to the "makes recursion go well" goal.
The connection between finitism (and its relatives) and induction is to be honest not something I've ever found convincing; I'm also not that interested in finitism as a whole. However, plenty of logicians (on both the mathematical and philosophical sides of the aisle) would strenuously disagree with me on both points, so I'll defer to them.
The basic theme is that in order to apply induction to a predicate $X$, we intuitively want each question of the form "Does $n$ satisfy $X$?" to be answerable in a way which doesn't depend on treating $\mathbb{N}$ as a completed object. There are a few ideas that start to bounce around at this point:

*

*Do we want each question of the above form to be answerable in a finite way, or just each positive instance to be answerable? These correspond to $\Sigma$- and $\Delta$-versions of induction respectively. (The negative instance version seems less natural since we only apply induction when all instances are positive; that said, it turns out that $\mathsf{I\Sigma_n}$ and $\mathsf{I\Pi_n}$ are equivalent for each $n$, so it really doesn't matter.) And, how do we feel about bounds on the time it will take to answer these sorts of questions?


*Fixing a quantifier complexity, what language should we apply it to? E.g. $\mathsf{I\Sigma_0}$ doesn't prove that exponentiation is total; how do we feel about $\mathsf{I\Sigma_0}(exp)$, the theory gotten from $\mathsf{I\Sigma_0}$ by extending the syntactic class "$\Sigma_1$" to formulas involving exponentiation as a primitve? Put another way, what are our basic operations on top of which we're slapping a notion of finitistic induction? (Towards this end I'll use "$\mathsf{IX_n}$" for the appropriate theory over the language $\{+,\times,<,0,1\}$ as usual, and "$\mathsf{IX_n}(L)$" for the analogue over a different language $L$.)
Now I personally find the choice of $\mathsf{I\Sigma_1}$ somewhat arbitrary. That said, it does have a couple nice features:

*

*It proves the totality of all primitive recursive functions (in fact, exactly the primitive recursive functions), and this massively overshoots all the basic functions we use in day-to-day life. So the language issue largely goes away, unless we want to argue that things like the Ackermann function are so embedded in natural mathematical discourse that they should be taken for granted in the same way as $+$ and $\times$.


*The $\Sigma_1$ properties are exactly those whose positive instances are verifiable by a finite search (albeit one lacking a nice bound on runtime). Arguably this is the broadest notion of checkability which doesn't treat $\mathbb{N}$ as a completed object.
That said, this is not universally accepted (especially that second point): e.g. primitive recursive arithmetic $\mathsf{PRA}$ is also taken as an appropriate first-order theory corresponding to finitism, and this is somewhat weaker than $\mathsf{I\Sigma_1}$ (although they $\mathsf{PRA}$-provably have the same $\Pi^0_2$ theorems and a fortiori are $\mathsf{PRA}$-provably equiconsistent).
