Exchanging RAA with double negation: is this valid? In the system of natural deduction that I am working with in Mathematical Logic (Chiswell & Hodges), there are three rules of inference presented dealing with negation, as follows:
Negation introduction: If $\Gamma, P \vdash \bot$, then $\Gamma \vdash \neg P$
Negation elimination: $P \wedge \neg P \vdash \bot$
RAA: If $\Gamma, \neg P \vdash \bot$, then $\Gamma \vdash P$
If I replaced RAA with double negation ($\neg \neg P \vdash P$), would the system remain consistent and complete?
 A: I think given negation introduction and elimination, RAA and double negation are equivalent. Thus given negation introduction/elimination, the two systems should be equivalent regardless of which you take. Admittedly this is outside my area of expertise, or rather it's been a long time since I did formal logic. But I'm pretty sure regardless of which rule of inference you assume, you can derive the other as a derived rule of inference.
Proof:
Suppose RAA is a rule of inference, then assuming we have conjuction introduction (you didn't actually give a complete list of the inference rules in the text, so I'll just assume you have it), from $\neg\neg P, \neg P$, we can derive $\neg P \wedge \neg\neg P$, and hence $\bot$ by negation elimination. So $\neg\neg P,\neg P \vdash \bot$, so $\neg\neg P \vdash P$ by RAA.
On the other hand, if double negation is chosen, if $\Gamma,\neg P \vdash \bot$, then by negation introduction, $\Gamma \vdash \neg \neg P$, and by double negation, $\Gamma \vdash P$.
