prove weak induction implies strong induction

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)$

Strong Induction :

$(\forall x)((\forall z)(z < x \rightarrow P(z)) \rightarrow P(x)) \rightarrow (\forall x)P(x)$.

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 :

$(\forall x)((\forall z)(z < x \rightarrow P(z)) \rightarrow P(x)) \vdash Q(0)$.

(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 :

$(\forall x)((\forall z)(z < x \rightarrow P(z)) \rightarrow P(x)) \vdash (\forall x)(Q(x) \rightarrow Q(x'))$.

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 :

$(\forall x)((\forall z)(z < x \rightarrow P(z)) \rightarrow P(x)) \vdash (\forall x)(\forall z)(z \le x \rightarrow P(z))$.

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 :

$(\forall x)((\forall z)(z < x \rightarrow P(z)) \rightarrow P(x)) \vdash (\forall x)P(x)$.

• (A)(iii)? Proved it before? – miniparser Oct 24 '14 at 18:51
• Shouldn't it be $\neg (z<0)$? Is that just because we're only dealing with natural numbers? Thanks. – miniparser Oct 26 '14 at 19:39