Does ZF prove that proximity spaces are completely regular?

(This is based on my earlier question, but I think this one would be easier to answer.)

Let $\langle X,\mathbf{\delta} \hspace{.01 in} \rangle$ be a separated proximity space, and let $\cal{T}\hspace{.04 in}$ be the induced topology on $X$.
Then, ZF proves that $\langle X,\cal{T}\hspace{.06 in} \rangle$ is regular Hausdorff, and
ZF + (Dependent Choice) $\;$proves that $\langle X,\cal{T}\hspace{.06 in} \rangle$ is completely regular.

Does ZF prove that $\langle X,\cal{T}\hspace{.06 in} \rangle$ is completely regular?

-
ZF does not even prove that every compact Hausdorff space is completely regular. – Emil Jeřábek Aug 29 '11 at 12:56
@Emil: Do you know of a reference for this fact? – Andrej Bauer Aug 29 '11 at 14:19
I don’t know of a reference, but since this is an easy basic result, it should be somewhere. One way to prove this is to use the following variant of the ordered Mostowski model (this is a permutation model, i.e., a model of ZFA, but it can be made a model of ZF using the Jech–Sochor embedding theorem): assume that the set $A$ of atoms is in 1–1 correspondence with $[0,1]$, and consider the permutation model $M$ determined by the group of order-preserving permutations of $A$ and the normal filter of its subgroups with finite support. Then $M$ contains $A$ and its order, which induces ... – Emil Jeřábek Aug 29 '11 at 16:42
.. the order topology on $A$. Crucially, the only subsets of $A$ in $M$ are finite unions of intervals (possibly degenerate), and a function $f\colon A\to\mathbb R$ is in $M$ only if there is a partition of $A$ to finitely many intervals such that $f$ is constant on each interval. In particular, every continuous $f$ is constant. On the other hand, $A$ is Hausdorff, and it is easy to see that the compactness of $A$ in the original model implies its compactness in $M$. – Emil Jeřábek Aug 29 '11 at 16:47
Since the only order-preserving permutation of $A$ with finite support is the identity, I don't see how that gives a model of ZFA. $\;$ Assuming it does, wouldn't you argument show that the resulting space also fails to be completely Hausdorff? (en.wikipedia.org/wiki/Completely_Hausdorff_space) – Ricky Demer Aug 29 '11 at 17:21

The answer is no. In fact, it is consistent with ZF that $(*)$ there exists an infinite compact Hausdorff space $X$ such that every continuous function $f\colon X\to\mathbb R$ is constant, so that $X$ is not even completely Hausdorff.

A simple example can be given using a Fraenkel–Mostowski permutation model of ZFA (ZF with atoms). The general setup is as follows. We work in a model of ZFA + AC where the atoms form a set $A$. We are given a group $G$ of permutations of $A$, and a normal (= closed under the action of $G$ by conjugation) filter $F$ of subgroups of $G$ such that the stabilizer of every point $a\in A$ belongs to $F$. (The smallest such filter consists of all subgroups $H\subseteq G$ of finite support, i.e., such that $H$ includes the point-wise stabilizer of some finite subset of $A$.) The action of $G$ on $A$ can be extended to the whole universe so that $g(x)=\{g(y):y\in x\}$ for every set $x$. An object $x$ is symmetric if its stabilizer belongs to $F$, and it is hereditarily symmetric if every element of the transitive closure of $\{x\}$ is symmetric. Then one can show that the class $M$ of hereditarily symmetric objects is a transitive model of ZFA.

Now, in our particular case, assume that $A$ has the power of continuum so that we can put it in a 1–1 correspondence with $[0,1]$, and let $<$ be the induced order on $A$. We take for $G$ the group of all order-preserving permutations of $A$, and for $F$ the above mentioned minimal filter of subgroups with finite support. Let $M$ be the resulting permutation model. (This is a minor variant of the Mostowski ordered model, which has $(A,< )$ isomorphic to $\mathbb Q$ instead of $[0,1]$.)

$M$ contains the totally ordered set $(A,< )$, since every $g\in G$ preserves $<$. The induced order topology on $A$ is clearly Hausdorff, and it is also compact: if $C\in M$ is an open cover of $A$, it has a finite subcover $C'$ in the ambient model by compactness of $[0,1]$; we have $C'\in M$, because it is a finite subset of $M$.

On the other hand, let $f\colon A\to\mathbb R$ belong to $M$. Then there exists a finite subset $a=\{a_1<a_2<\dots<a_n\}\subseteq A$ such that every $g\in G$ that preserves $a$ also preserves $f$. This is easily seen to imply that $f$ is constant on every interval $(a_i,a_{i+1})$. (The only property of $\mathbb R$ we need here is that it is a pure set, and therefore all its elements are fixed by $G$.) In particular, if $f$ is continuous, it is constant.

In this way, we construct a model of ZFA + $(*)$. We can use the Jech–Sochor embedding theorem to obtain a model of ZF + $(*)$. Moreover, Halpern proved that the Boolean prime ideal theorem (BPI) holds in Mostowski’s ordered model; I suppose that BPI also holds in the model $M$ above by the same argument, hence $(*)$ is consistent with ZFA + BPI. I guess that it is also consistent with ZF + BPI, but I can’t vouch for it, as the Jech–Sochor theorem does not apply to BPI.

-
I've managed to convince myself that the order topology on $A$ is still given by a uniform structure. So I think this shows that uniformizability and complete regularity are not the same in this model. However, I'm not so enlightened when it comes to proximities (both specifically and in general). How does one define the proximity structure on $A$? – François G. Dorais Aug 30 '11 at 16:35
Every compact Hausdorff space is induced by a unique uniformity (whose entourages are simply all neighbourhoods of the diagonal); the proof of this does not need AC. I’m not really familiar with proximities, but I relied on Wikipedia’s word that, likewise, every compact Hausdorff topology is induced by a (unique) proximity space, namely $A\mathrel{\boldsymbol\delta}B$ iff $\overline A\cap\overline B\ne\varnothing$. Is there a problem with that? – Emil Jeřábek Aug 30 '11 at 17:51
Right, it is easy to verify from the definition that the formula above defines a proximity space inducing the original topology for any $T_4$ space. ZF proves that compact Hausdorff spaces are $T_4$. – Emil Jeřábek Aug 30 '11 at 19:13