# nLab double negation

### Context

#### Topos Theory

Could not include topos theory - contents

# Double negation

## Idea

In logic, double negation is the operation that takes $P$ to $\neg{\neg{P}}$, where $\neg$ is negation. In other words, double negation is the composite of negation with itself. This is a closure operator/modality and as such a special case of a continuation monad.

## In logic

In classical logic, the double negation of any truth value or proposition is itself. More abstractly, double negation is the identity function on any boolean algebra.

In intuitionistic logic, double negation is weaker than the identity. That is, we have $P \Rightarrow \neg{\neg{P}}$ but not conversely. In paraconsistent logic, it is the other way around. More abstractly, this holds in any Heyting algebra (intuitionistic) or its dual (paraconsistent).

In linear logic, double negation is the identity again, although linear logic also has notions of intuitionistic negation and paraconsistent negation which act as above.

## In locale theory

Even in classical mathematics, a frame is a Heyting algebra but not a boolean algebra. Accordingly, double negation is usually not the identity on a frame. However, the operation of double negation is a nucleus on any frame.

Thus, every locale $L$ has a sublocale given by that nucleus, called the double negation sublocale and denoted $L_{\neg\neg}$. This sublocale is dense, and in fact it is the smallest dense sublocale of $L$, the intersection of all dense sublocales.

Classically, we have $L = L_{\neg\neg}$ if and only if $L$ is the discrete locale on some set $S$ of points. In constructive mathematics, $S$ must also have decidable equality.

###### Example

Let $\mathcal{O}_X$ be the sheaf of continuous (or smooth, or holomorphic, or regular?) functions on a topological space (or smooth manifold, or complex manifold, or reduced scheme) $X$. Then the pushforward of the pullback of $\mathcal{O}_X$ to the smallest dense sublocale of $X$ is the sheaf of meromorphic functions on $X$ (i.e. sections over an open subset $U$ are given by sections of $\mathcal{O}_X$ defined on some dense open subset $V \subseteq U$).

## In topos theory

The notion of double negation sublocale may be categorified from locales to toposes.

If $E$ is a topos with subobject classifier $\Omega$, there is a negation operator $\neg \colon \Omega \to \Omega$, defined by virtue of the fact that $\Omega$ is an internal Heyting algebra.

### Definition

###### Definition/Proposition

The double negation morphism

$\not \not \colon \Omega \to \Omega$

constitutes a Lawvere-Tierney topology on $\mathcal{E}$.

This is called the double negation topology.

###### Proof

The topology axioms can be formulated in purely equational form, i.e., as equations between operations of the form $\Omega^n \to \Omega$. By the Yoneda lemma, it suffices to verify the corresponding equations between transformations $Hom(-, \Omega)^n \to Hom(-, \Omega)$, which boils the problem down to checking the equations for ordinary Heyting algebras in $Set$. For ordinary Heyting algebras, proofs may be found here.

### Properties

###### Proposition

For $\mathcal{E}$ a sheaf topos, the sheaf topos corresponding to its double negation topology

$\mathcal{E}_{\not \not} \hookrightarrow \mathcal{E}$

is a Boolean topos.

This appears as MacLaneMoerdijk, theorem VI 3. The topos of double-negation sheaves is in fact the maximal Boolean subtopos contained in $E$.

###### Proposition

For every presheaf topos $[C^{op}, Set]$ the double negation topology coincides with the dense topology?.

This appears as MacLaneMoerdijk, corollary VI 5.

###### Proposition

Let $C$ be a poset. Then the double negation sheaf topos

$Sh_{\not \not}(C) \hookrightarrow [C^{op}, Set]$

satisfies the axiom of choice.

This appears as MacLaneMoerdijk, corollary VI 9.

###### Proposition

In a presheaf topos (on a small category) the notions of $\neg\neg$-topology and that of dense topology? coincide.

## In higher topos theory

Classically the double negation modality is equivalent to the n-truncation modality for $n = -1$ (the bracket type). In general, it's still true that double negation takes any type (object in the higher topos) to a $(-1)$-type, but the bracket type ${\|A\|_{-1}}$ only entails the double negation $\neg(\neg{A})$:

there is a canonical function

${\|A\|_{-1}} \longrightarrow \neg(\neg{A})$

and this is a 1-epimorphism precisely if the law of excluded middle holds.

## References

Section VI of

Revised on February 21, 2014 08:07:25 by Toby Bartels (64.89.53.163)