To what extent does the usual StoneWeierstrass Theorem depend on some form of the Axiom of Choice? There seems to be a lot of literature on constructive versions in toposes, but I have been unable to find a clear statement about the dependence of the usual theorem on the AC, or a counterexample without AC. And what about the metrizable or second countable case?

1$\begingroup$ Let me mention at least that the Weierstrass approximation theorem, asserting that every real continuous function on a closed interval $[a,b]$ in the reals is uniformly approximated by polynomials, does not use AC. To see this, observe that if $f:[a,b]\to\mathbb{R}$ is continuous, then $f$ is coded by a real, and the relative constructive universe $L[f]$ is therefore a model of ZFC, which therefore has the desired approximating polynomials, and the fact that they work is absolute to the ambient settheoretic universe $V$. So even if AC fails, we still get the polynomial approximations. $\endgroup$– Joel David HamkinsApr 23 at 15:52

6$\begingroup$ The proof of the Weierstrass Approximation Theorem using Bernstein polynomials does not use any choice. $\endgroup$– Bruce BlackadarApr 23 at 16:18

2$\begingroup$ @GeraldEdgar Bruce's proof depends on inspecting the proof of the Weierstrass Approximation Theorem; Joel's depends only on the theorem's statement. $\endgroup$– Andreas BlassApr 23 at 17:13

1$\begingroup$ @BruceBlackadar Yes. My argument was simply to point out that the approximation theorem is not the sort of mathematical statement that can depend on AC. Another way to see this: the theorem has complexity $\Pi^1_2$, which is therefore absolute to $L$, where AC holds. So it holds in $V$. $\endgroup$– Joel David HamkinsApr 23 at 18:34

1$\begingroup$ A completely regular space $X$ is compact iff each bounded unital subalgebra that separates points in $X$ uniformly approximates every bounded continuous realvalued function. This question is therefore about how different equivalent definitions of compactness bifurcate in the absence of choice. $\endgroup$– Joseph Van NameApr 23 at 19:59
1 Answer
Caveat  I am not well versed in working with mathematics without the axiom of choice, so this answer should be taken with a grain of salt.
This question seems to be sensitive to the precise definition of compactness, continuity, and separation of points. Here I use the following definitions:
 A space $X$ is compact if and only if for all open covers ${\mathcal U}$ there exists a finite subcover $U_1,\dots,U_n$ of ${\mathcal U}$. [We do not require that there is a choice function from ${\mathcal U}$ to $(U_1,\dots,U_n)$. We also do not require that the open cover come with a choice function $x \mapsto U_x$ from each point $x \in X$ to an open set $U_x$ in the cover that contains it.]
 A function $f: X \to Y$ is continuous if and only if the inverse image of every open set is open.
 An algebra ${\mathcal A} \subset C(X) = C(X \to {\bf R})$ separates points if and only if, for every distinct $x,y \in X$, there exists a function $f \in {\mathcal A}$ such that $f(x) \neq f(y)$. [We do not require that there is a choice function from $(x,y)$ to $f$.]
