Double-Negation Elimination

Double-negation elimination is an inference rule in logic that permits a proposition $A$ to be inferred from $\neg\neg A$, read “it is not the case that not $A$.” It is valid in classical logic, but is not generally derivable in intuitionistic logic. Its status distinguishes two approaches to reasoning: classically, ruling out the falsity of a proposition establishes it; intuitionistically, this need not provide the evidence required to establish the proposition itself. (plato.stanford.edu)

Formal statement

In natural deduction, the rule is written

Here $A$ can be any formula, not merely an atomic proposition. In an axiomatic presentation, the corresponding axiom schema is

The rule and schema are interderivable using implication introduction and modus ponens. They apply to formulas of both propositional logic and first-order logic. Adding unrestricted double-negation elimination to ordinary intuitionistic logic yields classical logic. (suppescorpus.stanford.edu)

The reverse implication,

is called double-negation introduction and is intuitionistically valid. Given $A$, temporarily assume $\neg A$; the two yield a contradiction, so the temporary assumption is refuted. Classical logic therefore establishes the full equivalence $\neg\neg A\leftrightarrow A$, whereas intuitionistic logic generally establishes only the introduction direction. (leanprover.github.io)

Classical interpretation

Under classical truth-functional semantics, negation reverses a truth value. Applying it twice restores the original value. A truth table consequently assigns $A$ and $\neg\neg A$ identical values:

Thus $\neg\neg A\rightarrow A$ is a tautology. The equivalence concerns logical negation with a specified meaning, rather than every expression that resembles a double negative in ordinary language. Different logical systems can give negation different properties, so the classical truth-table argument does not establish its validity in all systems. (plato.stanford.edu)

Relationship to excluded middle and contradiction

Over intuitionistic logic, unrestricted double-negation elimination is equivalent to the law of excluded middle,

To derive elimination from excluded middle, assume $\neg\neg A$ and reason by cases. In the $A$ case, the conclusion is immediate. In the $\neg A$ case, the assumption $\neg\neg A$ produces a contradiction, from which $A$ follows by the principle of explosion. Conversely, intuitionistic reasoning proves $\neg\neg(A\lor\neg A)$; double-negation elimination then gives excluded middle. (leanprover.github.io)

The rule also licenses classical proof by contradiction. If assuming $\neg A$ leads to falsity, discharging that assumption establishes $\neg\neg A$. Elimination supplies the final step to $A$. This must be distinguished from proving a negative statement: deriving a contradiction from an assumption $A$ and concluding $\neg A$ is already intuitionistically acceptable. The classical addition is the unrestricted transition from a refuted negation to a positive conclusion. (leanprover.github.io)

Constructive interpretation and countermodels

Under the Brouwer–Heyting–Kolmogorov interpretation, a proof of an implication is a construction transforming proofs of its antecedent into proofs of its consequent. Negation is understood as implication to falsity:

Accordingly, a proof of $\neg\neg A$ transforms any purported refutation of $A$ into a contradiction. Such a transformation need not supply a proof of $A$, particularly when establishing $A$ requires choosing a disjunct or providing an existential witness. This explains the constructive distinction between $A$ and its double negation. (leanprover.github.io)

An illustrative countermodel uses Kripke semantics. Consider two states $w_0\leq w_1$, with an atomic proposition $p$ forced at $w_1$, but not at $w_0$. Negation is forced at a state only if its argument is forced at no accessible extension. Neither state forces $\neg p$, since $p$ holds at $w_1$. Therefore $w_0$ forces $\neg\neg p$, although it does not force $p$. By the soundness of intuitionistic reasoning for these models, unrestricted elimination is not intuitionistically derivable. This example illustrates the semantic definitions rather than treating an unestablished proposition as false. (cs.cmu.edu)

Restricted validity and proof translation

Failure of the general schema does not exclude particular instances. A proposition is called stable when $\neg\neg A\rightarrow A$ is provable. If $A\lor\neg A$ is available constructively for a particular proposition, elimination holds for that proposition by the same case argument used above. Negated propositions are also stable: intuitionistically,

Thus rejecting unrestricted elimination does not mean rejecting every removal of two negation signs. (plato.stanford.edu)

In proof theory, double-negation translations connect classical and intuitionistic systems without asserting unrestricted elimination. Glivenko’s theorem states that a propositional formula $A$ is classically provable exactly when $\neg\neg A$ is intuitionistically provable. This simple formulation does not extend unchanged to first-order logic; more elaborate negative translations are used there. (plato.stanford.edu)

The distinction also appears in type theory through the Curry–Howard correspondence: constructive implication proofs behave like functions, while unrestricted elimination requires additional classical reasoning. In the Lean proof assistant, classical proof by contradiction can be expressed with Classical.byContradiction; from a hypothesis $h:\neg\neg A$, applying it to $h$ yields a proof of $A$. This makes the classical step explicit within a formal proof. (leanprover.github.io)