I'm doing some excercises from the book "The Incompleteness Phenomenom" from Goldstern and Judah.
I'm doing exercise about Peano Arithmetic and I have to show that:
$\vdash(\forall z\leq x(z\geq 1 \to z|y))\to(\forall z\leq Sx(z>1\to z|y·Sx))$
I think I have to use the deduction theorem, could you give me a hint? :)
Correct.
It can be useful to rewrite it as:
$∀z[z ≤ x \to (z≥1 → z|y)] \to ∀z [z ≤ Sx \to (z>1 → z|y⋅Sx)]$.
Thus, the formal proof needs the assumptions:
1) $∀z[z ≤ x \to (z≥1 → z|y)]$
2) $z ≤ Sx$
in order to derive:
$(z>1 → z|y⋅Sx)$.
The conclusion follows by Deduction Th, followed by Generalization Th, and Deduction Th again.
A good starting point can be Example 4.3.4 (2) [page 196]: $\mathsf {PA} \vdash z \le Sx \leftrightarrow z \le x \lor z = Sx$.
We have to apply it to 2) and use proof by cases [i.e. the tautology: $(p \to q) \to ((r \to q) \to (p \lor r \to q))$].
Case i): if $z=Sx$, then $z|Sx$ [because: $Sx=z⋅S0$]. Thus: $z|y⋅Sx$ and so [by the tautology: $p \to (q \to p)$]:
$(z > 1 → z|y⋅Sx)$.
Case ii): if $z \le x$, then, instantiating 1) and using modus ponens, we get: $(z≥1 → z|y)$.
We assume $z > 1$; thus: $z≥1$ [by the tautology: $p \to (p \lor q)$] and then, by modus ponens: $z|y$, and finally: $z|y⋅Sx$.
By Deduction Th we conclude again with:
$(z > 1 → z|y⋅Sx)$.
