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

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

{-# LANGUAGE TypeFamilies #-}

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?