Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Created double-negation shift, with a proof that it is equivalent to double-negated excluded middle.
If I’m not mistaken, this principle holds in the topos of sheaves on a space (or locale) $X$ iff $X$ contains a dense locally decidable open, i.e. a dense open set $U\in O(X)$ such that for all $V\subseteq U$ we have $U\subseteq V\cup\neg V$. An example is the Sierpinski space, a counterexample is the real line. (the negation is the closure of the complement)
I suppose at least in the spatial case the local decidability is equivalent to discreteness, so the condition means that $X$ has a dense and discrete open subspace.
An example satisfying T_2 is the 1-point compacitification of an infinite set.
If you’d like to add this to the page with a proof, feel free!
Did it, at least with proof outlines. I hope I didn’t make any mistakes!
Thanks!
1 to 7 of 7