Add spatiality condition to the characterization of $L=L_{\neg\neg}$.

]]>Yes, spatiality is certainly necessary here.

]]>Maybe it should be “If $L$ is spatial, then $L=L_{\neg\neg}$ if and only if …”?

]]>Yes, it seems that statement had been there since Day 1. I suspect Toby was thinking along roughly the following lines: a topological space $X$ in which every open is regular open is (classically) discrete. If you allow the luxury of $T_1$ spaces, and if $x$ is any non-isolated point, then its set-theoretic complement $U$ has $U \cup \{x\} = X$ as its closure, so $\neg \neg U = X$. So maybe with a sufficiently generous interpretation of “classical”, the statement is defensible – but I agree the statement is confusing as it stands.

]]>The article claims

```
Classically, we have L=L¬¬ if and only if L is the discrete locale on some set S of points. In constructive mathematics, S must also have decidable equality.
```

But any complete Boolean algebra is a frame for which the corresponding locale satisfies L=L_¬¬ because ¬¬=id. There are plenty of nonatomic complete Boolean algebras.

]]>That is a nice post, but I have to take issue with

classical logic is happy with

lack of negative evidence.

I would say that what classical logic is happy with is the *impossibility* of negative evidence, which is rather stronger than the present lack thereof.

I have added a sentence mentioning *forcing* to the Idea-section at *double negation*,

I have added to the References at *double negation* pointer to Andrej’s exposition:

which is really good. I have also added this to *double negation transformation*, but clearly that entry needs some real references, too.