Double negation – Wikipedia
From Wikipedia, the free encyclopedia
Propositional logic theorem
Type  Theorem 

Field  
Statement  If a statement is true, then it is not the case that the statement is not true.” 
Symbolic statement 
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.” This is expressed by saying that a proposition A is logically equivalent to not (notA), 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:

 “This is the principle of double negation, i.e. a proposition is equivalent of the falsehood of its negation.”
Elimination and introduction[edit]
Double negation elimination and double negation introduction are two valid rules of replacement. They are the inferences that, if not notA is true, then A is true, and its converse, that, if A is true, then not notA 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
P
and the double negation elimination rule is:
P
Where “
${displaystyle Rightarrow }$” is a metalogical symbol representing “can be replaced in a proof with.”
In logics that have both rules, negation is an involution.
Formal notation[edit]
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 into a single biconditional formula:
Since biconditionality is an equivalence relation, any instance of ¬¬A in a wellformed formula can be replaced by A, leaving unchanged the truthvalue of the wellformed 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
${displaystyle neg neg neg Avdash neg A}$.
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.
In classical propositional calculus system[edit]
In Hilbertstyle 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.
 A2.
 A3.
We use the lemma
${displaystyle pto p}$proved here, which we refer to as (L1), and use the following additional lemma, proved here:
 (L2)
We first prove
${displaystyle neg neg pto p}$. For shortness, we denote
${displaystyle qto (rto q)}$by φ_{0}. We also use repeatedly the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps.
 (1)
 (2)
 (3)
 (4)
 (5)
 (6)
 (7)
 (8)
 (9)
We now prove
${displaystyle pto neg neg p}$.
 (1)
 (2)
 (3)
And the proof is complete.
See also[edit]
References[edit]
 ^ 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[edit]
 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, NorthHolland Publishing Company, Amsterdam NY, ISBN 0720421039.
 Stephen C. Kleene, 1967, Mathematical Logic, Dover edition 2002, Dover Publications, Inc, Mineola N.Y. ISBN 0486425339
 Alfred North Whitehead and Bertrand Russell, Principia Mathematica to *56, 2nd edition 1927, reprint 1962, Cambridge at the University Press.
Recent Comments