Could not include topos theory - contents
In logic, double negation is the operation that takes to , where 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 intuitionistic logic, double negation is weaker than the identity. That is, we have 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.
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 has a sublocale given by that nucleus, called the double negation sublocale and denoted . This sublocale is dense, and in fact it is the smallest dense sublocale of , the intersection of all dense sublocales.
Let 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) . Then the pushforward of the pullback of to the smallest dense sublocale of is the sheaf of meromorphic functions on (i.e. sections over an open subset are given by sections of defined on some dense open subset ).
The double negation morphism
constitutes a Lawvere-Tierney topology on .
This is called the double negation topology.
The topology axioms can be formulated in purely equational form, i.e., as equations between operations of the form . By the Yoneda lemma, it suffices to verify the corresponding equations between transformations , which boils the problem down to checking the equations for ordinary Heyting algebras in . For ordinary Heyting algebras, proofs may be found here.
is the smallest dense subtopos.
is the unique largest topology in for which is closed.
For a proof see (Johnstone (1977), p.140).
Both of the preceeding results imply in particular that is always a -sheaf, i.e. is always a dense subtopos. In fact, we have:
It remains to show that (1) and (2) imply that . First note that the dense monos corresponding to are classified by the subobject classifier of . Since (2) implies that is an internal Boolean algebra, it follows that the dense subobjects of any object form a Boolean algebra.
This Boolean algebra is a reflective sub-poset of the Heyting algebra of all subobjects of , whose reflector is lex, i.e. preserves finite meets. Thus, it will suffice to show that if is a Boolean algebra that is a lex-reflective sub-poset of a Heyting algebra and if , then .
To show this, first note that the Boolean negation in is the restriction of the Heyting negation in . Thus, Booleanness of implies for all . Thus, it remains to show that if then . But since and is an exponential ideal, by the definition it follows that for any . Thus, if then as well.
The next two propositions consider the important special case of on presheaf toposes:
This appears as MacLaneMoerdijk, corollary VI 5.
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.)
Classically the double negation modality is equivalent to the n-truncation modality for (the bracket type). In general, it's still true that double negation takes any type (object in the higher topos) to a -type, but the bracket type only entails the double negation :
there is a canonical function
In topos theory:
Peter Johnstone, Topos Theory , Academic Press 1977 (Dover reprint 2014). (pp.139-140)