# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorMike Shulman
• CommentTimeDec 30th 2017

Created double-negation shift, with a proof that it is equivalent to double-negated excluded middle.

• CommentRowNumber2.
• CommentAuthorJonasFrey
• CommentTimeDec 31st 2017
• (edited Dec 31st 2017)

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)

• CommentRowNumber3.
• CommentAuthorJonasFrey
• CommentTimeDec 31st 2017
• (edited Dec 31st 2017)

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.

• CommentRowNumber4.
• CommentAuthorMike Shulman
• CommentTimeDec 31st 2017

If you’d like to add this to the page with a proof, feel free!

• CommentRowNumber5.
• CommentAuthorJonasFrey
• CommentTimeJan 1st 2018

Did it, at least with proof outlines. I hope I didn’t make any mistakes!

• CommentRowNumber6.
• CommentAuthorMike Shulman
• CommentTimeJan 2nd 2018

Thanks!

• CommentRowNumber7.
• CommentAuthorspitters
• CommentTimeJul 17th 2018

DNS holds in every Kripke model with finite frame.