nLab 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.

The double negation translation says that a proposition $P$ is provable in classical logic precisely if its double negation $\not \not P$ is provable in constructive logic.

The double negation topology closes morphisms under double negation (def. below), and its category of sheaves forms a boolean topos (prop. below). This notably serves to capture the forcing of set theory in terms of topos theory (classifying topoi), see also remark below.

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.

In classical mathematics, if $L$ is a spatial locale, then we have $L = L_{\neg\neg}$ if and only if $L$ is the discrete locale on some set $S$ of points. In constructive mathematics, the same holds except that $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(n elementary) 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.

Remark

A topos $\mathcal{E}$ such that $\mathcal{E}_{\neg\neg}$ is an open subtopos is called $\bot$-scattered. They play a role in the modeling of provability logic (cf. scattered topos).

Remark

The booleanization $\mathcal{E}_{\neg\neg}$ of a topos $\mathcal{E}$ has a close relative: the De Morganization $\mathcal{E}_m$.

Definition

Definition/Proposition

(double negation topology)

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.

Example

In case of $Set^{\rightrightarrows}$, the presheaf topos of directed graphs, the action of $\neg\neg$ as a closure operator on subgraphs $X\subseteq Y$ amounts to adding to the edge set of $X$ all the edges in $Y$ between vertices that are in $X$. The patient reader will find further details on the $\neg\neg$-topology for this elementary example spelled out at length at Quiv.

Properties

Let $\mathcal{E}$ be a(n elementary) topos.

Definition

The sheaf topos $\mathcal{E}_{\not \not} \hookrightarrow \mathcal{E}$ corresponding to the double negation topology (def. ) is a Boolean topos.

This appears for sheaf toposes $\mathcal{E}$ as MacLane & Moerdijk, theorem VI 3, and in the general case of elementary toposes as a special case of Johnstone, Lem. A4.5.21).

The following says that $\mathcal{E}_{\not \not}$ is the smallest subtopos $\mathcal{E}_j$ such that $\emptyset$ is a $j$-sheaf. This property looks innocent but when thinking of $\mathcal{E}$ as a generalized (topological) space becomes, as in the case of locales, rather remarkable.

Proposition

$\mathcal{E}_{\not \not} \hookrightarrow \mathcal{E}$ is the smallest dense subtopos.

(Johnstone 2002, below Cor. A4.5.20, or Johnstone 1977, p.140)

Another, slightly more general, way to state this is the following (cf. Blass & Scedrov 1983, p.19, Caramello 2012, p.9):

Proposition

A topology $j$ satisfies $j\le\neg\neg$, i.e. $j$ is dense, iff $(\mathcal{E}_j)_{\not\not}=\mathcal{E}_{\not\not}$.

Proposition

$\mathcal{E}_{\not \not} \hookrightarrow \mathcal{E}$ is the largest Boolean subtopos.

This follows from Johnstone 2002, Lemma A4.5.21.

From these two results, we can deduce the following characterization of the double negation topology.

Proposition

$\not\not$ is the unique topology $j$ such that (1) $j$ is dense, i.e. $j(0)=0$, and (2) the sheaf topos $\mathcal{E}_j$ is Boolean.

There are several other characterizations of the double negation topology:

Proposition

$\not \not$ is the smallest topology $j$ on $\mathcal{E}$ such that the canonical mono $(\top,\bot)\, \colon \; 2 \,=\, 1\coprod 1 \, \rightarrowtail\, \Omega$ is $j$-dense.

This is theorem 2.4. in Caramello (2009).

Proposition

$\neg\neg$ is the smallest topology $j$ on $\mathcal{E}$ such that all monomorphisms of the form $A\vee\neg A\rightarrowtail E$ for subobjects $A\rightarrowtail E$ in $\mathcal{E}$ are $j$-dense.

This appears as proposition 6.2 in Caramello (2012a).

As the smallest dense subtopos, $\mathcal{E}_{\not\not}$ becomes important for Lawvere’s calculus of Aufhebung:

Proposition

