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?

  • 3
    $\begingroup$ $\Pi^0_1$-induction is equivalent to $\Sigma^0_1$-induction. With $\Sigma^0_0$-induction, you only get something like $RCA_0^*$ (without exponentiation) instead of $RCA_0$. (The explanation that “we want a base system to be as elementary as possible” is utter rubbish, as there are many much weaker systems.) With full induction, you get $RCA$. $\endgroup$ Feb 17 '19 at 9:03
  • $\begingroup$ @EmilJeřábek Would it be non-rubbish if "as elementary as possible" were accompanied by the constraint that we need to express some basic coding and prove its essential properties? $\endgroup$ Feb 17 '19 at 20:07
  • $\begingroup$ ISTR that it suffices to have the exponentiation axioms a^0 = 1, a^Sb = a a^b to code the incompleteness theorem, so it would seem no induction at all is necessary. $\endgroup$
    – luqui
    Feb 18 '19 at 1:04
  • 2
    $\begingroup$ @AndreasBlass No, it would not. You don’t need even remotely anything as strong as $\Sigma^0_1$-induction for basic coding. $\endgroup$ Feb 18 '19 at 9:07
  • $\begingroup$ @EmilJeřábek Thanks. $\endgroup$ Feb 18 '19 at 18:45

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.