Natural Deduction - use RAA

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

• You have misapplied RAA ... having derived $\bot$, you have to discharge by RAA $\lnot P_2$ deriving $P_2$ and then discharge $P_1$ deriving $P_1 \to P_2$. But in this case, you are left with the two top left assumptions open ... Delete them and start directly from the premise. Commented Sep 13, 2015 at 10:00
• Ah okay thanks, but how do i know when to apply RAA then? Is this something you just "see" when you have done a bunch of these kind of problems?
– user231999
Commented Sep 13, 2015 at 10:04
• In order to apply RAA, you must start with a $\lnot \ldots$ premise; in this case, if we try to start from the negation of the conclusion : $\lnot (P_1 \to P_2)$ we are in trouble because we have no "easy way" to remove the outer $\lnot$: we need again RAA ? Thus, we have to try with $\lnot P_2$. Commented Sep 13, 2015 at 10:07

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