I often see two variations in how the principle of strong induction is stated:
First Variation: $\Big(B\!\subseteq\!\mathbb{N}\wedge1\!\in\!B\wedge\big(\forall x[x\!\leq\!k\rightarrow x\!\in\!B]\rightarrow k\!+\!1\!\in\!B\big)\Big)\longrightarrow B\!=\!\mathbb{N}$
Second Variation: $\Big(B\!\subseteq\!\mathbb{N}\wedge\big(\forall x[x\!<\!k\rightarrow x\!\in\!B]\rightarrow k\!\in\!B\big)\Big)\longrightarrow B\!=\!\mathbb{N}$
Are these logically equivalent (superficially, it seems that they are, but I am having difficulty proving that they are). And is one variation preferred over the other, or does it basically depend on the specific problem at hand?
For context, I am assuming only the following axioms and definitions:
Peano Axioms:
(P1) $\ \exists x[x\!=\!1]$;
(P2) $\ $there exists an unary ("successor") function $S$ on $\mathbb{N}$ (i.e., $x\!\in\!\mathbb{N}\rightarrow S(x)\!\in\!\mathbb{N}$);
(P3) $\ \forall x[S(x)\!\neq\!1]$;
(P4) $\ \forall x\forall y[S(x)\!=\!S(y)\rightarrow x\!=\!y]$
(P5) $\ $Principle of Mathematical Induction
Addition
(A1) $\forall x[S(x)=x+1]$
(A2) $\forall x\forall y[x+S(y)=S(x\!+\!y)]$
Order Relation
(O1) $\ x\!<\!y\leftrightarrow\exists z[x\!+\!z\!=\!y]$
(O2) $\ x\!\leq\!y\leftrightarrow[x\!=\!y\vee x\!<\!y]$
You need to quantify the $k$, so you get:
$$\Big(B\!\subseteq\!\mathbb{N}\wedge1\!\in\!B\wedge\forall k\big(\forall x[x\!\leq\!k\rightarrow x\!\in\!B]\rightarrow k\!+\!1\!\in\!B\big)\Big)\longrightarrow B\!=\!\mathbb{N}$$
and
$$\Big(B\!\subseteq\!\mathbb{N}\wedge\forall k\big(\forall x[x\!<\!k\rightarrow x\!\in\!B]\rightarrow k\!\in\!B\big)\Big)\longrightarrow B\!=\!\mathbb{N}$$
But if you do so, they are arithmetically equivalent. Using the other axioms, you should be able to derive the one from the other. Here is the general strategy:
First, you can use weak induction to prove that:
$$\forall x (x \not =1 \rightarrow \exists y \ x = y+1)$$
And you can also use weak induction to show things like:
$$\forall x \ x+1 \not =x$$
And:
$$\forall x \ \neg x <x$$
And:
$$\forall x \forall y (x \le y \leftrightarrow x < y+1)$$
and:
$$\forall x \ \neg x <1$$
And:
$$\forall x \ 1 \le x$$
Now let's derive version 2 from version 1.
So we assume $$\forall k (\forall x (x<k \rightarrow x \in B) \rightarrow k \in B)) \tag{1}$$
And we need to show that:
$$1 \in B \land \forall k (\forall x (x \le k \rightarrow x \in B) \rightarrow k+1 \in B)\tag{2}$$
To show $1 \in B$, simply instantiate $(1)$ with $1$: then, since nothing is smaller than $1$, that makes the antecedent true, and hence we get $1 \in B$
For the other part, assume that for some arbitrary $k$:
$$\forall x (x \le k \rightarrow x \in B)$$
Instantiate $(1)$ with $k+1$:
$$\forall x (x < k+1 \rightarrow x \in B) \rightarrow k+1 \in B$$
And since $x <k+1 \leftrightarrow x \le k$, you thus get $k+1 \in B$ as desired.
Deriving version 1 from version 2:
So now we assume $(2)$, and try to prove $(1)$
Ok, so for some arbitrary $k$ assume
$$\forall x (x < k \rightarrow x \in B)$$
Where want to show $k \in B$
Well, if $k=1$, we're done, since we have $1 \in B$ from $(2)$
If $k \not =1$, then $k = m+1$ for some $m$. But since $x < m+1 \leftrightarrow x \le m$, we thus have
$$\forall x (x \le m \rightarrow x \in B)$$
and thus we get $m+1 \in B$ from $(2)$, i.e. $k \in B$ as desired.
Personally I prefer working with the second; it's simpler and looks less like weak induction. But often times you'll end up having to prove the $n=1$ 'base case' separately anyway.