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 \emptyset) \to \emptyset \vdash \mathrm{doubleneg}(c):A}

If one doesn’t have function types, the law of double negation could be expressed as

ΓAtypeΓ,a:A,b:Aproptrunc A(a,b):a= AbΓ,a:A,b(a):,c(a,b):doubleneg(a,b,c):A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, a:A, b:A \vdash \mathrm{proptrunc}_A(a, b):a =_A b}{\Gamma, a:A, b(a):\emptyset, c(a, b):\emptyset \vdash \mathrm{doubleneg}(a, b, c):A}


Last revised on December 8, 2022 at 21:46:57. See the history of this page for a list of all contributions to it.