How to derive $\bot \vdash P$ (EFQ)? I want to prove this statement (EFQ) using the natural deduction rules presented in the book Mathematical Logic (Chiswell & Hodges, 2007).  It does not explicitly state EFQ as one of the fundamental rules of inference, so I am trying to derive it somehow.  
The book provides the usual rules for $\wedge, \vee, \to$ introduction and elimination, which seem to agree with every other text that I have seen, but each text seems to differ on the rest of the rules.  C&H uses the following:
($\neg$E):   $P, \neg P \vdash \bot$
($\neg$I):  If $P \vdash \bot$, then $\vdash \neg P$
(RAA):  If $\neg P \vdash \bot$, then $\vdash P$
Is the following proof sufficient?


*

*$\bot$  (Initial premise)

*Assume $\neg P$

*Therefore, P (RAA using 1 and 2, discharges assumption on line 2)


I'm a little sketchy as to whether the use of RAA in line 3 is proper use, because the assumption is introduced after the $\bot$. Do you need to derive $\bot$ from $\neg P$ in order to use RAA?  If this proof is not legal, then how would I prove it?

I looked at the $RAA$ rule defined by the book:
It says that if you have a derivation $D$ of $\bot$, i.e. if you have:
$D$
$-$
$\bot$
then you can have a derivation of any statement $\phi$ as follows:
$D$
$-$
$\bot$
$-$ ($RAA$)
$\phi$ 
And it says:
"Its assumptions are those of $D$, except possibly $\neg \phi$"  
(by which they mean that if $\neg \phi$ is part of the undischarged assumptions of $D$, then you can remove $\neg \phi$)
OK, since you have $\bot$ as a premise, your 'derivation' of $\bot$ is just:
$\bot$
So, using the $RAA$ rule, this means we can now have the following derivation:
$\bot$
$-$ ($RAA$)
$P$ 
And that's it!  So, no assumption of $\neg P$ necessary: you can immediately infer $P$ from $\bot$ as a special case of the $RAA$ rule.
