I've been thinking about the propositions one can prove using the Peano axioms lately and there's this one question that crossed my mind.
I understand that the axiom of induction was introduced to remove 'unwanted' elements from $\mathbb{N}$. These 'unwanted' elements would be objects that obey the first four axioms, but are detached from the list of objects obtained through applying the successor function repeatedly on $0$ (i.e. detached from the $0$, $S(0)$, $S(S(0)) ...$ list).
I believe I understand the logic behind how the axiom of induction achieves this. My question is whether we can rigorously prove the statement
$\forall n \in \mathbb{N} (\text{n can be reached by applying the successor function sufficiently many times to 0})$.
I know that this statement that I just wrote down is informal, but I'm not sure how I should restate such a statement in a more rigorous way. However, if I stick to this informal statement, I can use induction to heuristically justify my claim:
Proof: Let $P(n)$ be the statement 'n can be reached by applying the successor function sufficiently many times to 0'.
$P(0)$ is automatically true, since $0$ is already equal to $0$.
Now we suppose $P(n)$ is true for some arbitrary $n \in \mathbb{N}$. This means $n$ can be expressed as something like $S(...(0)...)$.
Then this implies $P(S(n))$ is also true, since $S(n) = S(S(...(0)...))$.
So this closes the induction, and $\forall n \in \mathbb{N} (P(n))$ is true.
I was wondering whether it's possible to reframe this claim and proof into a more logically rigorous form.
Thank you very much in advance for taking the time to read through my question.
Induction tries to accomplish this, but it doesn’t, really. We know this is because, if Peano is consistent, it has models which are uncountable infinite.
Gödel shows us, amongst other things, why we can’t encode our full intuition about the natural numbers with human-usable axioms - a set of axioms that allow human (or computer) to check a proof.
Your statement is really “every natural number can be expressed as a finite number of applications of $S.$” Well that requires a rigorous definition of “finite,” which is what we are studying when we study the natural numbers. If we define $S^k$ as $S^0(x)=x$ and $S^{k+1}(x)=S(S^k(x))$ we can prove , by induction, that $S^n(0)=n.$
But that is circular - our ability to define $S^k$ uses induction, which could end up “accidentally” defining $S^k$ for “non-intuitive” natural numbers $k.$
Induction, intuitively, is an outline for an infinite proof - we know how to prove $P(0),$ from there we know how to prove $P(1), P(2),\dots.$ So, intuitively, we know how to prove it for all natural numbers.
But the proofs by induction are a severely limited form of infinite proof[*]. And this limitation means that it is possible that any statement $P(n)$ which can be proved by induction also applies to non-intuitive natural numbers.
Induction puts big restrictions on non-intuitive natural numbers, so that they have to almost seem magical. It is relatively easy to find non-intuitive models without induction, but even with, it doesn’t keep them from existing in models of Peano.
[*] An example of an infinite proof that cannot be outlined by an induction proof is any statement $P(n)$ like the Goldbach conjecture that can be checked in finite time for each $n.$ If Goldbach is true, there is an infinite proof where, for each $n\geq 2,$ we show primes $p,q$ with $p+q=2n.$ There might be no rhyme or reason connecting the examples for each $n.$
[Indeed, if Goldbach is undecidable from Peano, then intuitively it is true, because otherwise there would be a counter-example. And this is why, if it is undecidable, we can’t prove it is undecidable - if we could prove undecidability, we could turn this proof into a proof there is no counterexample, which would be a proof of Goldbach.]