The law of double negation is the statement that the double negation of a proposition implies that proposition
In classical logic, this is simply true. In constructive logic, it is equivalent to the law of excluded middle (because is a constructive theorem), and is not assertable in general.
In dependent type theory, the law of double negation states that given a type and a witness that it is an h-proposition, one could derive that one could get an element of in the context of a function from the function type from to the empty type to the empty type:
Last revised on January 26, 2023 at 08:47:07. See the history of this page for a list of all contributions to it.