So trying to prove:
i) $[t(n_0)\wedge \forall_n[t(n)\rightarrow t(n+1)]\Rightarrow \forall_{n_0\le n}t(n)]$
$\Rightarrow$
ii) $[s(n_0)\wedge s(n_1)\wedge\cdots \wedge s(n_k)\wedge\forall_n[s(n-k)\wedge s(n-k+1)\wedge\cdots \wedge s(n-1)\wedge s(n)\rightarrow s(n+1)]\Rightarrow \forall_{n_0\le n}s(n)]$
$1.)$ Let function $t(n) = s(n)\wedge s(n+1)\wedge\cdots \wedge s(n+k-1)\wedge s(n+k)$
$2.)$ assume $s(n_0)\wedge s(n_1)\wedge\cdots \wedge s(n_k)$
$3.)$ $\therefore t(n_0)$ $\space\space\space\space 1)$ and $2)$
$4.)$ assume $\forall_n[s(n-k)\wedge s(n-k+1)\wedge\cdots \wedge s(n-1)\wedge s(n)\rightarrow s(n+1)]$
$5.)$ for sbac $q\in Z$, $s(q-k)\wedge s(q-k+1)\wedge\cdots \wedge s(q-1)\wedge s(q)\rightarrow s(q+1)$ $\space\space\space\space 4)$ and Rule of Universal Specification
$6.)$ $\therefore s(q)\wedge s(q+1)\wedge\cdots \wedge s(q+k-1)\wedge s(q+k)\rightarrow s(q+k+1)$ $\space\space\space\space5)$
$7.)$ $s(q)\wedge s(q+1)\wedge\cdots \wedge s(q+k-1)\wedge s(q+k)\rightarrow s(q)\wedge s(q+1)\wedge\cdots \wedge s(q+k-1)\wedge s(q+k)$
$8.)$ ($(a\rightarrow b\wedge a\rightarrow c)\Rightarrow a\rightarrow b\wedge c$ established via truth table – omitted)
$10.)$ $s(q)\wedge s(q+1)\wedge\cdots \wedge s(q+k-1)\wedge s(q+k)\rightarrow s(q)\wedge s(q+1)\wedge\cdots \wedge s(q+k-1)\wedge s(q+k)\wedge s(q+k+1)$ $\space\space\space\space 6),7),8)$, Rule of Conjunction
$11.)$ $\forall_n[s(n)\wedge s(n+1)\wedge\cdots \wedge s(n+k-1)\wedge s(n+k)\rightarrow s(n)\wedge s(n+1)\wedge\cdots \wedge s(n+k-1)\wedge s(n+k)\wedge s(n+k+1)]$ $\space\space\space\space 10)$ and Rule of Universal Generalization
$12.)$ $\forall_n[t(n)\rightarrow t(n+1)]$ $\space\space\space\space 1)$ and $11)$
$13.)$ $\forall_{n_0\le n}t(n)$ $\space\space\space\space 3)$ and $12)$ and i)*
$14.)$ $\therefore \forall_{n_0\le n}s(n)$ $\space\space\space\space 1)$ and $13)$
Best Answer
Strong Induction :
To prove it from Induction , we have to define $Q(x) := (\forall z)(z \le x \rightarrow P(z))$ and apply Induction to $Q(x)$.
See Elliott Mendelson, Introduction to mathematical logic (4ed - 1997), PROPOSITION 3.9, page 166 :
Proof
(A)
(i) $(\forall x)((\forall z)(z < x \rightarrow P(z)) \rightarrow P(x))$ --- assumed
(ii) $(\forall z)(z < 0 \rightarrow P(z)) \rightarrow P(0))$ --- from (i) by $\forall$-elim
(iii) $(\forall z)\lnot (z < 0)$ --- provable from axioms
(iv) $(\forall z)(z < 0 \rightarrow P(z))$ --- from tautology : $\lnot A \rightarrow (A \rightarrow B)$ and (iii) and $\forall$-intro
(v) $P(0)$ --- from (ii) and (iv) by modus ponens
(vi) $(\forall z)(z \le 0 \rightarrow P(z))$ --- from the fact that : for any natural number $k$ and any formula $\varphi$, $\varphi(0) \land \varphi(1) \land \ldots \land \varphi(k) \leftrightarrow (\forall x)(x \le k \rightarrow \varphi(x))$.
But (vi) is $Q(0)$; thus, from (i)-(vi) we have :
(B)
In the same way, we prove that from assumptions : $(\forall x)((\forall z)(z < x \rightarrow P(z)) \rightarrow P(x))$ and $Q(x)$, $Q(x')$ follows [where $x'$ is $S(x)$, the "successor" of $x$].
Thus, by Deduction Theorem :
By (A), (B) and Induction, we obtain $(\forall x)((\forall z)(z < x \rightarrow P(z)) \rightarrow P(x)) \vdash (\forall x)Q(x)$, that is :
Hence, by rule $\forall$-elim twice , $(\forall x)((\forall z)(z < x \rightarrow P(z)) \rightarrow P(x)) \vdash (x \le x \rightarrow P(x))$.
But we have : $\vdash x \le x$.
Thus, $(\forall x)((\forall z)(z < x \rightarrow P(z)) \rightarrow P(x)) \vdash P(x)$; by $\forall$-intro and the Deduction theorem :