$(\forall n, {\rm T} \vdash P(n)) \Rightarrow ({\rm T} \vdash \forall n, P(n))$ Why is it false?

Question

I'm wondering why do we "need" a proof of mathematical induction.

Let's $T$ be our theory and $P$ our property. $\vdash$ means that there is a proof.

Thanks to induction : $\forall n$, ${\rm T} \vdash P(n)$, (so ${\rm T} \vdash P(0)$, ${\rm T} \vdash P(1)$, ${\rm T} \vdash P(2)$, ${\rm T} \vdash P(3)$, ...)

Why can't we imply : ${\rm T} \vdash \forall n, P(n)$ ?

And even if there is a good reason for that, why can it be a problem ?

Answer 1

My previous answer was aimed at the title question; I think the current answer better addresses the actual question.

---

To begin with, let me talk about induction and induction-like principles outside of the natural numbers.

Let's start by considering $\mathbb{R}$. Both $0$ and "$+1$" make sense in $\mathbb{R}$, so we can formulate the statement of proof by induction:

$(WI)\quad$ If $P$ holds of $0$ and $P(n)\implies P(n+1)$ for all $n\in\mathbb{R}$, then $P(n)$ holds for all $n$.

This however is blatantly false: take $P$ to be"is an integer." Hence the name "$WI$" for "wrong induction."

An arguably more interesting example occurs in the context of ordinals. These are generalizations of the natural numbers "past the finite." If we take $P$ to be "is finite," we again see a failure of induction: $0$ is finite, and $n$ being finite implies that $n+1$ is finite, but there are infinite ordinals. The reason this example is interesting is that there is a version of induction which works for ordinals:

$(TransInd)\quad$ Suppose $P$ is a property of ordinals such that $(i)$ $P$ hods of $0$, $(ii)$ if $P(n)$ holds then $P(n+1)$ holds for all ordinals $n$, and $(iii)$ if $P(\alpha)$ holds for all $\alpha<\lambda$ then $P(\lambda)$ holds for limit ordinals $\lambda$. Then in fact $P$ holds of all ordinals.

(In fact, clause $(iii)$ is enough on its own.)

Similarly, there is an "induction-like" principle which works in the context of the real numbers (and other situations). One instance of it is:

$(TopInd)\quad$ Suppose $P$ is a property of real numbers which holds of $0$ and such that whenever $P$ holds of every nonnegative real less than $x$, then $P$ holds of $x$. Then $P$ holds of every nonnegative real.

This uses the completeness property of the reals, and can be used to give a slick proof of the Heine-Borel theorem.

---

OK, what does this have to do with your question?

Well, the point is that proof by induction relies on some structural properties of the natural numbers; there are contexts (like the reals or the ordinals) where we can state induction, but where induction is false. So from the point of view of axiomatics, we can't take induction for granted. Maybe we explicitly include proof by induction (or rather, a scheme of axioms for proof by induction) as axioms in our theory, but something justifying induction needs to appear explicitly in our axioms: pure logic alone isn't enough to justify induction, since there are contexts where induction doesn't work.

Answer 2

Actually there is a much simpler 'reason': $ \def\nn{\mathbb{N}} $

(1) "$\forall n \in \nn\ ( T \vdash P(n) )$" expands to "$\forall n \in \nn\ \exists q \in Strings\ ( \text{$q$ is a proof over $T$ of $P(n)$} )$".

(2) "$T \vdash \forall n ( P(n) )$" expands to "$\exists q \in Strings\ ( \text{$q$ is a proof over $T$ of ($\forall n ( P(n) )$)} )$".

On the face of it, it is similar to an invalid quantifier switch; informally $\forall \exists$ does not imply $\exists \forall$.

Of course, this is not a proof that it fails, but it should have given you a very clear warning that if your claim is true at all it must be due to some rather deep reason. For example, continuity of a real function on a compact set does imply uniform continuity, and this theorem is literally a quantifier switch of this kind, and the proof is not logically trivial.

Worse still, in this case there are two severe problems. Firstly, the "$n$" is not even of the same type! In (1) it has to be encoded as a term of the form "$0$" or "$1+\cdots+1$" before "$P(n)$" makes sense as a string that could be proven. If you did not realize this coding issue, it implies that you have made a type-error. Let me say again: It is only meaningful to talk about whether a string is provable or not within some first-order theory. It is not meaningful to talk about whether the theory $T$ can prove something about a natural number in the meta-system, unless you first encode it. This is why careful authors will write something like "$\forall n \in \nn\ ( T \vdash P(\overline{n}) )$" where "$\overline{n}$" is defined to be the term of the form I described above with the correct number of ones. In contrast, in (2) the "$n$" is merely a variable in the language of the theory, so whether or not $T$ proves "$\forall n \in \nn\ ( P(n) )$" or not is purely a syntactic question about $T$ and has nothing to do with any interpretation of $T$ (even if the intended domain of $T$ is the naturals). Hence it is already a type-error to shift the quantifier.

Secondly, one can ask whether it makes sense to include your reasoning as a rule. This has been considered before, and even has a name: the ω-rule. The big problem is that there is no computable procedure for determining whether or not "$\forall n \in \nn\ ( T \vdash P(n) )$" is true, for any consistent theory $T$ extending PA that has a proof verifier program. This is because $T$ proves ($\neg Proof_T(\overline{k},\ulcorner 0=1 \urcorner)$) for every natural $k$, but does not prove ($\forall n \neg Proof_T(n,\ulcorner 0=1 \urcorner)$), by the incompleteness theorem, where $Proof_T(x,y)$ is some formula that captures the statement ($x$ codes a proof of the sentence coded by $y$). In other words, PA is ω-incomplete.