# Double negation

__: Propositional logic theorem__

**Short description**Type | Theorem |
---|---|

Field | |

Statement | If a statement is true, then it is not the case that the statement is not true." |

Transformation rules |
---|

Propositional calculus |

Rules of inference |

Rules of replacement |

Predicate logic |

In propositional logic, **double negation** is the theorem that states that "If a statement is true, then it is not the case that the statement is not true."^{[citation needed]} This is expressed by saying that a proposition *A* is logically equivalent to *not (not-A*), or by the formula A ≡ ~(~A) where the sign ≡ expresses logical equivalence and the sign ~ expresses negation.^{[1]}

Like the law of the excluded middle, this principle is considered to be a law of thought in classical logic,^{[2]} but it is disallowed by intuitionistic logic.^{[3]} The principle was stated as a theorem of propositional logic by Russell and Whitehead in *Principia Mathematica* as:

- [math]\displaystyle{ \mathbf{*4\cdot13}. \ \ \vdash.\ p \ \equiv \ \thicksim(\thicksim p) }[/math]
^{[4]} - "This is the principle of double negation,
*i.e.*a proposition is equivalent of the falsehood of its negation."

- [math]\displaystyle{ \mathbf{*4\cdot13}. \ \ \vdash.\ p \ \equiv \ \thicksim(\thicksim p) }[/math]

## Elimination and introduction

**Double negation elimination** and **double negation introduction** are two valid rules of replacement. They are the inferences that, if *not not-A* is true, then *A* is true, and its converse, that, if *A* is true, then *not not-A* is true, respectively. The rule allows one to introduce or eliminate a negation from a formal proof. The rule is based on the equivalence of, for example, *It is false that it is not raining.* and *It is raining.*

The *double negation introduction* rule is:

*P [math]\displaystyle{ \Rightarrow }[/math] [math]\displaystyle{ \neg }[/math][math]\displaystyle{ \neg }[/math]P*

and the *double negation elimination* rule is:

*[math]\displaystyle{ \neg }[/math][math]\displaystyle{ \neg }[/math]P [math]\displaystyle{ \Rightarrow }[/math] P*

Where "[math]\displaystyle{ \Rightarrow }[/math]" is a metalogical symbol representing "can be replaced in a proof with."

In logics that have both rules, negation is an involution.

### Formal notation

The *double negation introduction* rule may be written in sequent notation:

- [math]\displaystyle{ P \vdash \neg \neg P }[/math]

The *double negation elimination* rule may be written as:

- [math]\displaystyle{ \neg \neg P \vdash P }[/math]

In rule form:

- [math]\displaystyle{ \frac{P}{\neg \neg P} }[/math]

and

- [math]\displaystyle{ \frac{\neg \neg P}{P} }[/math]

or as a tautology (plain propositional calculus sentence):

- [math]\displaystyle{ P \to \neg \neg P }[/math]

and

- [math]\displaystyle{ \neg \neg P \to P }[/math]

These can be combined into a single biconditional formula:

- [math]\displaystyle{ \neg \neg P \leftrightarrow P }[/math].

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. Double negation introduction is a theorem of both intuitionistic logic and minimal logic, as is [math]\displaystyle{ \neg \neg \neg A \vdash \neg A }[/math].

Because of their constructive character, 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.

## Proofs

### In classical propositional calculus system

In Hilbert-style deductive systems for propositional logic, double negation is not always taken as an axiom (see list of Hilbert systems), and is rather a theorem. We describe a proof of this theorem in the system of three axioms proposed by Jan Łukasiewicz:

- A1. [math]\displaystyle{ \phi \to \left( \psi \to \phi \right) }[/math]
- A2. [math]\displaystyle{ \left( \phi \to \left( \psi \rightarrow \xi \right) \right) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right) }[/math]
- A3. [math]\displaystyle{ \left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right) }[/math]

We use the lemma [math]\displaystyle{ p \to p }[/math] proved here, which we refer to as (L1), and use the following additional lemma, proved here:

- (L2) [math]\displaystyle{ p \to ((p \to q) \to q) }[/math]

