Double Negation/Double Negation Elimination/Proof Rule
Contents
Theorem
The rule of Double Negation Elimination is a valid deduction sequent in propositional logic.
As a proof rule it is expressed in the form:
- If we can conclude $\neg \neg \phi$, then we may infer $\phi$.
It can be written:
- $\displaystyle {\neg \neg \phi \over \phi} \neg \neg_e$
Tableau Form
Let $\neg \neg \phi$ be a propositional formula in a tableau proof.
The Law of Double Negation Elimination is invoked for $\neg \neg \phi$ as follows:
Pool: | The pooled assumptions of $\neg \neg \phi$ | |||||||
Formula: | $\phi$ | |||||||
Description: | Double Negation Elimination | |||||||
Depends on: | The line containing the instance of $\neg \neg \phi$ | |||||||
Abbreviation: | $\text{DNE}$ or $\neg \neg \mathcal E$ |
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$
Technical Note
When invoking Double Negation Elimination in a tableau proof, use the {{DoubleNegElimination}}
template:
{{DoubleNegElimination|line|pool|statement|depends}}
or:
{{DoubleNegElimination|line|pool|statement|depends|comment}}
where:
line
is the number of the line on the tableau proof where Double Negation Elimination is to be invokedpool
is the pool of assumptions (comma-separated list)statement
is the statement of logic that is to be displayed in the Formula column, without the$ ... $
delimitersdepends
is the line of the tableau proof upon which this line directly dependscomment
is the (optional) comment that is to be displayed in the Notes column.
Sources
- 1964: Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning ... (previous) ... (next): $\text{I}$: 'NOT' and 'IF': $\S 3$
- 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