Is every proof for natural numbers equivalent to an induction proof?

Question

The other day I had the following idea: Suppose one could show that a theorem for natural numbers is not provable by induction for all $n$, in other words, there do not exist useful induction steps that would allow to prove the theorem for all $n$. Would this imply the theorem is undecidable?

Answer 1

Irrationality of $\sqrt 2$ does not seem to be provable by induction, but it does not make the theorem undecidable.

PS : Just because it seems unprovable by induction, does not mean it is unprovable by induction @Esokrates

Answer 2

An elegant revision of Peano's axioms for natural numbers treats the axiom scheme of induction as separate from some individual axioms for properties of zero, the successor function, addition, and multiplication.

The induction schema is therefore not needed to prove some theorems of Peano arithmetic. If your point of view is that such results are nevertheless "provable by induction" by combination with an unnecessary application of the induction schema, then it seems to me we are left with a condition that more simply is stated as "not provable in Peano arithmetic".

In any case there are certainly statements that can be refuted without use of the induction schema, so that it is not the case that being unprovable without induction implies undecidability. [NB: If Peano arithmetic were inconsistent as a formal first-order theory, then it would be decidable.]

---

There's some room for interpretation as to just what it means to separate the axiom scheme of induction from the theory $\textbf{PA}$ of Peano arithmetic. The six axioms from above:

1. $\forall x (0 \neq S(x))$
2. $\forall x,y (S(x) = S(y) \implies x = y)$
3. $\forall x (x + 0 = x)$
4. $\forall x,y (x + S(y) = S(x +y))$
5. $\forall x (x \cdot 0 = 0)$
6. $\forall x,y (x \cdot S(y) = (x \cdot y) + x)$

have been studied by Machover (1996, Set Theory, Logic, and Their Limitation, Cambridge University Press, p.256-7) and by Hájek and Pudlák (1998, Metamathematics of First-Order Arithmetic, 2nd Ed., Springer-Verlag, p.28). These give a theory $\textbf{PA}^-$ of discrete ordered semirings, whose models consist of an initial segment isomorphic to the natural numbers $\mathbb{N}$ followed by possible other "nonstandard" numbers.

If we add to these an axiom that every nonzero $x$ is a successor:

$$ \forall x (0 \neq x \implies \exists y (x = S(y))) $$

then we have a finitely axiomatized first-order theory $\textbf{Q}$ known as Robinson arithmetic. This extra axiom was identified by R.M. Robinson as the one implication of induction needed to make the proof that every computable function is representable in $\textbf{PA}$ go through, so $\textbf{Q}$ shares with $\textbf{PA}$ the property of essential incompleteness and undecidability.

Nevertheless $\textbf{Q}$ is unable to prove many theorems of $\textbf{PA}$, as for example the familiar commutative law of addition:

$$ \forall x,y (x + y = y + x) $$

despite being able to prove every concrete instance of this, nor to prove:

$$ \forall x (x \neq S(x)) $$

See Burgess (2005, Fixing Frege, Princeton University Press, p.56), citing Saul Kripke for the observation that cardinal numbers, with $S(x) = x+1$, are a natural model for $\textbf{Q}$ in which $x = S(x)$ is true of every infinite cardinal.