nLab law of double negation

Contents

Definition

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

¬¬AA. \not \not A \Rightarrow A \,.

equivalently, that the double negation of a proposition is logically equivalent to that proposition:

¬¬AA. \not \not A \iff 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, we define the negation of a type AA as the function type from AA to the empty type 𝟘\mathbb{0}; ¬AA𝟘\neg A \coloneqq A \to \mathbb{0}. The law of double negation states that given a type AA, one could derive that one could get an element of AA in the context of a witness that AA is an h-proposition and a witness of the double negation of AA:

ΓAtypeΓ,p:isProp(A),c:¬¬Adoubleneg A(p,c):A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, p:\mathrm{isProp}(A), c:\neg \neg A \vdash \mathrm{doubleneg}_A(p, c):A}

Given function types, this could be wrapped up as

ΓAtypeΓdoubleneg A:isProp(A)(¬¬AA)\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{doubleneg}_A:\mathrm{isProp}(A) \to (\neg \neg A \to A)}

The requirement that AA 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 Ω\Omega or a Tarski type of all propositions (Ω,El Ω)(\Omega, \mathrm{El}_\Omega), the law of double negation could be expressed as an axiom:

ΓctxΓdoubleneg: P:Ω(¬¬P)PRussellΓctxΓdoubleneg: P:Ω(¬¬El Ω(P))El Ω(P)Tarski\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{doubleneg}:\prod_{P:\Omega} (\neg \neg P) \to P}\mathrm{Russell} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{doubleneg}:\prod_{P:\Omega} (\neg \neg \mathrm{El}_\Omega(P)) \to \mathrm{El}_\Omega(P)}\mathrm{Tarski}

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:

ΓAtypeΓdoubleneg A:isProp(A)((¬¬A)A)\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{doubleneg}_A:\mathrm{isProp}(A) \to ((\neg \neg A) \simeq A)}

In dependent type theory as foundations of mathematics, the requirement that AA 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:

ΓAtypeΓdoubleneg A:(¬¬A)A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{doubleneg}_A:(\neg \neg A) \simeq A}

Similarly, if one additionally has a Russell type of all propositions Ω\Omega or a Tarski type of all propositions (Ω,El Ω)(\Omega, \mathrm{El}_\Omega), this alternate law of double negation could be expressed as an axiom:

ΓctxΓdoubleneg: P:Ω(¬¬P)PRussellΓctxΓdoubleneg: P:Ω(¬¬El Ω(P))El Ω(P)Tarski\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{doubleneg}:\prod_{P:\Omega} (\neg \neg P) \simeq P}\mathrm{Russell} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{doubleneg}:\prod_{P:\Omega} (\neg \neg \mathrm{El}_\Omega(P)) \simeq \mathrm{El}_\Omega(P)}\mathrm{Tarski}

References

Last revised on August 9, 2023 at 15:13:03. See the history of this page for a list of all contributions to it.