(I will leave it to the experts to work out what happens if we use netbased, sequencebased, or ultrafilterbased definitions of compactness and/or continuity instead.)
Then:
StoneWeierstrass Theorem Let $X$ be a compact space, and let ${\mathcal A} \subset C(X)$ be a unital algebra that separates points. Then for any $f \in C(X)$ and $\varepsilon > 0$ there exists $g \in {\mathcal A}$ such that $d(f,g) \leq \varepsilon$ (where $d$ denotes the uniform metric).
[Strictly speaking, this is only one direction of the StoneWeierstrass theorem; the converse direction, which is essentially Urysohn's lemma for compact Hausdorff spaces, asserts that if $X$ is additionally assumed to be Hausdorff, then any dense subset of $C(X)$ must necessarily separate points. This direction appears to be more reliant on the axiom of choice, but I will not pursue this question further here, as the direction stated above is the one which is most commonly invoked in applications.]
Proof This is going to be the textbook proof of StoneWeierstrass, with all unnecessary references to choice functions removed (and also by refusing to pass to the uniform closure of the algebra, though this seems less critical to me).
First observe from the Weierstrass approximation theorem (which as noted in comments is completely constructive) that for any $f,g \in {\mathcal A}$ and $\varepsilon > 0$ there exists $h \in {\mathcal A}$ such that $d(\max(f,g),h) \leq \varepsilon$. Similarly with $\max$ replaced by $\min$. By induction, this implies that ${\mathcal A}$ is closed under arbitrary finite lattice operations to arbitrary error in the uniform topology. [Here we are using the fact that continuous functions on a compact set are bounded, which is still true without AC with our definitions, as one can easily check by inspecting the standard proof (the collection of open sets on which the function is bounded is an open cover).]
We have the following key subclaim: if $f \in C(X)$, $x \in X$ and $\varepsilon>0$, then there exists $g \in {\mathcal A}$ such that $f(x)g(x) \leq \varepsilon$ and $g(y) \leq f(y)+\varepsilon$ for all $y \in X$.
To prove the subclaim, consider the collection ${\mathcal U}$ of open sets $U$ for which there exists a function $g \in {\mathcal A}$ such that $f(x)g(x) \leq \varepsilon$ and $g(y) \leq f(y)+\varepsilon$ for all $y \in U$. By continuity of $f$, there is a neighbourhood of $x$ that lies in ${\mathcal U}$. Because ${\mathcal A}$ is a unital algebra that separates points and $f$ is continuous, every $y$ not equal to $x$ has a neighborhood that lies in ${\mathcal U}$. Hence ${\mathcal U}$ is an open cover of $X$, hence by compactness there is a finite subcover $U_1,\dots,U_n$. By finite choice, for each $i=1,\dots,n$ one can find $g_i \in {\mathcal A}$ such that $f(x)g_i(x) \leq \varepsilon$ and $g_i(y) \leq f(y)+\varepsilon$ for $y \in U_i$. By preceding remarks, we can find $g \in {\mathcal A}$ which lies within $\varepsilon$ in the uniform metric of $\min(g_1,\dots,g_n)$, then $f(x)g(x) \leq 2\varepsilon$ and $g(y) \leq f(y)+2\varepsilon$ for all $y \in X$. The claim now follows after replacing $\varepsilon$ with $\varepsilon/2$.
Now for a given $f \in C(X)$, let ${\mathcal V}$ denote the open sets $V$ for which there exists $g \in {\mathcal A}$ such that $f(x)g(x) \leq \varepsilon$ for $x \in V$ and $g(y) \leq f(y)+\varepsilon$ for all $y \in X$. By the preceding claim and continuity (replacing $\varepsilon$ with $\varepsilon/2$) we see that every $x \in X$ has a neighbourhood in ${\mathcal V}$, thus ${\mathcal V}$ is an open cover of $X$. By compactness it has a finite subcover $V^1,\dots,V^m$. By finite choice, for each $i=1,\dots,m$ we can find $g^i \in {\mathcal A}$ such that $f(x)g^i(x) \leq \varepsilon$ for $x \in V^i$ and $g^i(y) \leq f(y) + \varepsilon$ for $y \in X$. By the previous discussion, we can find $g \in {\mathcal A}$ that lies within $\varepsilon$ of $\max(g^1,\dots,g^m)$. Then $f(x)g(x) \leq 2\varepsilon$ for all $x \in X$, giving the claim after replacing $\varepsilon$ with $\varepsilon/2$ one final time. $\Box$
I think what is going on here is that compactness becomes a strong hypothesis in the absence of choice  so strong, in fact, that while the StoneWeierstrass theorem is technically provable without AC, it is somewhat useless since there are so few provably compact spaces one can apply it to.

1$\begingroup$ (ZFC) One can also characterize compactness in terms of the StoneWeierstrass theorem, so the question is about various characterizations of compactness without AC. If $X$ is completely regular but not compact, then we select $x_0\in X,y_0\in \beta X\setminus X$ and define $\mathcal{A}$ as the collection of all bounded continuous functions $f:X\rightarrow\mathbb{R}$ where $f(x_0)=\overline{f}(y_0)$, then $\mathcal{A}$ is a bounded unital algebra that separates points in $X$ but is not uniformly dense in the space $C^*(X)$ of bounded continuous functions. $\endgroup$ Apr 23 at 20:03

3$\begingroup$ Thanks, this proof looks good. The technique is similar to what one must do to prove, for example, that a compact Hausdorff space is normal without using AC. Some other comments: (1) Your definitions of compactness and continuity are standard, and are equivalent to the net definitions even without AC, but not to sequential or ultrafilter definitions. (2) Compactness is not so rare without AC. For example, it can be proved without any choice that the Hilbert cube is compact, and so is any closed subset, and in particular any closed bounded subset of Euclidean space is compact. $\endgroup$ Apr 23 at 20:20

$\begingroup$ There are many others, such as the onepoint compactification of any locally compact Hausdorff space (e.g. any set with the discrete topology, or any topological manifold). (3) Not relevant to StoneWeierstrass, but it cannot be proved without some choice (Dependent Choice suffices) that a compact Hausdorff space is completely regular. There are even compact Hausdorff spaces (Läuchli continua) on which every realvalued continuous function is constant, where StoneWeierstrass has no content. $\endgroup$ Apr 23 at 20:26

1$\begingroup$ Yes. Urysohn's Lemma requires Dependent Choice since a sequence of separating open sets must be successively chosen, but in the metrizable case they can be defined canonically so no choice is needed. $\endgroup$ Apr 24 at 16:32

1$\begingroup$ I believe it's even simpler than that: If $X$ is metrizable and $\varnothing\neq A,B\subset X$ are closed with $A\cap B=\varnothing$, then defining $$f(x)=\frac{d(x,A)}{d(x,A)+d(x,B)}\ ,$$ with $d$ a distance function on $X$ that induces its topology and $d(x,C)=\text{inf}\{d(x,y)\ \ y\in C\}$ for $\varnothing\neq C\subset X$, yields that $f:X\rightarrow[0,1]$ is continuous, $f^{1}(0)=A$ and $f^{1}(1)=B$. The only choice made is that of $d$. $\endgroup$ Apr 24 at 17:01