Is this a correct natural deduction proof for $\{(\phi\vee\psi),\neg\phi\}\vdash\psi$?

Question

I'm not sure I used RAA correctly by putting $\neg\psi$ next to $\bot$ and discharging it.

Answer 1

I see the idea (the notation is different to what I'm used to). You want to use $\lor$-elimination to conclude $\psi$ from $\phi \lor \psi$.

My write-up would be (the left hand clauses I call axioms)

1. $\phi \lor \psi$ (axiom)
2. $\psi$ (assumption 1)
3. $\psi \Rightarrow \psi$ (assumption 1 is dropped), by $\Rightarrow$-introduction.
4. $\phi$ (assumption 2)
5. $\lnot \phi$ (axiom)
6. $\bot$ (from 4 and 5), introduction of $\bot$.
7. $\psi$ (from 6 and Ex Falso Quodlibet, EFQ)
8. $\phi \Rightarrow \psi$ by $\Rightarrow$ introduction. Asumption 2 dropped. 6,7 go away.
9. $\psi$, by 1., 3. and 8. and $\lor$-elimination.

(normally I'd use indentation for subproofs of implication, RAA etc. as well)

If I understand your proof correctly your strategy is a bit different: you first assume $\phi$, from which you get $\bot$ (using the axiom $\lnot \phi$), and then (maybe you don't have EFQ as a rule) you use $\lnot \psi$ as a temporary second assumption to get $\psi$ with RAA (reductio ad absurdum). The assumption $\psi$ goes away and then $\phi$ goes away to get the implication. This is also possible, of course. The RAA is used correctly, AFAIK. But I'd use Ex Falso Quodlibet, which is a bit more direct.