The **double negation rule** is a rule in logic that holds that a proposition is equivalent to its double negation (double negative).

The double negation takes the form of "A is equivalent to not not A", or "A implies and is implied by not not A".

The rule may also take the form of:

**α ¬¬α**

Where α is any proposition or formula. The symbol, , is used to signify two-way inference, or equivalence. The symbol ⇔ is sometimes used for the same purpose.

Although it is very simple, the double negation rule is not a basic rule of inference — that is, it may be described by more fundamental rules. To justify the double negation rule using basic rules, we may construct two proofs, one of each direction of inference, as follows.

To show that A ¬¬A:

1 A Pr.

RTP ¬¬A

2 ¬A AIP

RTP Contradiction

3 A R, 1

4 ¬¬A ¬I, 2–3

And to show that ¬¬A A:

1 ¬¬A Pr.

RTP A

2 ¬A AIP

RTP Contradiction

3 ¬¬A R, 1

4 A ¬E, 2–3

The basic rules used to demonstrate this derived rule are the *introduction* and *elimination* rules for negation (¬). These are the two versions of the proof by contradiction (*reductio ad absurdum* method).