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! :)
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]
Thus, from 1) and 7) :
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$$