nLab law of double negation

Definition

The law of double negation is the statement that the double negation of a proposition implies that proposition

$$\not \not A \Rightarrow A \,.$$

In classical logic, this is simply true. In constructive logic, it is equivalent to the law of excluded middle (because $\not \not (P \vee \not P)$ is a constructive theorem), and is not assertable in general.

In dependent type theory

In dependent type theory, the law of double negation states that given a type $A$ and a witness that it is an h-proposition, one could derive that one could get an element of $A$ in the context of a function from the function type from $A$ to the empty type to the empty type:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, a:A, b:A \vdash \mathrm{proptrunc}_A(a, b):a =_A b}{\Gamma, c:(A \to \mathbb{0}) \to \mathbb{0} \vdash \mathrm{doubleneg}(c):A}$$

Related concepts

• excluded middle

• ex falso quodlibet

• closed subspace

References

• eomDouble negation, law of