Double negation – Wikipedia

Propositional logic theorem

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 (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:

${displaystyle mathbf {*4cdot 13} . vdash . p equiv thicksim (thicksim p)}$

^[4]

“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 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

${displaystyle Rightarrow }$

${displaystyle neg }$

${displaystyle neg }$

P

and the double negation elimination rule is:

${displaystyle neg }$

${displaystyle neg }$

P

${displaystyle Rightarrow }$

P

Where “

” 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:

${displaystyle Pvdash neg neg P}$

The double negation elimination rule may be written as:

${displaystyle neg neg Pvdash P}$

In rule form:

${displaystyle {frac {P}{neg neg P}}}$

and

${displaystyle {frac {neg neg P}{P}}}$

or as a tautology (plain propositional calculus sentence):

${displaystyle Pto neg neg P}$

and

${displaystyle neg neg Pto P}$

These can be combined into a single biconditional formula:

${displaystyle neg neg Pleftrightarrow P}$

.

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

.

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 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.

${displaystyle phi to left(psi to phi right)}$

A2.

${displaystyle left(phi to left(psi rightarrow xi right)right)to left(left(phi to psi right)to left(phi to xi right)right)}$

A3.

${displaystyle left(lnot phi to lnot psi right)to left(psi to phi right)}$

We use the lemma

proved here, which we refer to as (L1), and use the following additional lemma, proved here:

(L2)

${displaystyle pto ((pto q)to q)}$

We first prove

. For shortness, we denote

by φ₀. We also use repeatedly the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps.

(1)

${displaystyle varphi _{0}}$

      (instance of (A1))

(2)

${displaystyle (neg neg varphi _{0}to neg neg p)to (neg pto neg varphi _{0})}$

      (instance of (A3))

(3)

${displaystyle (neg pto neg varphi _{0})to (varphi _{0}to p)}$

      (instance of (A3))

(4)

${displaystyle (neg neg varphi _{0}to neg neg p)to (varphi _{0}to p)}$

      (from (2) and (3) by the hypothetical syllogism metatheorem)

(5)

${displaystyle neg neg pto (neg neg varphi _{0}to neg neg p)}$

      (instance of (A1))

(6)

${displaystyle neg neg pto (varphi _{0}to p)}$

      (from (4) and (5) by the hypothetical syllogism metatheorem)

(7)

${displaystyle varphi _{0}to ((varphi _{0}to p)to p)}$

      (instance of (L2))

(8)

${displaystyle (varphi _{0}to p)to p}$

      (from (1) and (7) by modus ponens)

(9)

${displaystyle neg neg pto p}$

      (from (6) and (8) by the hypothetical syllogism metatheorem)

We now prove

.

(1)

${displaystyle neg neg neg pto neg p}$

      (instance of the first part of the theorem we have just proven)

(2)

${displaystyle (neg neg neg pto neg p)to (pto neg neg p)}$

      (instance of (A3))

(3)

${displaystyle pto neg neg p}$

      (from (1) and (2) by modus ponens)

And the proof is complete.

See also[edit]

References[edit]

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, 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.