Double Negation

Double Negation Introduction

The rule of double negation introduction is a valid argument in types of logic dealing with negation $\neg$.

This includes propositional logic and predicate logic, and in particular natural deduction.

Proof Rule

If we can conclude $\phi$, then we may infer $\neg \neg \phi$.

Sequent Form

$p \vdash \neg \neg p$

Double Negation Elimination

The rule of double negation elimination is a valid argument in certain types of logic dealing with negation $\neg$.

This includes classical propositional logic and predicate logic, and in particular natural deduction, but for example not intuitionistic propositional logic.

Proof Rule

If we can conclude $\neg \neg \phi$, then we may infer $\phi$.

Sequent Form

$\neg \neg p \vdash p$

Combined Double Negation Law

These are often combined into one law:

Formulation 1

$p \dashv \vdash \neg \neg p$

Formulation 2

$\vdash p \iff \neg \neg p$

Double Negation from Intuitionistic Perspective

The intuitionist school rejects the Law of the Excluded Middle as a valid logical axiom.

This in turn invalidates the Law of Double Negation Elimination from the system of intuitionistic propositional logic.

Hence a difference is perceived between Double Negation Elimination and Double Negation Introduction, whereby it can be seen from the Principle of Non-Contradiction that if a statement is true, then it is not the case that it is false.

However, if all we know is that a statement is not false, we can not be certain that it is actually true without accepting that there are only two possible truth values.

Such distinctions may be important when considering, for example, multi-value logic.

However, when analysing logic from a purely classical standpoint, it is common and acceptable to make the simplification of taking just one Double Negation rule:

$p \dashv \vdash \neg \neg p$

Also see

• Definition:Logical Not
• Double Negation Elimination implies Law of Excluded Middle

Sources

• 1964: Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning ... (previous) ... (next): $\text{I}$: 'NOT' and 'IF': $\S 3$
• 1965: E.J. Lemmon: Beginning Logic ... (previous) ... (next): Chapter $1$: The Propositional Calculus $1$: $2$ Conditionals and Negation
• 1978: Thomas A. Whitelaw: An Introduction to Abstract Algebra ... (previous) ... (next): $\S 3$: Statements and conditions; quantifiers
• 1982: P.M. Cohn: Algebra Volume 1 (2nd ed.) ... (previous) ... (next): Chapter $1$: Sets and mappings: $\S 1.1$: The need for logic
• 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems ... (previous) ... (next): $\S 1.2.1$: Rules for natural deduction