nLab
double negation

Context

Topos Theory

Could not include topos theory - contents

Double negation

Idea

In logic, double negation is the operation that takes PP to ¬¬P\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¬¬PP \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 LL has a sublocale given by that nucleus, called the double negation sublocale and denoted L ¬¬L_{\neg\neg}. This sublocale is dense, and in fact it is the smallest dense sublocale of LL, the intersection of all dense sublocales.

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

Example

Let 𝒪 X\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) XX. Then the pushforward of the pullback of 𝒪 X\mathcal{O}_X to the smallest dense sublocale of XX is the sheaf of meromorphic functions on XX (i.e. sections over an open subset UU are given by sections of 𝒪 X\mathcal{O}_X defined on some dense open subset VUV \subseteq U).

In topos theory

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

If EE 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 Ω nΩ\Omega^n \to \Omega. By the Yoneda lemma, it suffices to verify the corresponding equations between transformations Hom(,Ω) nHom(,Ω)Hom(-, \Omega)^n \to Hom(-, \Omega), which boils the problem down to checking the equations for ordinary Heyting algebras in SetSet. For ordinary Heyting algebras, proofs may be found here.

Properties

Proposition

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

This appears for sheaf toposes as (MacLaneMoerdijk, theorem VI 3), and in the general case as a special case of (Johnstone, Lemma A4.5.21).

Proposition

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

(Johnstone, below Corollary A4.5.20)

Proposition

¬¬\not\not is the unique largest topology in \mathcal{E} for which 010\rightarrowtail 1 is closed.

For a proof see (Johnstone (1977), p.140).

Both of the preceding results imply in particular that 00 is always a ¬¬\not\not-sheaf, i.e. ¬¬\mathcal{E}_{\not\not} is always a dense subtopos. In fact, we have:

Proposition

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

Proof

It remains to show that (1) and (2) imply that j=¬¬j=\not\not. First note that the dense monos corresponding to jj are classified by the subobject classifier Ω j\Omega_j of j\mathcal{E}_j. Since (2) implies that Ω j\Omega_j is an internal Boolean algebra, it follows that the dense subobjects of any object XX form a Boolean algebra.

This Boolean algebra is a reflective sub-poset of the Heyting algebra of all subobjects of XX, whose reflector is lex, i.e. preserves finite meets. Thus, it will suffice to show that if BB is a Boolean algebra that is a lex-reflective sub-poset of a Heyting algebra HH and if 0B0\in B, then B={U|U=¬¬U}B = \{ U | U = \neg\neg U \}.

To show this, first note that the Boolean negation in BB is the restriction of the Heyting negation in HH. Thus, Booleanness of BB implies U=¬¬UU=\neg\neg U for all UBU\in B. Thus, it remains to show that if U=¬¬UU=\neg\neg U then UBU\in B. But since 0B0\in B and BB is an exponential ideal, by the definition ¬U=(U0)\neg U = (U\Rightarrow 0) it follows that ¬¬UB\neg\neg U\in B for any UU. Thus, if U=¬¬UU=\neg\neg U then UBU\in B as well.

Proposition

As the Aufhebung j\mathcal{E}_j of 010 \dashv 1 (a sharp modality satisfying 00\sharp 0 \simeq 0) is necessarily dense it follows that ¬¬ j\mathcal{E}_{\neg\neg}\subseteq \mathcal{E}_j in general and ¬¬= j\mathcal{E}_{\neg\neg}=\mathcal{E}_j in case the former is an essential subtopos (Lawvere 91, p. 8, for further details cf. Aufhebung).

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

Proposition

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

This appears as MacLaneMoerdijk, corollary VI 5.

Proposition

Let CC be a poset. Then the double negation sheaf topos Sh ¬¬(C)[C op,Set] Sh_{\not \not}(C) \hookrightarrow [C^{op}, Set] satisfies the axiom of choice.

This appears as MacLaneMoerdijk, corollary VI 9. Essentially because of this fact, 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.)

In higher topos theory

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

there is a canonical function

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

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

References

In topos theory:

In homotopy type theory:

Discussion in relation to cohesion and the sharp modality is in

which has 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).

Here the “Hegelian fashion” refers to what is discussed in detail at Aufhebung.

Revised on June 16, 2015 09:17:43 by Todd Trimble (67.81.95.215)