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

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?

-
Some statements cannot be proven by direct induction on the proposition itself, a stronger statement has to be proven with induction and then the desired result is a corollary. – DanielV Dec 1 '13 at 19:56
Is that your experience, or is there a proof for that? – Esokrates Dec 1 '13 at 19:57
More of an observation. Obviously if you are generalizing $P(x)$ to $Q(x)$, then you could still use induction on $P$ and when you get to the inductive case, prove the inductive case with induction on $Q$. But in that approach while you are using induction on $P$ it is a vacuous application of it. – DanielV Dec 1 '13 at 20:07

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.

-

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

-
Consider the Irrationality of $sqrt(2)$ is not a theorem about natural numbers. – Esokrates Dec 1 '13 at 17:51
Rationality of $\sqrt{2}$ could be expressed in first-order theory of natural numbers, $\exists p \exists q$ s.t. $p^2 = 2q^2 \gt 0$. – hardmath Dec 1 '13 at 17:53
And the usual proof uses the well ordering principle in $\Bbb N$, which is equivalent to induction. – Git Gud Dec 1 '13 at 17:59
Just because it seems unprovable by induction, does not mean it is unprovable by induction. – Esokrates Dec 1 '13 at 18:02
@Esokrates : Very true, what the hell was I thinking. That is usually my line as well. – Arjang Dec 1 '13 at 19:54