Double negation principle

Principle that, for any proposition P, P logically implies not-not-P, and not-not-P logically implies P.

Classical logic accepts both these halves of the principle, but intuitionist logic accepts only the first half, and not the second. This is because it accepts the law of contradiction (and so, given P, cannot allow not-P), but rejects the law of excluded middle(and so, given not-not-P, does not consider itself forced to accept P).

Source:
G T Kneebone, Mathematical Logic and the Foundations of Mathematics (1963), 243-50; elementary account of intuitionism

Elimination and introduction

‘Double negation elimination and double negation introduction are two valid rules of replacement. They are the inferences that if A is true, then not not-A is true and its converse, that, if not not-A is true, then A is true. 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 “{\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

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

{\displaystyle P\vdash \neg \neg P}

The double negation elimination rule may be written as:

{\displaystyle \neg \neg P\vdash 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 P\to \neg \neg P}

and

{\displaystyle \neg \neg P\to P}

These can be combined together into a single biconditional formula:

{\displaystyle \neg \neg P\leftrightarrow 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 {\displaystyle \neg \neg \neg A\vdash \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.

Proofs

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 {\displaystyle p\to p} proved here, which we refer to as (L1), and use the following additional lemma, proved here:

(L2) {\displaystyle p\to ((p\to q)\to q)}

We first prove {\displaystyle \neg \neg p\to p}. For shortness, we denote {\displaystyle q\to (r\to q)} 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 p\to \neg \varphi _{0})}       (instance of (A3))

(3) {\displaystyle (\neg p\to \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 p\to (\neg \neg \varphi _{0}\to \neg \neg p)}       (instance of (A1))

(6) {\displaystyle \neg \neg p\to (\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 p\to p}       (from (6) and (8) by the hypothetical syllogism metatheorem)

We now prove {\displaystyle p\to \neg \neg p}.

(1) {\displaystyle \neg \neg \neg p\to \neg p}       (instance of the first part of the theorem we have just proven)

(2) {\displaystyle (\neg \neg \neg p\to \neg p)\to (p\to \neg \neg p)}       (instance of (A3))

(3) {\displaystyle p\to \neg \neg p}       (from (1) and (2) by modus ponens)

And the proof is complete.