DNS holds in every Kripke model with finite frame.
]]>Thanks!
]]>Did it, at least with proof outlines. I hope I didn’t make any mistakes!
]]>If you’d like to add this to the page with a proof, feel free!
]]>I suppose at least in the spatial case the local decidability is equivalent to discreteness, so the condition means that has a dense and discrete open subspace.
An example satisfying T_2 is the 1-point compacitification of an infinite set.
]]>If I’m not mistaken, this principle holds in the topos of sheaves on a space (or locale) iff contains a dense locally decidable open, i.e. a dense open set such that for all we have . An example is the Sierpinski space, a counterexample is the real line. (the negation is the closure of the complement)
]]>Created double-negation shift, with a proof that it is equivalent to double-negated excluded middle.
]]>