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.