Exchanging RAA with double negation: is this valid?

Question

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?

Answer 1

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$.