The smallest essential subtopos $\mathcal{E}_j$ that is dense (in other words the Aufhebung of $0 \dashv 1$) has the property that $\mathcal{E}_{\neg\neg}\le \mathcal{E}_j$ and concides with $\mathcal{E}_{\neg\neg}$ in case the latter is an essential subtopos: $\mathcal{E}_j=\mathcal{E}_{\neg\neg}$ (cf. Lawvere-Menni 2015).¹

For further discussion of this relation see at dense subtopos.

The double negation topology is closely related to the class of skeletal geometric morphims i.e. $f:\mathcal{F}\to\mathcal {E}$ that restrict to a geometric morphism $\mathcal{F}_{\neg\neg}\to\mathcal{E}_{\neg\neg}$ e.g. skeletal geometric morphisms are the 1-cells in 2-category of toposes in which Boolean toposes are co-reflective (cf. Johnstone (2002, p.1008)).

The next propositions consider the important special case of $\neg\neg$ on presheaf toposes:

Proposition

Let $C$ be a small category admitting a right calculus of fractions with respect to the set $\Sigma$ of all morphisms and let $G$ be the free groupoid generated by $C$, i.e. $G\cong C\Sigma^{-1}$. Then the following holds:

$$Sh_{\neg\neg}(Set^{C^{op}})\cong Set^{G^{op}}\quad .$$

This appears as ex.5.2 in Johnstone (1977, p.162). It applies e.g. to $C$ a commutative monoid.

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.

Remark

(relation to forcing)

Essentially because of prop. , double-negation sheaves on posets are the basic context for forcing in set theory (since set theorists generally want the axiom of choice to be preserved in forcing models). For such a use of double negation in the so called Cohen topos see at continuum hypothesis.

Examples

Example

Consider the Sierpinski topos $\mathcal{E} \,\coloneqq\, Set^{\to}$, hence the arrow category of Set.

This has

• exactly two dense subtoposes:

  1. the topos itself

  2. the double-negation topos whose sheaves are the bijections,

• exactly three Boolean subtoposes:

  1. the double-negation subtopos,

  2. the subcategory on the arrows whose codomain is the terminal object,

  3. the degenerate subtopos consisting of just the identity morphism on the terminal object.

Observe that the two non-degenerate Boolean toposes, which complement each other in the lattice of subtoposes, are both equivalent to the topos of sets, which incidentally shows that merely requiring the equivalence $(\mathcal{E}_j)_{\neg\neg}\simeq \mathcal{E}_{\neg\neg}$ in Prop. xy is not sufficient.

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.

Related entries

• law of double negation

• Heyting algebra

• Boolean algebra

• double negation translation

• dense subtopos

• logical topology, synthetic differential topology

• skeletal geometric morphism

• de Morganization

• scattered topos

