Double negative elimination

In logic and the propositional calculus, double negative elimination is a rule that states that double negatives can be removed from a proposition without changing its meaning:

It's not the case that it's not raining.

means the same as:

It's raining.

Formally:

  ¬ ¬ A
  ∴ A

Also:

  ¬ ¬ ¬ A
  ∴ ¬ A

The rule of double negative introduction states the converse, that double negatives can be added without changing the meaning of a proposition.

This rule is true in classical logic, but in intuitionistic logic, the statement, It's not the case that it's not raining. is weaker than It's raining.. As a slightly clearer example, It's not unreasonable is slightly less direct than It's reasonable.

In naive set theory also we have the negation operation of the complement which obeys this property: a set A and a set A'' (where A' represents the complement of A) are the same.