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?

  • 4
    $\begingroup$ YES: RAA, Excluded Middle and Double Negation are all equivalent. $\endgroup$ Jan 15 '18 at 7:16
  • 2
    $\begingroup$ 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! $\endgroup$ Jan 15 '18 at 9:33
  • $\begingroup$ @PeterSmith: I can't understand how RAA can ever be called "negation introduction", when it eliminates rather than introduces "¬". $\endgroup$
    – user21820
    Aug 1 '19 at 14:51
  • $\begingroup$ 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".] $\endgroup$ Aug 1 '19 at 14:57

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.


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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.