Double Negative Elimination - Formal Notation

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:

    The conviction that the best way to prepare children for a harsh, rapidly changing world is to introduce formal instruction at an early age is wrong. There is simply no evidence to support it, and considerable evidence against it. Starting children early academically has not worked in the past and is not working now.
    David Elkind (20th century)