Formal Notation
The double negation introduction rule may be written in sequent notation:
The double negation elimination rule may be written as:
In rule form:
and
or as a tautology (plain propositional calculus sentence):
and
These can be combined together into a single biconditional formula:
- .
Since biconditionality is an equivalence relation, any instance of ¬¬A in a well-formed formula can be replaced by A, leaving unchanged the truth-value of the well-formed formula.
Double negative elimination is a theorem of classical logic, but not of weaker logics such as intuitionistic logic and minimal logic. Because of their constructive flavor, a statement such as It's not the case that it's not raining is weaker than It's raining. The latter requires a proof of rain, whereas the former merely requires a proof that rain would not be contradictory. (This distinction also arises in natural language in the form of litotes.) Double negation introduction is a theorem of both intuitionistic logic and minimal logic, as is .
In set theory also we have the negation operation of the complement which obeys this property: a set A and a set (AC)C (where AC represents the complement of A) are the same.
Read more about this topic: Double Negative Elimination
Famous quotes containing the word formal:
“True variety is in that plenitude of real and unexpected elements, in the branch charged with blue flowers thrusting itself, against all expectations, from the springtime hedge which seems already too full, while the purely formal imitation of variety ... is but void and uniformity, that is, that which is most opposed to variety....”
—Marcel Proust (1871–1922)