Natural Deduction - use RAA

Question

Give natural deduction proofs showing each of the following:

a) $\phi\vdash\top$ for any formula $\phi$.

b) $(P_1\to P_2)\vdash (\lnot P_2\to\lnot P_1)$.

c) $(\lnot P_2\to\lnot P_1)\vdash (P_1\to P_2)$ (Hint: This requires reductio ad absurdum).

---

I have solved both a) and b) but not c). I don't really understand RAA more than it's proof by contradiction. And I don't understand when to use it or where i should use it. Is RAA always the last step in your proof tree or can you use it in some earlier stage? In my case do I want to assume $\lnot(\lnot P_2\to\lnot P_1)$ and try to contradict this fact by comming up with something nonsense which can't be true?

---

Here is my attempt to solve the problem:

$$\frac{\frac{\frac{\lnot(\lnot P_2\to\lnot P_1)\to\lnot P_2\to\lnot P_1\quad \quad[\lnot(\lnot P_2\to\lnot P_1)]}{\lnot P_2\to\lnot P_1}\to I \quad \quad \lnot P_2}{\lnot P_1}\to I\quad \quad [P_1]^1}{\frac{\bot}{P_1\to P_2}RAA}\to I.$$

So I worked my way from bottom to top when i constructed the proof tree. I think the two last step (bottom of the tree) are logic to me. I "think" I really believe in these two steps. But then I start to become unsure and I am not fully aware of what I'm doing. Hope someone can help me. Thanks! :)

Answer 1

1) $¬P_2 → ¬P_1$ --- premise

2) $¬P_2$ --- assumed [a]

3) $¬P_1$ --- from 1) and 2) by $\to$-elim

4) $P_1$ --- assumed [b]

5) $\bot$ --- from 4) and 3) by $\to$-elim ($\lnot A $ is $A \to \bot$)

6) $P_2$ --- from 2) and 5) by RAA, discharging [a]

7) $P_1 → P_2$ --- from 4) and 6) by $\to$-intro, discharging [b].

Thus, from 1) and 7) :

$(¬P_2 → ¬P_1) \vdash (P_1 → P_2)$.

---

Here the same as a proof-tree :

$$\frac{\frac{\lnot P_2\to\lnot P_1 \quad \quad [\lnot P_2]^1}{\lnot P_1}\to E\quad \quad [P_1]^2}{\frac {\frac{\bot}{P_2}RAA_1}{P_1 \to P_2}\to I_2}\to E$$