Can someone provide a proof or counterexample to the following conjecture?
Conjecture: if $X$ is a topological space such that every open set $U \subseteq X$ satisfies $\mathrm{int}( \mathrm{c\ell}(U)) = U$, then every open set is closed (i.e. clopen).
Context: for any topological space $X$, its lattice of open sets forms a "model" of intuitionistic propositional logic. We interpret propositions as open sets $U$, $\land$ as intersection, $\lor$ as union, $\varnothing$ as $\bot$ and $X$ as $\top$. Implication is defined $U \to V = \mathrm{int}( U^\complement \cup V)$ – see this nLab article – and negation is defined $\lnot U = U \to \bot = \mathrm{ext}(U)$.
It is known that, over intuitionistic logic, the law of excluded middle $P \lor \lnot P$ and double negation elimination $\lnot \lnot P \to P$ are equivalent. Saying $U \cup \lnot U = X$ for an open set $U \subseteq X$ is equivalent to saying $U$ is closed (clopen). Meanwhile, saying that $\lnot \lnot U = U$ is equivalent to saying $\mathrm{int}( \mathrm{c\ell}(U)) = U$.
Thus, I was trying to prove the equivalence of $\mathsf{LEM}$ and $\mathsf{DNE}$ using this topological interpretation. The forward direction is easy enough, but I couldn't prove the reverse easily, which is the conjecture above.
Best Answer
As mentioned in my comment above, it is perhaps worth posting here a very succinct argument which establishes the OP's conjecture.
Proof. For every $x \in X$ let us write $Z_x=\mathring{\overline{\{x\}}} \in \mathscr{T}$. By dualising via complementation the given hypothesis of regularity -- according to which $\mathring{\overline{U}}=U$ for any open subset $U \in \mathscr{T}$ -- we gather that $\overline{\mathring{F}}=F$ for any closed subset $F \subseteq X$. Applying this to the particular case of the closed subset $\overline{\{x\}}$ we infer that $\overline{Z_x}=\overline{\{x\}}$.
In order to proceed with this argument it is also essential that we establish the nontrivial relation $x \in Z_x$. This we achieve by considering an arbitrary point $x \in X$ and assuming the contrary, $x \in X \setminus Z_x$. For ease of notation let us write $\overset{\smile}{M}\colon=X \setminus \overline{M}=\left(X \setminus M\right)^{\circ}$ for the exterior of arbitrary subset $M \subseteq X$. Our assumption then means that $x \in X \setminus Z_x=\overline{\left(X \setminus \{x\}\right)^{\circ}}=\overline{\overset{\smile}{\{x\}}}$, whence we infer that $\overline{\overset{\smile}{\{x\}}} \supseteq \overset{\smile}{\{x\}} \cup \{x\}$. Since it is in general (in any topological space) true that $\overline{M \cup \overset{\smile}{M}}=X$ for any subset $M \subseteq X$, we gather in particular that $\overline{\overset{\smile}{\{x\}}}\supseteq \overline{\overset{\smile}{\{x\}} \cup \{x\}}=X$, which simply means that $\overline{\overset{\smile}{\{x\}}}=X$. We now apply the hypothesis of regularity by considering interiors in this last relation in order to obtain $X=\mathring{\overline{\overset{\smile}{\{x\}}}}=\overset{\smile}{\{x\}}$. This is an obvious contradiction as $\overset{\smile}{\{x\}} \subseteq X \setminus \{x\} \subset X$ (where $\subset$ denotes strict inclusion). In other words, it is in general true that exteriors of nonempty subsets are proper subsets and that under our particular assumption of regularity the adherence of a proper open subset must remain a proper subset.
Considering now an arbitrary closed subset $F \subseteq X$ and an arbitrary point $x \in F$ we clearly have $\overline{\{x\}} \subseteq F$. This however leads to $Z_x \subseteq \overline{Z_x}=\overline{\{x\}} \subseteq F$ and as $x \in Z_x \in \mathscr{T}$ the point $x$ is established to be an interior point of $F$. By virtue of the arbitrariness of $x$ this entails $F \subseteq \mathring{F}$, which means that $F=\mathring{F}$ and hence any closed subset is equally open. The topology is thus seen to consist of clopen subsets. $\Box$