Is compact metric space separable in ZF?

Question

Reference;

http://www.samos.aegean.gr/math/kker/papers/CompactMetric.pdf

The paper says "Compact metric space is separable" is unprovable in ZF$^0$( That is, ZF without axiom of regularity).

And I know "Limit point compact" does not imply "separable" in ZF

I searched for it, but couldn't find whether "Compact metric space $\Rightarrow$ Separable"

Is it provable in ZF?

Thank you in advance

Answer 1

It is an exercise in Herrlich The Axiom of Choice, E.9 p. 85.

The statement that every compact metric space is separable is equivalent to that of "countable sum of compact metric spaces are separable".

The latter is not provable without the axiom of choice, because if there is a countable set of pairs whose union is a Dedekind-finite set (i.e. a Russell set) then each of the pairs is a compact metric space with the discrete topology, but the union is not a separable space.

---

The exercise itself is referred from:

K. Keremedis and E. Tachtsis. Countable sums and products of metrizable spaces in ZF. Math. Logic Quart. 51:95–103, 2005.