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:
means the same as:
Formally:
Also:
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 more clearer example, It's not unreasonable is slightly less direct than It's reasonable.
¬ ¬ A
∴ A
¬ ¬ ¬ A
∴ ¬ A