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.
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.
I have added a sentence mentioning forcing to the Idea-section at double negation,
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.
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.
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.
Maybe it should be “If $L$ is spatial, then $L=L_{\neg\neg}$ if and only if …”?
Yes, spatiality is certainly necessary here.
Corrected reference to Caramello ’09. Added reference to Sketches of an Elephant which removes the need for the ad hoc proof of the subsequent Proposition (moved up) that the double negation subtopos is the unique subtopos which is both dense and Boolean. Rearranged the other propositions and made the Sierpinski topos remark into an example. In my opinion, the page contained insufficient background for the proof to be reader-comprehensible anyway, so pointing to a detailed reference is more useful. Here is the removed proof, in case someone wishes to restore it later: 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.
Have looked at your latest edits, but it’s not easy to see what’s going on. (Am on the last day of a vacation – still just on my phone.)
Probably the paragraph on the Sierpinski topos wants to be in an Example-environment. For that just enclose it inside
\begin{example}
\end{example}
And then not to forget to delete the spurious section header
#### Example
If you still get stuck, I can try to look into it later this week.
Am still not sure what’s going on, hence what was really intended:
The new example (currently still here)
sits in between two propositions which look like they want to be directly subsequent,
refers to “the above” topos which is probably meant to be $\mathcal{E}_{\not \not}$ but remains ambiguous,
refers to a proposition with label “negdense
”, which has not been declared.
I suggest to edit further such as to
either clarify why this example is in the Properties-subsection right after the proposition that currently precedes it,
or else move it to a separate Examples-subsection (to be created, which may have been the original intention) after the Properties-subsection.
So I have moved the example of the Sierpisnki topos out of the Properties-section into a new Examples-section (now here).
In doing so I have replaced the words “the above” with “the double-negation subtopos”, which is probably what was meant (but check).
And the broken reference to a Proposition labeled “negdense
” I have replaced with “Prop. xy”, so that it’s visible that the reference needs fixing and hoping that this makes somebody go and fix it.
1 to 14 of 14