\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{double negation} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{topos_theory}{}\paragraph*{{Topos Theory}}\label{topos_theory} [[!include topos theory - contents]] \hypertarget{double_negation}{}\section*{{Double negation}}\label{double_negation} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{in_logic}{In logic}\dotfill \pageref*{in_logic} \linebreak \noindent\hyperlink{double_negation_locale}{In locale theory}\dotfill \pageref*{double_negation_locale} \linebreak \noindent\hyperlink{topology}{In topos theory}\dotfill \pageref*{topology} \linebreak \noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak \noindent\hyperlink{example_2}{Example}\dotfill \pageref*{example_2} \linebreak \noindent\hyperlink{Properties}{Properties}\dotfill \pageref*{Properties} \linebreak \noindent\hyperlink{remarks}{Remarks}\dotfill \pageref*{remarks} \linebreak \noindent\hyperlink{InHigherToposTheory}{In higher topos theory}\dotfill \pageref*{InHigherToposTheory} \linebreak \noindent\hyperlink{related_entries}{Related entries}\dotfill \pageref*{related_entries} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{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 \emph{[[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 \emph{double negation topology} closes morphisms under double negation (def. \ref{DoubleNegationTopology} below), and its [[category of sheaves]] forms a [[boolean topos]] (prop. \ref{DoubleNegationSheavesFormBooleanTopos} below). This notably serves to capture the \emph{[[forcing]]} of [[set theory]] in terms of [[topos theory]] ([[classifying topoi]]), see also remark \ref{RelationToForcing} below. \hypertarget{in_logic}{}\subsection*{{In logic}}\label{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. \hypertarget{double_negation_locale}{}\subsection*{{In locale theory}}\label{double_negation_locale} 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 \textbf{double negation sublocale} and denoted $L_{\neg\neg}$. This sublocale is [[dense sublocale|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]]. \begin{example} \label{}\hypertarget{}{} Let $\mathcal{O}_X$ be the sheaf of [[continuous map|continuous]] (or [[smooth map|smooth]], or [[holomorphic map|holomorphic]], or [[regular map|regular]]) functions on a [[topological space]] (or [[smooth manifold]], or [[complex manifold]], or [[reduced scheme]]) $X$. Then the [[direct image|pushforward]] of the [[inverse image|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$). \end{example} \hypertarget{topology}{}\subsection*{{In topos theory}}\label{topology} The notion of double negation sublocale may be [[categorification|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 [[internalisation|internal]] [[Heyting algebra]]. \hypertarget{definition}{}\subsubsection*{{Definition}}\label{definition} \begin{defn} \label{DoubleNegationTopology}\hypertarget{DoubleNegationTopology}{} \textbf{(double negation topology)} The double negation morphism \begin{displaymath} \not \not \colon \Omega \to \Omega \end{displaymath} constitutes a [[Lawvere-Tierney topology]] on $\mathcal{E}$. This is called the \textbf{double negation topology}. \end{defn} \begin{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 \href{Heyting+algebra#ToBooleanAlgebras}{here}. \end{proof} \hypertarget{example_2}{}\subsubsection*{{Example}}\label{example_2} \begin{itemize}% \item 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]]. \end{itemize} \hypertarget{Properties}{}\subsubsection*{{Properties}}\label{Properties} \begin{prop} \label{DoubleNegationSheavesFormBooleanTopos}\hypertarget{DoubleNegationSheavesFormBooleanTopos}{} The sheaf topos $\mathcal{E}_{\not \not} \hookrightarrow \mathcal{E}$ corresponding to the \hyperlink{DoubleNegationTopology}{double negation topology} (def. \ref{DoubleNegationTopology}) is a [[Boolean topos]]. \end{prop} This appears for [[sheaf toposes]] $\mathcal{E}$ as (\hyperlink{MacLaneMoerdijk}{MacLane-Moerdijk, theorem VI 3}), and in the general case ([[elementary toposes]]) as a special case of (\hyperlink{Johnstone}{Johnstone, Lemma 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. \begin{prop} \label{smallest_dense_subtopos}\hypertarget{smallest_dense_subtopos}{} $\mathcal{E}_{\not \not} \hookrightarrow \mathcal{E}$ is the smallest [[dense subtopos]]. \end{prop} (\hyperlink{Johnstone}{Johnstone 2002, below Corollary A4.5.20}, or \hyperlink{Johnstone77}{Johnstone 1977}, p.140) \begin{prop} \label{smallest_j-dense}\hypertarget{smallest_j-dense}{} $\not \not$ is the smallest topology $j$ on $\mathcal{E}$ such that the canonical mono $(\top,\bot):2=1\coprod 1\rightarrowtail\Omega$ is $j$-dense. \end{prop} This is theorem 1.4. in \hyperlink{Caramello09}{Caramello (2009)}. \begin{prop} \label{Boolean_mono}\hypertarget{Boolean_mono}{} $\neg\neg$ is the smallest [[Lawvere-Tierney topology|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. \end{prop} This appears as proposition 6.2 in \hyperlink{Caramello12a}{Caramello (2012a)}. From the above we have that $\mathcal{E}_{\not\not}$ is a [[Boolean topos|Boolean]] and [[dense subtopos]]. In fact, even better, we have \begin{prop} \label{boolean_subtopos}\hypertarget{boolean_subtopos}{} $\not\not$ is the unique topology $j$ such that (1) $j$ is [[dense subtopos|dense]], i.e. $j(0)=0$, and (2) the sheaf topos $\mathcal{E}_j$ is [[Boolean topos|Boolean]]. \end{prop} \begin{proof} It remains to show that (1) and (2) imply that $j=\not\not$. First note that the dense monos corresponding to $j$ are classified by the subobject classifier $\Omega_j$ of $\mathcal{E}_j$. Since (2) implies that $\Omega_j$ is an internal [[Boolean algebra]], it follows that the dense subobjects of any object $X$ form a Boolean algebra. This Boolean algebra is a reflective sub-poset of the [[Heyting algebra]] of all subobjects of $X$, whose reflector is lex, i.e. preserves finite [[meets]]. Thus, it will suffice to show that if $B$ is a Boolean algebra that is a lex-reflective sub-poset of a Heyting algebra $H$ and if $0\in B$, then $B = \{ U | U = \neg\neg U \}$. To show this, first note that the Boolean negation in $B$ is the restriction of the Heyting negation in $H$. Thus, Booleanness of $B$ implies $U=\neg\neg U$ for all $U\in B$. Thus, it remains to show that if $U=\neg\neg U$ then $U\in B$. But since $0\in B$ and $B$ is an [[exponential ideal]], by the definition $\neg U = (U\Rightarrow 0)$ it follows that $\neg\neg U\in B$ for any $U$. Thus, if $U=\neg\neg U$ then $U\in B$ as well. \end{proof} Another, slightly more general, way to state this is is the following (cf. \hyperlink{BlassScedrov83}{Blass-Scedrov 1983}, p.19, \hyperlink{Caramello12}{Caramello 2012}, p.9): \begin{prop} \label{}\hypertarget{}{} Let $\mathcal{E}$ be a topos. A topology $j$ satisfies $j\le\neg\neg$, i.e. $j$ is [[dense subtopos|dense]], iff $(\mathcal{E}_j)_{\not\not}=\mathcal{E}_{\not\not}$. \end{prop} Notice that, though these results prevent a topos from having more than one \emph{dense} Boolean subtopos, nothing prevents a topos from having more than one \emph{Boolean} subtopos e.g. the [[Sierpinski topos]] $Set^{\to}$ has two non trivial ones that complement each other in the [[lattice of subtoposes]]. This example, incidentally, also shows that in the \hyperlink{negdense}{above proposition} just $(\mathcal{E}_j)_{\neg\neg}\cong\mathcal{E}_{\neg\neg}$ wouldn't do. As the smallest dense subtopos, $\mathcal{E}_{\not\not}$ becomes important for Lawvere's calculus of [[Aufhebung]]: \begin{prop} \label{RelationToAufhebungof01}\hypertarget{RelationToAufhebungof01}{} The smallest \emph{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 geometric morphism|essential]] subtopos: $\mathcal{E}_j=\mathcal{E}_{\neg\neg}$ (cf. \hyperlink{LawvereMenni15}{Lawvere-Menni 2015}).\footnote{\hyperlink{Lawvere91}{Lawvere (1991)} says around p.8: ``\emph{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 [[Aufhebung|Hegelian fashion]] always the smallest level for which both 0,1 are sheaves)``}.} \end{prop} For further discussion of this relation see at [[dense subtopos]]. The double negation topology is closely related to the class of [[skeletal geometric morphism|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 topos|presheaf toposes]]: \begin{prop} \label{}\hypertarget{}{} Let $C$ be a small category admitting a [[calculus of fractions|right calculus of fractions]] with respect to the set $\Sigma$ of \emph{all} morphisms and let $G$ be the free groupoid generated by $C$, i.e. $G\cong C\Sigma^{-1}$. Then the following holds: \begin{displaymath} Sh_{\neg\neg}(Set^{C^{op}})\cong Set^{G^{op}}\quad . \end{displaymath} \end{prop} This appears as ex.5.2 in \hyperlink{Johnstone77}{Johnstone (1977, p.162)}. It applies e.g. to $C$ a commutative monoid. \begin{prop} \label{}\hypertarget{}{} For every [[presheaf topos]] $[C^{op}, Set]$ the double negation topology coincides with the [[dense topology]]. \end{prop} This appears as \hyperlink{MacLaneMoerdijk}{MacLaneMoerdijk, corollary VI 5}. \begin{prop} \label{DoubleNegationSheavesSatisfyAxiomOfChoice}\hypertarget{DoubleNegationSheavesSatisfyAxiomOfChoice}{} Let $C$ be a [[poset]]. Then the double negation sheaf topos $Sh_{\not \not}(C) \hookrightarrow [C^{op}, Set]$ satisfies the [[axiom of choice]]. \end{prop} This appears as \hyperlink{MacLaneMoerdijk}{MacLaneMoerdijk, corollary VI 9}. \begin{remark} \label{RelationToForcing}\hypertarget{RelationToForcing}{} \textbf{(relation to [[forcing]])} Essentially because of prop. \ref{DoubleNegationSheavesSatisfyAxiomOfChoice}, double-negation sheaves on posets are the basic context for \emph{[[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 \textbf{Cohen topos} see at \emph{[[continuum hypothesis]]}. \end{remark} \hypertarget{remarks}{}\subsubsection*{{Remarks}}\label{remarks} \begin{itemize}% \item A topos $\mathcal{E}$ such that $\mathcal{E}_{\neg\neg}$ is an [[open subtopos]] is called \emph{$\bot$-scattered}. They play a role in the modeling of [[provability logic]] (cf. [[scattered topos]]). \item The booleanization $\mathcal{E}_{\neg\neg}$ of a topos $\mathcal{E}$ has a close relative: the [[De Morganization]] $\mathcal{E}_m$. \end{itemize} \hypertarget{InHigherToposTheory}{}\subsection*{{In higher topos theory}}\label{InHigherToposTheory} [[classical logic|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]] \begin{displaymath} {\|A\|_{-1}} \longrightarrow \neg(\neg{A}) \end{displaymath} and this is a [[1-epimorphism]] precisely if the [[law of excluded middle]] holds. \hypertarget{related_entries}{}\subsection*{{Related entries}}\label{related_entries} \begin{itemize}% \item [[law of double negation]] \item [[Heyting algebra]] \item [[Boolean algebra]] \item [[double negation translation]] \item [[dense subtopos]] \item [[logical topology]], [[synthetic differential topology]] \item [[skeletal geometric morphism]] \item [[de Morganization]] \item [[scattered topos]] \end{itemize} [[!include logic symbols -- table]] \hypertarget{references}{}\subsection*{{References}}\label{references} Informal exposition of double negation with an eye towards [[physics]] is in \begin{itemize}% \item [[Andrej Bauer]], \emph{\href{http://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/}{Intuitionistic mathematics for physics}}, 2008 \end{itemize} In [[topos theory]]: \begin{itemize}% \item [[Peter Johnstone]], \emph{Topos Theory} , Academic Press 1977 (Dover reprint 2014). (pp.139-140) \item [[Peter Johnstone]], \emph{[[Sketches of an Elephant]] vols. I,II}, Oxford UP 2002. (pp.211,219-220,1008) \item [[Saunders Mac Lane]], [[Ieke Moerdijk]], \emph{[[Sheaves in Geometry and Logic]]} , Springer Heidelberg 1994. (chap. VI, in particular sec.VI.1) \end{itemize} In [[homotopy type theory]]: \begin{itemize}% \item [[Univalent Foundations Project]], section 3.4 of \emph{[[Homotopy Type Theory -- Univalent Foundations of Mathematics]]} \end{itemize} Discussion in relation to [[cohesion]] and the [[sharp modality]] is in \begin{itemize}% \item [[F. W. Lawvere]], \emph{[[Some Thoughts on the Future of Category Theory]]} , pp.1-13 in LNM \textbf{1488} Springer Heidelberg 1991. \end{itemize} More detailed discussion of this is in \begin{itemize}% \item [[William Lawvere]], [[Matías Menni]], \emph{Internal choice holds in the discrete part of any cohesive topos satisfying stable connected codiscreteness}, TAC \textbf{30} no. 26 (2015) pp.909-932. (\href{http://www.tac.mta.ca/tac/volumes/30/26/30-26abs.html}{abstract}) \item [[Matías Menni]], \emph{The unity and identity of opposites between decidable objects and double-negation sheaves} , JSL to appear. (\href{https://drive.google.com/file/d/18P2qsihtZG7_eCT5VdjvQ1I7T-U_S7y9/view}{preprint}) \end{itemize} Other useful references include \begin{itemize}% \item [[Andreas Blass]], Andrej Scedrov, \emph{Boolean Classifying Topoi} , JPAA \textbf{28} (1983) pp.15-30. \item [[Olivia Caramello]], \emph{De Morgan classifying toposes} , Advances in Mathematics \textbf{222} no.6 (2009) pp.2117-2144. (\href{http://arxiv.org/abs/0808.1519}{arXiv:0808.1519}) \item [[Olivia Caramello]], \emph{Universal models and definability} , Math. Proc. Cam. Phil. Soc. (2012) pp.279-302. (\href{http://arxiv.org/abs/0906.3061}{arXiv:0906.3061}) \item [[Olivia Caramello]], \emph{Topologies for intermediate logics} , arXiv:1205.2547 (2012). (\href{http://arxiv.org/abs/1205.2547}{abstract}) \item D. S. Mcnab, \emph{Some applications of double-negation sheafification} , Proc. Edinburgh Math. Soc. \textbf{20} (1977) pp.279-285. \end{itemize} [[!redirects double negation]] [[!redirects double negations]] [[!redirects double-negation]] [[!redirects not not]] [[!redirects not-not]] [[!redirects double negation sublocale]] [[!redirects double negation sublocales]] [[!redirects double-negation sublocale]] [[!redirects double-negation sublocales]] [[!redirects double negation nucleus]] [[!redirects double negation nuclei]] [[!redirects double-negation nucleus]] [[!redirects double-negation nuclei]] [[!redirects double negation topology]] [[!redirects double negation topologies]] [[!redirects double-negation topology]] [[!redirects double-negation topologies]] [[!redirects double negation modality]] [[!redirects double negation modalities]] [[!redirects double negation monad]] [[!redirects double negation monads]] \end{document}