The law of double negation is the statement that the double negation of a proposition implies that proposition
equivalently, that the double negation of a proposition is logically equivalent to 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, we define the negation of a type as the function type from to the empty type ; . The law of double negation states that given a type , one could derive that one could get an element of in the context of a witness that is an h-proposition and a witness of the double negation of :
Given function types, this could be wrapped up as
The requirement that be an h-proposition is necessary; the law of double negation for h-sets is the set-theoretic choice operator, which implies the set-theoretic axiom of choice in addition to excluded middle, and the law of double negation for general types is the type-theoretic choice operator, which implies UIP in addition to the set-theoretic axiom of choice and excluded middle.
If one additionally has a Russell type of all propositions or a Tarski type of all propositions , the law of double negation could be expressed as an axiom:
There is an alternative presentation of the law of double negation, which uses an equivalence type for logical equivalence rather than a function type for implication:
In dependent type theory as foundations of mathematics, the requirement that be an h-proposition is also necessary. This alternate law of double negation for general types implies that all types are h-propositions a la propositional logic as a dependent type theory, since the double negation of a type is always an h-proposition:
Similarly, if one additionally has a Russell type of all propositions or a Tarski type of all propositions , this alternate law of double negation could be expressed as an axiom:
Last revised on August 9, 2023 at 15:13:03. See the history of this page for a list of all contributions to it.