Is (Hausdorff $\implies$ Unique Limits) intuitionistic?

Question

It's well known that in Hausdorff topological spaces, limits of convergent sequences are unique and essentially the only proof I know (which appears very natural) is:

Suppose $(x_i)$ is a convergent sequence with distinct limits $x,y$ in a Hausdorff top. space $(X, \mathcal{T})$. Then there must be disjoint open sets $U,V\in \mathcal{T}$ with $x\in U$ and $y \in V$. But by definition of convergence, the sequence then must eventually lie (and stay) in $U$ and also eventually lie in $V$ and this is a contradiction.

Now notice that this appears to use the law of double-not-reduction or non-intuitionistic logic: if $P$ represents the statement that "Sequences in $X$ have unique limits" then our proof proceeds by assuming $\neg P$ and deducing a contradiction so we obtain $\neg \neg P$, which is classically equivalent to $P$. Notice also that using contradiction in this way seems naively unavoidable as to apply Hausdorffness we must assume $x\not = y$...

Is it possible to prove the uniqueness of limits in Hausdorff spaces intuitionisticly or does this implication not hold in general in non-classical logics?

Answer 1

Some care is needed to properly define a Hausdorff space in a constructive world. A nice definition is: a space $W$ is Hausdorff if and only if $\{(x, y) \in W^2 \mid x = y\}$ is the pseudocomplement of an open set. Equivalently, this condition states that if there are no open sets $U, V$ with $x \in U$, $y \in V$, and $U \cap V = \emptyset$, then $x = y$.

We may strengthen the notion of Hausdorff space in a few ways which are classically trivial, but this is a reasonable starting point. The main strengthening is: define $x \# y$ to mean there are disjoint open neighbourhoods of $x, y$. Then for all $x, y, z$, if $x \# y$, then either $x \# z$ or $y \# z$. But we do not need this additional axiom here.

From here, it’s easy to see that your proof is, in fact, constructive. You showed that if, in fact, we had non-overlapping neighbourhoods of $x$ and $y$, this would lead to a contradiction. Therefore, you’ve shown that $x = y$.