$\phantom{-}$symbol$\phantom{-}$	$\phantom{-}$in logic$\phantom{-}$
$\phantom{A}$$\in$	$\phantom{A}$element relation
$\phantom{A}$$\,:$	$\phantom{A}$typing relation
$\phantom{A}$$=$	$\phantom{A}$equality
$\phantom{A}$$\vdash$$\phantom{A}$	$\phantom{A}$entailment / sequent$\phantom{A}$
$\phantom{A}$$\top$$\phantom{A}$	$\phantom{A}$true / top$\phantom{A}$
$\phantom{A}$$\bot$$\phantom{A}$	$\phantom{A}$false / bottom$\phantom{A}$
$\phantom{A}$$\Rightarrow$	$\phantom{A}$implication
$\phantom{A}$$\Leftrightarrow$	$\phantom{A}$logical equivalence
$\phantom{A}$$\not$	$\phantom{A}$negation
$\phantom{A}$$\neq$	$\phantom{A}$negation of equality / apartness$\phantom{A}$
$\phantom{A}$$\notin$	$\phantom{A}$negation of element relation $\phantom{A}$
$\phantom{A}$$\not \not$	$\phantom{A}$negation of negation$\phantom{A}$
$\phantom{A}$$\exists$	$\phantom{A}$existential quantification$\phantom{A}$
$\phantom{A}$$\forall$	$\phantom{A}$universal quantification$\phantom{A}$
$\phantom{A}$$\wedge$	$\phantom{A}$logical conjunction
$\phantom{A}$$\vee$	$\phantom{A}$logical disjunction
symbol	in type theory (propositions as types)
$\phantom{A}$$\to$	$\phantom{A}$function type (implication)
$\phantom{A}$$\times$	$\phantom{A}$product type (conjunction)
$\phantom{A}$$+$	$\phantom{A}$sum type (disjunction)
$\phantom{A}$$0$	$\phantom{A}$empty type (false)
$\phantom{A}$$1$	$\phantom{A}$unit type (true)
$\phantom{A}$$=$	$\phantom{A}$identity type (equality)
$\phantom{A}$$\simeq$	$\phantom{A}$equivalence of types (logical equivalence)
$\phantom{A}$$\sum$	$\phantom{A}$dependent sum type (existential quantifier)
$\phantom{A}$$\prod$	$\phantom{A}$dependent product type (universal quantifier)
symbol	in linear logic
$\phantom{A}$$\multimap$$\phantom{A}$	$\phantom{A}$linear implication$\phantom{A}$
$\phantom{A}$$\otimes$$\phantom{A}$	$\phantom{A}$multiplicative conjunction$\phantom{A}$
$\phantom{A}$$\oplus$$\phantom{A}$	$\phantom{A}$additive disjunction$\phantom{A}$
$\phantom{A}$$\&$$\phantom{A}$	$\phantom{A}$additive conjunction$\phantom{A}$
$\phantom{A}$$\invamp$$\phantom{A}$	$\phantom{A}$multiplicative disjunction$\phantom{A}$
$\phantom{A}$$\;!$$\phantom{A}$	$\phantom{A}$exponential conjunction$\phantom{A}$
$\phantom{A}$$\;?$$\phantom{A}$	$\phantom{A}$exponential disjunction$\phantom{A}$

References

Informal exposition of double negation with an eye towards physics is in

• Andrej Bauer, Intuitionistic mathematics for physics, 2008

In topos theory:

• Peter Johnstone, Topos Theory , Academic Press 1977 (Dover reprint 2014). (pp.139-140)

• Peter Johnstone, Sketches of an Elephant vols. I,II, Oxford UP 2002. (pp.211,219-220,1008)

• Saunders Mac Lane, Ieke Moerdijk, Sheaves in Geometry and Logic , Springer Heidelberg 1994. (chap. VI, in particular sec.VI.1)

In homotopy type theory:

• Univalent Foundations Project, section 3.4 of Homotopy Type Theory – Univalent Foundations of Mathematics

Discussion in relation to cohesion and the sharp modality is in

• F. W. Lawvere, Some Thoughts on the Future of Category Theory , pp.1-13 in LNM 1488 Springer Heidelberg 1991.

More detailed discussion of this is in

• William Lawvere, Matías Menni, Internal choice holds in the discrete part of any cohesive topos satisfying stable connected codiscreteness, TAC 30 no. 26 (2015) pp.909-932. (abstract)

• Matías Menni, The unity and identity of opposites between decidable objects and double-negation sheaves , JSL to appear. (preprint)

Other useful references include

• Andreas Blass, Andrej Scedrov, Boolean Classifying Topoi , JPAA 28 (1983) pp.15-30.

• Olivia Caramello, De Morgan classifying toposes , Advances in Mathematics 222 no.6 (2009) pp.2117-2144. (arXiv:0808.1519)

• Olivia Caramello, Universal models and definability , Math. Proc. Cam. Phil. Soc. (2012) pp.279-302. (arXiv:0906.3061)

• Olivia Caramello, Topologies for intermediate logics , arXiv:1205.2547 (2012). (abstract)

• D. S. Mcnab, Some applications of double-negation sheafification , Proc. Edinburgh Math. Soc. 20 (1977) pp.279-285.

---

1. Lawvere (1991) says around p.8: “The base in fact seems in examples to be determined by the given category of Being itself, either as the latter’s QD reflection with the extra localness condition supplying the right adjoint pure Becoming inclusion, or else (for example simplicial sets) as the double-negation sheaves with the extra essentialness condition supplying the left adjoint inclusion (in the latter case it is in Hegelian fashion always the smallest level for which both 0,1 are sheaves)“. ↩