nLab law of double negation




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

¬¬AA. \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 ¬¬(P¬P)\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 AA and a witness that it is an h-proposition, one could derive that one could get an element of AA in the context of a function from the function type from AA to the empty type to the empty type:

ΓAtypeΓ,a:A,b:Aproptrunc A(a,b):a= AbΓ,c:(A𝟘)𝟘doubleneg(c):A\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}


Last revised on January 26, 2023 at 08:47:07. See the history of this page for a list of all contributions to it.