Do $P(0)$ and $P(n)\implies P(n+1)$ yield $P(5)$ without an axiom of induction?

Question

As I understand it, Peano arithmetic needs the axiom of induction to prevent non-standard models of the natural numbers.

Given $P(0)$ and $P(n)\implies P(n+1) \forall n\in \mathbb{N}$ I can apply modus ponens to get $P(1)$ and again to get $P(2)$. After 5 iterations, I should have deduced $P(5)$. Is this reasoning correct?

It seems the important part of the induction axiom is that it asserts $P(n)$ for all $n$ in the model, where without this axiom we could have elements not reachable from $0$ by iterated succession.

Does this mean that for any particular "ordinary" natural number that can be obtained by writing $S$ sufficiently many times in my formula, I can deduce $P(S(S(...S(0)))$ without appealing to the axiom of induction?

Answer 1

Does this mean that for any particular "ordinary" natural number that can be obtained by writing $S$ sufficiently many times in my formula, I can deduce $P(S(S(...S(0)))$ without appealing to the axiom of induction?

Yes, you can. To be exact, if you have

$$P(0)$$

and

$$\forall n (P(n) \to P(s(n)))$$

then you can prove $P(S(S(...S(0)))$ without the axiom of induction.

Indeed, even if the axiom of induction would be assumed to be false, i.e. if you also have:

$$\neg ((P(0) \land \forall n (P(n) \to P(s(n)))) \to \forall n \ P(n))$$

you can still infer $P(S(S(...S(0)))$

And this isn't because you can now suddenly prove a contradiction, because as you point out, there are non-standard models in which the axiom of induction is false, but where $P(0)$ and $\forall n (P(n) \to P(s(n)))$ are still true. No, it's simply because you can keep instantiating the $\forall n (P(n) \to P(s(n)))$ to get $P(s(0))$, $P(s(s(0)))$, etc.

Answer 2

Does this mean that for any particular "ordinary" natural number that can be obtained by writing $S$ sufficiently many times in my formula, I can deduce $P(S(S(...S(0)))$ without appealing to the axiom of induction

That is actually the logical equivalent of the axiom of induction. Essentially, this axiom is used to rule out the existence disconnected subsets of N that are inaccessible from $0$ by repeated succession.

In general, if $f: X\to X$, $~x_0 \in X~$ and $~X=\{x_0,f(x_0), f(f(x_0)), \cdots \}$, then induction can be said to hold on $(X,f,x_0)$, where $f$ is the "successor function" on $X$ and $x_0$ is the "first element" of $X$.

$~~~~~~~\forall P\subset X:[x_0 \in P~\land~\forall a\in P: [ f(a)\in P] \implies P=X]$

Available on request, the formal proof (228 lines) is too long to post here. (I am told by moderators not to have links to proofs in an answer. I think I can post a link in a comment if requested.)