S is uncountable := |$\mathbb{N}$| < |S|
  

S is noncountable := |S| $\not\leq |\mathbb{N}|$
  

(X,$T$) is a nice space := (X,$T$) is a compact Hausdorff space without isolated points


Does [ ZF / ZF + Countable Choice ] prove that every nice space is [ uncountable / noncountable ] ?
  

If not, is it known to prove that the statement implies some choice principle?
  

What if the spaces are additionally assumed to be metrizable?


Now, that's basically 12 questions, so I certainly don't anticipate answers for all of them.
  

If it matters, the one I'm most curious about is "Does ZF prove that every nice space is noncountable?".



Compact Hausdorff spaces without isolated points in ZF
One of the usual ways of proving in ZFC that every compact
Hausdorff space $X$ without isolated points ([perfect
space](http://en.wikipedia.org/wiki/Perfect_space)) is
uncountable is by proving that there is a copy of the
Cantor space $2^\omega$ inside it, as follows. Pick two
points and separate them with neighborhoods $U\_0, U\_1$
having disjoint closures. Inside each of these
neighborhoods, pick two points and separating neighborhoods
$U\_{00},U\_{01}\subset U\_0$ and $U\_{10},U\_{11}\subset U\_1$
having disjoint closures inside those neighborhoods, and so
on proceeding inductively. Every infinite binary sequence
$s\in 2^{\omega}$ determines a unique nesting sequence of
these sets, which must be nonempty. And so we have
continuum many points in $X$, so it is uncountable.


This proof, however, makes several uses of the axiom of
choice. First, we have the choices involved with picking
the points to be separated, and second, the choices
involved with picking the separating neighborhoods.
Although there are only countably many choices being made
here, this is an instance of [Dependent
Choice](http://en.wikipedia.org/wiki/Axiom_of_dependent_choice),
a stronger principle than mere countable choice, since the
choices are being made in succession. Finally, third, a
subtle point, we have the choices involved in picking for
each binary sequence a single point from the intersection
of the corresponding nested neighborhoods. After all, there
could be many points in that intersection.


With some additional assumptions on $X$, however, we can get around
these uses of choice, and thereby obtain answers to some of your questions. For example, if we only aim to prove
that $X$ is noncountable, rather than uncountable, then we
may assume towards contradiction that $X$ is countable, which provides for us a
canonical way of picking points from the space. (In the
case of the first use of choice, it would suffice if $X$
were separable, since we could just pick points from a
fixed countable dense set.) If $X$ were a metric space,
then we have a canonical way to pick neighborhoods of any
given point. Also, by making these neighborhoods shrink to $0$ as
the construction proceeds, we ensure that the intersection
of the nested sets contains a single point.


Thus, this argument shows in ZF, without any choice, that
every compact Hausdorff metric space having no isolated
points is noncountable. More generally, it shows, again without any choice, that every separable compact Hausdorff metric space without isolated points has uncountable size at least continuum.


If we have Dependent Choice, then we can prove that every
compact Hausdorff metric space is uncountable of size at
least continuum, since DC allows us to overcome the first
two uses of choice (picking the points and the
neighborhoods), and by shrinking the neighborhoods we avoid
the need for choice in the last step.


A clever person may be able to
improve these arguments to cover additional cases.


Meanwhile, let me mention an interesting example on the other side of the question. This example illustrates that several of the usual equivalent formulations of compactness are no longer equivalent in the non-AC context. Namely, it is consistent with ZF that there is an infinite but [Dedekind finite](http://en.wikipedia.org/wiki/Dedekind-finite) set $D$ of real numbers. That is, $D$ is infinite, but has no countably infinite subset. It follows that $D$ has at most finitely many isolated points, since otherwise we could enumerate the rational intervals and find these isolated points, thereby enumerating a countably infinite subset of $D$, which is impossible. Let us simply omit these finitely many isolated points and thereby assume without loss of generality that $D$ is an infinite Dedekind-finite set of reals having no isolated points. Since $D$ is Dedekind-finite, every sequence in $D$ has only finitely many values and hence has a convergent (constant) subsequence. Thus, $D$ is a sequentially compact set of reals. In other words, $D$ is a sequentially compact metrizable space with no isolated points. However, $D$ is not uncountable in the sense you mentioned, since we don't even have $|\mathbb{N}|\leq D$, as there is no countably infinite subset of $D$. Nevertheless, $D$ is noncountable. 


