How to complete proof of strong induction from weak induction I am wanting a proof of strong induction from weak induction.  This has been answered here, and I can follow the proof except for how part B is obtained.   Assuming that:
$\forall x(\forall z(z < x \to P(z)) \to P(x))$ 
and  
$\forall z(z \le x \to P(z))$ --- defined as "$Q(x)$"
are true, I need to derive $Q(s(x))$.  That is, $\forall z(z \le s(x) \to P(z))$, where $s$ is the successor function.
All I can achieve is the following: 


*

* $\forall x(\forall z(z < x \to P(z)) \to P(x))$  --Assume

* $\forall z(z \le x \to P(z))$  --Assume $Q(x)$

* ???

* ???

* $\forall z(z \le s(x) \to P(z))$

* $Q(s(x))$

* $Q(x) \to Q(s(x))$

* $\forall x(Q(x) \to Q(S(x)))$

* $\forall x(\forall z(z < x \to P(z)) \to P(x)) \vdash \forall x(Q(x) \to Q(S(x)))$


Can anyone help me with this?
 A: The trick is to instantiate your proof's overall assumption on line 1 with $s(x)$ for $x$ (for part A, you had to instantiate $0$ for $x$, but for part B you instantiate $s(x)$).
I do this on line 3 (exactly where you got stuck):
$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$ 
$\fitch{
1.  \forall x (\forall z (z < x \rightarrow P(z)) \rightarrow P(x)) \quad Assume}
{\fitch{
2. \forall z (z \le x \rightarrow P(z)) \quad Assume}{
3. \forall z (z < s(x) \rightarrow P(z)) \rightarrow P(s(x)) \quad \forall \ Elim \ 1\\
\fitch {
4. z < s(x) \quad Assume}{
5. z \le x \quad from \ 4\\
6. P(z) \quad from \ 2,5}\\
7. \forall z (z < s(x) \rightarrow P(z)) \quad \forall \ Intro \ 4-6\\
8. P(s(x)) \quad \rightarrow \ Elim \ 3,7\\
\fitch{
9. z \le s(x) \quad Assume}{
10. z < s(x) \lor z = x \quad \ from \ 9\\
\fitch{
11. z < s(x) \quad Assume
}{
12. P(z) \quad from \ 7,11}\\
\fitch{
13. z = s(x)}{
14. P(z) \quad = \ Elim \ 8,13}\\
15. P(z) \quad \lor \ Elim \ 10,11-12,13-14}\\
16. \forall z (z \le s(x) \rightarrow P(z)) \quad \forall \ Intro \ 9-15} \\}$
