Return to Answer

In my opinion, the only way for anyone to really understand induction is to really understand the logical structure behind it. So a prerequisite is a complete grasp of working in first-order logic, for which I recommend both boolean algebra and natural deduction (Fitch-style) in conjunction. It is unfortunate that many people, teachers and students alike, don't actually appreciate how important this is, and hence they try to teach induction to students who are so weak in logic that they cannot possibly know what they understand or do not understand about induction.

There is a first-order induction schema that we can use to have something like induction in a first-order theory like PA, but the original intuition is not first-order at all. Incidentally, PA with second-order induction (and full semantics) is categorical (has only one model), but the usual PA which has first-order induction has infinitely many non-standard models. Second-order induction correctly captures our intuition, but second-order logic does not satisfy the completeness theorem or compactness theorem unlike first-order logic.

Also, the induction axiom does not imply that (A) always implies (B). If (A) always implies (B), then the formal system is ω-complete. However, PA is ω-incomplete if it is consistent, because it cannot prove $\mathrm{Con}(PA)$, which is a sentence of the form $\forall n\ ( \neg \mathrm{CodesAProofOfFalse}(n) )$, even though it can prove $\neg \mathrm{CodesAProofOfFalse}(n)$ for each natural number $n$ encoded as $\underbrace{1+1+\cdots+1}_{\text{$n$ times}}$.

Finally, note that throughout this answer, in the meta-logic "natural number" refers to the true natural numbers (which is ultimately undefinable), while in the logic "natural numbers" are simply defined by the properties they obey, such as the axiom of induction. The axioms including induction serve as how we characterize the natural numbers, but no recursive axiomatization can ever fully characterize them. So the best way we can describe these true natural numbers is what I gave at the start: Exactly those that we can get by counting upwards from $0$. =)

In my opinion, the only way for anyone to really understand induction is to really understand the logical structure behind it. So a prerequisite is a complete grasp of working in first-order logic, for which I recommend both boolean algebra and natural deduction (Fitch-style) in conjunction. It is unfortunate that many people, teachers and students alike, don't actually appreciate how important this is, and hence they try to teach induction to students who are so weak in logic that they cannot possibly know what they understand or do not understand about induction.

Also, induction does not imply that (A) always implies (B). If (A) always implies (B), then the formal system is ω-complete. However, PA is ω-incomplete if it is consistent, because it cannot prove $\mathrm{Con}(PA)$, which is a sentence of the form $\forall n\ ( \neg \mathrm{CodesAProofOfFalse}(n) )$, even though it can prove $\neg \mathrm{CodesAProofOfFalse}(n)$ for each natural number $n$ encoded as $\underbrace{1+1+\cdots+1}_{\text{$n$ times}}$.

Finally, note that throughout this answer, in the meta-logic "natural number" refers to the true natural numbers (which is ultimately undefinable), while in the logic "natural numbers" are simply defined by the properties they obey, such as the axiom of induction. The axioms including induction serve as part of how we characterize the natural numbers, but no recursive axiomatization can ever fully characterize them. So although the true natural numbers are exactly those that we can get by counting upwards from $0$, there will never be a systematic non-circular definition of them. (In particular, "we can get by counting upwards" presupposes natural steps.)

$P(0)$. (1)

 

$\forall n \in \nn\ ( P(n) \imp P(n+1) )$. (2)

$P(0) \imp P(1)$ [from instantiating (2)]. (3)

 

$P(1)$ [from (1) and (3)]. (4)

 

$P(1) \imp P(2)$ [from instantiating (2)]. (5)

 

$P(2)$ [from (4) and (5)]. (6)

 

...

(A) Is it true that for any $n \in \nn$, there some proof that $P(n)$ is true? Yes, and we've shown above how to construct one.

 

(B) Is it true that there some proof that $P(n)$ is true for any $n \in \nn$? No!

$P(0)$. (1)

$\forall n \in \nn\ ( P(n) \imp P(n+1) )$. (2)

$P(0) \imp P(1)$ [from instantiating (2)]. (3)

$P(1)$ [from (1) and (3)]. (4)

$P(1) \imp P(2)$ [from instantiating (2)]. (5)

$P(2)$ [from (4) and (5)]. (6)

...

(A) Is it true that for any $n \in \nn$, there some proof that $P(n)$ is true? Yes, and we've shown above how to construct one.

(B) Is it true that there some proof that $P(n)$ is true for any $n \in \nn$? No!

Intuition for Induction

It is now clear that given any natural number $n$ written in decimal notation, one can prove $P(n)$ by continuing the above proof up to a length of $2n$ lines. So there are two questions:

It should now be clear why the induction axiom is really a meta-logical axiom intrinsically. The quantification in (A) is outside the formal system with the usual deductive rules, while the quantification in (B) is inside the formal system. It essentially stipulates that whenever we can systematically generate a proof of $P(n)$ for every $n \in \nn$ in the above manner, we can transfer this meta-logical universal quantifier inside the formal system itself.

Notes

Intuition for Induction (after the logic foundation is firm)

It is now clear that given any natural number $n$ written in decimal notation, one can prove $P(n)$ by continuing the above proof up to a length of $2n$ lines. Of course, this fact about what we can prove is not something proven within the formal system itself, but is an external fact observed from the outside. All this fact requires is that we have the same common understanding about strings from a fixed alphabet (with which we form proofs) and how we can manipulate strings (joining them together, reading each symbol in order, ...). But it is not a fact provable within the formal system. In other words, this fact is a meta-logical fact. "Meta-logic" means "about logic", since we're now thinking not within the logical framework we set up but thinking about the logical framework from the outside.

So there are two questions:

Together with the earlier comment about the meta-logical intuition behind induction, it should now be even clearer why the induction axiom is really a meta-logical axiom intrinsically. The quantification in (A) is outside the formal system with the usual deductive rules, while the quantification in (B) is inside the formal system. It essentially stipulates that whenever we can systematically generate a proof of $P(n)$ for every $n \in \nn$ in the above manner, we can transfer this meta-logical universal quantifier inside the formal system itself.

Notes (only for the teacher, not the student learning induction!)