Exercise in Peano Arithmetic

Question

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? :)

Answer 1

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