Give a derivation in Peano Arithmetic

Question

I'm doing some excercises from the book "The Incompleteness Phenomenom" from Goldstern and Judah.

Show that: $\vdash \exists y[y>1 \wedge \forall z(z\leq 0\wedge z>1\to z|y)]$

Hint: Show that $\vdash [2>1 \wedge \forall z(z\leq 0\wedge z>1\to z|2)]$

I think I have to prove that $\vdash [2>1 \wedge \forall z(z\leq 0\wedge z>1\to z|2)]\to \exists y[y>1 \wedge \forall z(z\leq 0\wedge z>1\to z|y)]$(by $\exists$-introduction is easy) and that $\vdash [2>1 \wedge \forall z(z\leq 0\wedge z>1\to z|2)]$(this is the difficult T.T).

But I don't know how to get it. Thanks!!

Answer 1

Example 4.3.4 [page 196]: $\mathsf {PA} \vdash z \le 0 \leftrightarrow z=0$.

Thus, $z \le 0 \land z > 1$ is equivalent to: $z=0 \land z > 1$.

Thus, by laws of equality, we have $0 > 1$: contradiction.

So: $\lnot (z \le 0 \land z > 1)$ and thus [by the tautology: $\lnot p \to (p \to q)$]:

$(z \le 0 \land z > 1) \to z|2$.

This is true for $z$ whatever, and thus we can use the Generalization Th (1.4.27) to conclude with:

$\forall z \ [(z \le 0 \land z > 1) \to z|2]$.

Then we have to prove $2 > 1$, which is: $S(1) > 1$, and we can "add them" [by the tautology: $p \to (q \to (p \land q))$] to get:

$\mathsf {PA} \vdash 2 > 1 \land \forall z \ [(z \le 0 \land z > 1) \to z|2]$.

For the final step, use Lemma 1.4.31 (Introduction of $\exists$) [page 87].