Why induction is defined as an implication instead of an "if and only if" statement?

Question

The formal definition of induction, taken from wikipedia, is written as

$$\forall P.\,[[P(0)\land \forall (k\in \mathbb {N} ).\,[P(k)\implies P(k+1)]]\implies \forall (n\in \mathbb {N} ).\,P(n)]$$

But then, it is this version true?

$$\forall P.\,[[P(0)\land \forall (k\in \mathbb {N} ).\,[P(k)\implies P(k+1)]]\iff \forall (n\in \mathbb {N} ).\,P(n)]\tag{1}$$

If it is not true can you show me why? (I cant found a counterexample.) Thank you.

---

The background of this question is that if $(1)$ is true then the proof for the equivalence of weak induction ($W$) and strong induction ($S$) is really trivial.

Let the shortened theorem of strong induction to be $$S\implies \forall (n\in \mathbb {N} ).\,P(n)$$

and by $(1)$ the definition of weak induction $$W\iff \forall (n\in \mathbb {N} ).\,P(n)$$

The case $S\implies W$ is trivial but now the case $W\implies S$ is trivial too because we can verify that

$$\forall (n\in \mathbb {N} ).\,P(n)\implies S$$

Answer 1

Of course it is true, but the $\Longleftarrow$ direction is trivially true as a matter of logic, so writing $\Longrightarrow$ directs the reader's focus to the interesting direction.

If $\forall n\, P(n)$ then clearly $P(0)$ is true, and clearly also any formula of the form $\cdots\Rightarrow P(k+1)$ will be true.

Answer 2

The implication from left to right is the key property that the ordering of the natural numbers satisfies. (In fact, a second-order version of induction uniquely characterizes the set of natural numbers.)

But the implication from right to left holds trivially for any structure at all: If $A$ is any set, $a_0$ is any member of $A,$ and $f\colon A\to A$ is any function, then we have

$$(\forall P) \Big(\big((\forall x\in A)\,P(x)\big) \implies \big(P(a_0)\land (\forall x\in A)\,\big(P(x)\implies P(f(x))\big)\Big).$$

So this reversed implication tells us nothing interesting about $\mathbb{N}.$

Answer 3

Induction is 1/2 of the definition of $\forall$ for natural numbers. It is the rule that let's you introduce $\forall$. It is:

$$\frac{P(0),~ (P(n) \vdash P(n + 1))}{\forall m~P(m)}$$

Note that it is not $\forall n P(n) \implies P(n+1)$. In induction, $n$ is treated as a free variable. How exactly would you prove $\forall n P(n) \implies P(n+1)$ if you don't already have a rule for introducing $\forall$? Induction is the rule for introducing $\forall$ so it can't depend on it already being introduced.

The rule for eliminating $\forall$ is (roughly) :

$$\frac{\forall m~P(m)}{P(n)}$$

So there are 2 reasons it is not an equivalence: first, induction is (usually) an inference, not an axiom, and inferences are 1 directional. Second, the reverse direction isn't useful, the elimination rule is what you want for the reverse direction.