2
$\begingroup$

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

$\endgroup$
2
$\begingroup$

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

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.