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?