We first prove [math]\displaystyle{ \neg \neg p \to p }[/math]. For shortness, we denote [math]\displaystyle{ q \to ( r \to q ) }[/math] by φ_{0}. We also use repeatedly the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps.

- (1) [math]\displaystyle{ \varphi_0 }[/math] (instance of (A1))
- (2) [math]\displaystyle{ (\neg \neg \varphi_0 \to \neg \neg p ) \to (\neg p \to \neg \varphi_0) }[/math] (instance of (A3))
- (3) [math]\displaystyle{ (\neg p \to \neg \varphi_0) \to (\varphi_0 \to p ) }[/math] (instance of (A3))
- (4) [math]\displaystyle{ (\neg \neg \varphi_0 \to \neg \neg p ) \to (\varphi_0 \to p ) }[/math] (from (2) and (3) by the hypothetical syllogism metatheorem)
- (5) [math]\displaystyle{ \neg \neg p \to ( \neg \neg \varphi_0 \to \neg \neg p ) }[/math] (instance of (A1))
- (6) [math]\displaystyle{ \neg \neg p \to (\varphi_0 \to p ) }[/math] (from (4) and (5) by the hypothetical syllogism metatheorem)
- (7) [math]\displaystyle{ \varphi_0 \to ((\varphi_0 \to p) \to p) }[/math] (instance of (L2))
- (8) [math]\displaystyle{ (\varphi_0 \to p) \to p }[/math] (from (1) and (7) by modus ponens)
- (9) [math]\displaystyle{ \neg \neg p \to p }[/math] (from (6) and (8) by the hypothetical syllogism metatheorem)

We now prove [math]\displaystyle{ p \to \neg \neg p }[/math].

- (1) [math]\displaystyle{ \neg\neg\neg p \to \neg p }[/math] (instance of the first part of the theorem we have just proven)
- (2) [math]\displaystyle{ (\neg\neg\neg p \to \neg p) \to (p \to \neg\neg p) }[/math] (instance of (A3))
- (3) [math]\displaystyle{ p \to \neg \neg p }[/math] (from (1) and (2) by modus ponens)

And the proof is complete.

## See also

## References

- ↑ Or alternate symbolism such as A ↔ ¬(¬A) or Kleene's *49
^{o}: A ∾ ¬¬A (Kleene 1952:119; in the original Kleene uses an elongated tilde ∾ for logical equivalence, approximated here with a "lazy S".) - ↑ Hamilton is discussing Hegel in the following: "In the more recent systems of philosophy, the universality and necessity of the axiom of Reason has, with other logical laws, been controverted and rejected by speculators on the absolute.[
*On principle of Double Negation as another law of Thought*, see Fries,*Logik*, §41, p. 190; Calker,*Denkiehre odor Logic und Dialecktik*, §165, p. 453; Beneke,*Lehrbuch der Logic*, §64, p. 41.]" (Hamilton 1860:68) - ↑ The
^{o}of Kleene's formula *49^{o}indicates "the demonstration is not valid for both systems [classical system and intuitionistic system]", Kleene 1952:101. - ↑ PM 1952 reprint of 2nd edition 1927 pp. 101–02, 117.

## Bibliography

- William Hamilton, 1860,
*Lectures on Metaphysics and Logic, Vol. II. Logic; Edited by Henry Mansel and John Veitch*, Boston, Gould and Lincoln. - Christoph Sigwart, 1895,
*Logic: The Judgment, Concept, and Inference; Second Edition, Translated by Helen Dendy*, Macmillan & Co. New York. - Stephen C. Kleene, 1952,
*Introduction to Metamathematics*, 6th reprinting with corrections 1971, North-Holland Publishing Company, Amsterdam NY, ISBN:0-7204-2103-9. - Stephen C. Kleene, 1967,
*Mathematical Logic*, Dover edition 2002, Dover Publications, Inc, Mineola N.Y. ISBN:0-486-42533-9 - Alfred North Whitehead and Bertrand Russell,
*Principia Mathematica to *56*, 2nd edition 1927, reprint 1962, Cambridge at the University Press.

Original source: https://en.wikipedia.org/wiki/Double negation.
Read more |