# 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?

• YES: RAA, Excluded Middle and Double Negation are all equivalent. – Mauro ALLEGRANZA Jan 15 '18 at 7:16
• An aside: it is worth noting that, unfortunately, the labelling of ND rules varies across textbooks. I think the majority use "RAA" for what C&H call "Negation introduction". So you have to be on the alert if you dip into other books for help on issues! – Peter Smith Jan 15 '18 at 9:33
• @PeterSmith: I can't understand how RAA can ever be called "negation introduction", when it eliminates rather than introduces "¬". – user21820 Aug 1 '19 at 14:51
• If RAA is the rule "Given a proof from X to Absurd, you can derive not-X" you've introduced a negation, no? [Distinguish RAA proper, which is acceptable to an intuitionist, from the quite distinct rule which is sometimes called "classical reductio", i .e. "Given a proof from not-X to Absurd, you can derive X".] – Peter Smith Aug 1 '19 at 14:57

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