If a computer can demonstrate singleton sets are closed, is the space Hausdorff?

Question

In Haskell, I made a class of admissible (that is, second-countable and $T_0$) spaces:

{-# LANGUAGE TypeFamilies #-}

class Admissible a where
    type BasisElem a -- Type of a basis element
    semidecide :: a -> BasisElem a -> [Bool] -- Semidecides whether an element is in a basis element
    countFirst :: a -> [BasisElem a] -- Computes a countable basis at an element
    countSecond :: a -> [BasisElem a] -- Computes a countable basis (the parameter is dummy)
    countDense :: [a] -- Computes a countable dense subset

semidecide outputs a list having a True if and only if the element is in the basis element. Generally, it is not a decider; the output may be an infinite list of Falses.

I tried to make a class of Fréchet ($T_1$) spaces and a class of Hausdorff ($T_2$) spaces. The sketch was:

class Admissible a => Frechet a where
    frechet :: a -> [BasisElem a]

class Frechet a => Hausdorff a where
    hausdorff :: a -> a -> [Bool]

frechet outputs the open set whose complement is the singleton set of given element.

hausdorff semidecides the inequality $≠$.

But apparently, if frechet is present, hausdorff is redundant? Like this:

weaveOmegaSq :: [[a]] -> [a]
weaveOmegaSq = go 1
  where
    go n xss = let
        partitioned = do
            (us, vs) <- fmap (splitAt n) xss
            [us, vs]
        in case partitioned of
            [] -> []
            xs:yss -> xs ++ go (1 + n) (go2 yss)
    go2 [] = []
    go2 [xs] = [xs]
    go2 (xs:ys:xss) = (ys ++ xs) : go2 xss

hausdorff x y = weaveOmegaSq (fmap (semidecide x) (frechet y))

weaveOmegaSq is a bijection from the ordinal $\omega^2$ to $\omega$.

Does this mean, if a computer can demonstrate singleton sets are closed, the space is Hausdorff? What's the rigorous proof?

Answer 1

Indeed, having your map frechet available and having your map hausdorff available is equivalent. You can find this in my article Topological aspects of the theory of represented spaces (arXiv). The proof is a very straight-forward currying/uncurrying affair.

If you are only working with second-countable spaces, this is essentially the end of the story. But beyond them, it gets a bit tricky because there the semidecidability of inequality no longer implies the topological characterization of Hausdorffness, namely that there are disjoint open sets separating the points. Matthias Schröder has found a few examples, eg the one-point compactification of the Baire space has semidecidable inequality, but the point at infinity is not separated from the others by any pair of disjoint open sets.