"Boolean algebras are to powersets as complete Heyting algebras are to topologies", or topology from logic (part 3)

In the last post I gave the definition of a Heyting algebra and stated and proved many properties about Heyting algebras and Boolean algebras, a proper subclass of Heyting algebras. Moreover I showed how the implication and negations operations on a Heyting algebra can be interpreted ("proof" and "information" interpretation) as logical operations within a lattice of propositions. We also had the important result that, when considered as spaces alone, frames and complete Heyting algebras are equivalent. In a later post we shall add yet another class of space that is equivalent when considered as a space alone to the former two. Eventually we shall be able to distinguish them, however, when considered in the context of category theory. Specifically we shall see later that they each have different "morphisms".

Let us return to our "lattice of observations" approach to a topology $\Omega X$ on an abstract space $X$ that we began to develop in part 1.  We know that $\Omega X$ is a frame, hence it is also a complete Heyting algebra (cHa).  Now recall for $x \in X$ that $x \in U \in \Omega X \implies x \in \mathscr{N}(x)$. Conversely if $U \in \mathscr{N}(x)$ then $x \in U$, which recall that by $x\in U$, under the lattice of observations interpretation we mean that we have observed (know empirically, have a "proof" that $x \in U$) $x$ to be in the "region" $U$ of the abstract space $X$. So let $y \in U$. Then by definition (different defintion of $\in$ here than is usual) we have a proof that $y \in U$ so $U \in \mathscr{N}(y)$. So $U$ is a (intuitionistic) neighborhood of each of its points, hence $U \in \Omega X$.  (Caution: This is not classically true! It depends entirely of  the particular interpretation of $\in$ I was using. This type of reasoning was used at the end of my second post, however I never mentioned that it forces us to have that neighborhoods are (intuitionistically) open (only due to interpretation!).  Really, as I remarked in a similar paragraph in the second post, I am using a different definition of set containment than is standard in classical logic for the above reasoning. Therefore let us use an alternate symbol for when we mean this type of containment rather than the standard usage so it is no longer necessary to remind the reader for which paragraphs to "suspend disbelief". From now on in the lattice of observations interpretation, for $x \in X$ and $U\subset X$ we shall write \[definition: \qquad x\vdash U \iff  U \in \mathscr{N}(x)\] and say $x$ inhabits $U$ when we mean this type of membership. Note that by definition $x$ can only inhabit a neighborhood. So this definition depends entirely on $\Omega X$. To emphasize this dependence on $\Omega X$ we may write $\vdash_{\Omega}$. For instance if one were speaking of another topology $\Gamma X$ on $X$ distinct from $\Omega X$ then distinction must be made between $\vdash _{\Omega}$ and $\vdash_{\Gamma}$.
We have not yet considered $\vdash_{\mathscr{P}}$ where $\mathscr{P}(X)$ is the classical lattice of observations. Well if $A \subset X$ and $x \in A$ then $x\ \in A \in \mathscr{P}(x)$. So $A$ is a n-hood of $x$ (relative to $\mathscr{P}(X)$. Hence $x \vdash_{\mathscr{P}} A$. Therefore $\in$ = $\mathscr{P}$. So when we deviate from the classical lattice of observations we also deviate from classical inclusion if we keep the internalized logic of the lattice.
Now we can see in the claim earlier than neighborhoods are forced to be open, what was really meant using our new notation is that neighborhoods are open in the internal logic of $\Omega$ because the classical
 \[U \in \Omega X \iff \{\forall x \in U\:[\:x\vdash_\Omega U]\}\]
becomes a trivial statement when we replace $\in$ with $\vdash_{\Omega}$ (that is n-hoods are open under $\vdash$ (internal logic of $\Omega$ but not necessarily under $\in$). On the other hand $x \vdash U$ can also have the interpretation $x$ is known empirically to be in $U$ (a type of metalogic) and can be used to recover $\mathscr{N}(x)$ for each $x \in X$. In this latter sense only topologies "coarser" than $\Omega X$ ($\Gamma X \subset \Omega X$) may be produced.
Now that we have two concepts of membership we get two distinct concepts of set inclusion: the standard one induced by $\in$ and a now one induced by $\vdash$. For the latter we shall define
\[definition: \qquad \forall A, B \in \Omega X \:[\:A\sqsubset B \iff  \{\forall x\in X \:[\:x\vdash A \implies x\vdash B]\}]\] and sometimes write $A \sqsubset_{\Omega} B$ to show dependence on $\Omega X$.

Now $\Omega X$ is a cHa. Let us examine implication and negation in this case. Recall from part 1 that the  partial order on $\Omega X$ is subset inclusion $\subset$ and that we have \[\forall \alpha \subset \Omega X \:[\bigvee \alpha = \bigcup \alpha \: \: \&\:\: \bigwedge \alpha = (\bigcap \alpha)^{\circ}]\]
So arbitrary joins are unions but in general arbitrary meets are equal to the interior of the intersection. Since $\Omega X$ is a topology, the condition that $\Omega X$ is closed under finite intersections translates to finite meets are the same as finite intersections.

Note that if we have $A, B \in \Omega X$ and $A \subset B$ then we may consider the proposition $x \vdash A$. Then we also have $x \vdash B$ because $\mathscr{N}(x)$ is a filter. So any observation that can be made in $A$ can also be made in $B$. This follows the "proof interpretation" model that I mentioned in the last post because a proof of $x$ being contained in $A$ is $x \vdash A$ which implies that we have a proof of $x$ being contained in $B$ or $x\vdash B$.

Let's see what $A \rightarrow B$ looks like for $A, B \in \Omega X$. Since $\Omega X$ is complete, we must have $A \rightarrow B = \bigvee\{C \in\Omega X \: | \:A \wedge C \leq B\} = \bigcup \{ C\in \Omega X \:|\:A \cap C \subset B\}$. Then $\sim A =A \rightarrow \emptyset = \bigcup \{C\in \Omega X\:|\:A \cap C = \emptyset\} = \bigcup \{C\in \Omega X\:|\: C \subset A^c\} = (A^c)^{\circ}$. So the negation of $A$ is the interior of its complement. But from property (5) from the last post we know that a Heyting algebra is boolean $\iff \sim \sim a = a$ for each $a \in L$. So $\Omega X$ is boolean  $\iff \forall A \in \Omega X \:[\sim \sim A = ((A^c)^{{\circ}})^c)^{\circ}=A]$.

Let's try to simplify $\sim \sim A = ((A^c)^{{\circ}})^c)^{\circ}$ using that $(A^c)^{{\circ}} = (\bar{A})^c$. Plugging this in we get $\sim \sim A = (((\bar{A})^c)^c)^{\circ} = (\bar{A})^{\circ}$. Hence $\sim \sim A$ is the interior of the closure of $A$. So we have that a topology is Boolean $\iff$ for all $A \in \Omega X$ we have that $(\bar{A})^{\circ} = A$. In general topology open sets $A$ that satisfy the condition $(\bar{A})^{\circ} = A$ are called normal open sets. So for our characterization an open set $A$ is normal when $\sim \sim A = A$ and a topology is Boolean $\iff$ every open set is normal.

Therefore we now have a multitude of examples of Heyting algebras that are not Boolean. Take any topology $\Omega X$ on $X$ that is not closed under complementation. Then it will be Heyting but not Boolean. This is because if $A \in \Omega X$ but $A^c \notin \Omega X$ then $\sim A \subsetneq A^c$. So $A \vee \sim A = A \cup \sim A \subsetneq A \cup A^c = X$. So $\sim A$ is not the Boolean negation of $A$. So $\Omega X$ is not Boolean. The proceeding argument also shows that if we have that $\Omega X$ is not Boolean then excluded middle does not hold internally on $\Omega X$. To see this note that if $\Omega X$ is not Boolean then $\exists A \in \Omega X \:[A^c \notin \Omega X]$.  Then apply the proceeding argument to show that $\sim A \cup A \neq X$ which shows excluded middle does not hold internally.

For an example take $\mathbb{R}$ with its standard topology. Then it clearly is not Boolean because $\sim (0, 1) = (\infty,0) \cup (1,\infty) \neq (0,1)^c$. So that means there must exist open sets that are not normal. Let's try to find one. $(0, 1)$ is normal because $\sim ((\infty,0) \cup (1,\infty))= (0, 1)$. Let's try $(0, \frac{1}{2}) \cup (\frac{1}{2}, 1)$. Well $\sim ((0, \frac{1}{2}) \cup (\frac{1}{2}, 1)) = (\infty,0) \cup (1,\infty)$ and $\sim ((\infty,0) \cup (1,\infty) = (0,1) \neq  (0, \frac{1}{2}) \cup (\frac{1}{2}, 1)$. So $(0, \frac{1}{2}) \cup (\frac{1}{2}, 1)$ is an open set that is not normal.