I'm having troubles with exercise *162a in "Introduction to Metamathematics", by S.C. Kleene, 1952.
The ask is to prove:
(1) $ \vdash A(0) \& \forall x [\forall y (y \leq x \Rightarrow A(y)) \Rightarrow A(x')] \Rightarrow A(x)$
where x and y are variables distinct from each other, y is free for x in A(x) and does not occur free in A(x).
Kleene's hint is to proof:
(2) $ \vdash A(0) \& \forall x [\forall y (y \leq x \Rightarrow A(y)) \Rightarrow A(x')] \vdash \forall y (y \leq x \Rightarrow A(y))$
and
(3) $ \vdash \forall y (y \leq x \Rightarrow A(y)) \vdash A(x)$
from which (1) follows. He also suggests that (2) can be proofed using the induction rule, which requires the proof of:
(4) $\vdash A(0) \& \forall x [\forall y (y \leq x \Rightarrow A(y)) \Rightarrow A(x')] \vdash \forall y (y \leq 0 \Rightarrow A(y))$
and of
(5) $\vdash A(0) \& \forall x [\forall y (y \leq x \Rightarrow A(y)) \Rightarrow A(x')], \forall y (y \leq x \Rightarrow A(y)) \vdash \forall y (y \leq x' \Rightarrow A(y))$
I managed to prove (3), but I'm struggling with (4) and (5). Can you help? Thanks
Hint for (4): by induction with $P(y) := (y \le 0 \to A(y))$.
$A(0)$ by assumption; thus, using $P \to (Q \to P)$ and MP, we get $(0 \le 0) \to A(0)$.
Assume $P(y)$ and prove $P(y+1)$. But $P(y+1)$ is $(y+1 \le 0 \to A(y+1))$ and $\lnot (y+1 \le 0)$, because $y+1$ is a successor and we know that no successor can be equal to $0$.
Thus, using tautology $\lnot P \to (P \to Q)$ and MP we get $P(y+1)$.
Thus: $P(y) \to (P(y+1)$; $y$ is not free in the assumption and we can generalize it to get: $\forall y (P(y) \to (P(y+1))$. With $P(0)$, by Induction: $\forall y ((y \le 0) \to A(0))$.
Hint for (5)
Using the second part of the fist premise instantiating the leading quantifier we have: $∀y(y≤x \to A(y)) \to A(x')$ and using 2nd premise and MP we get: $A(x')$ and thus $y=x' \to A(y)$. From which: $y=x' \vdash (y \le x' \to A(y))$.
If $y≤x'$ we have $y \le x \lor y=x'$. Thus, assuming $y \le x$ from 2nd premise we have $A(y)$ and so $y \le x \to A(y)$ and also $y \le x \vdash (y \le x' \to A(y))$.
Thus, from $y \le x \lor y=x'$ by cases, we get: $y \le x' \to A(y)$