In ZF, does the ring of continuous functions $C([0,1], \mathbb{R})$ have prime ideals which is not maximal? In ZFC, it is known that the ring of continuous functions $C([0,1], \mathbb{R})$ have prime ideals which is not maximal. But all proofs of this which I saw uses the axiom of choice.
Then, in ZF, does the same statement hold?
If ZF cannot prove this, how strong is $\mathrm{ZF}+(\text{$C([0,1], \mathbb{R})$ has prime ideals which is not maximal})$ as an intermediate between ZF and ZFC?
 A: No, the existence of such a nonmaximal prime ideal cannot be proved in ZF.  In fact, the existence of such a nonmaximal prime ideal is equivalent to the existence of a nonprincipal ultrafilter on $\mathbb{N}$.
First, suppose $F$ is a nonprincipal ultrafilter on $\mathbb{N}$.  Let $I$ be the set of continuous $f:[0,1]\to \mathbb{R}$ such that $\{n\in\mathbb{N}:f(1/n)=0\}\in F$.  It is then easy to see that $I$ is an ideal in $C([0,1],\mathbb{R})$, and it is prime since $F$ is an ultrafilter.  However, it is not maximal since it is strictly contained in the ideal of functions that vanish at $0$.
Conversely, suppose no nonprincipal ultrafilter on $\mathbb{N}$ exists and $I\subset C([0,1],\mathbb{R})$ is a prime ideal; we will prove $I$ is maximal.  For each $a\in[0,1]$ and each $n\in\mathbb{N}$, let $f_{n,a}:[0,1]\to\mathbb{R}$ be the function that is $0$ on $[a-1/n,a+1/n]$, $1$ off of $[a-2/n,a+2/n]$, and interpolates linearly in between.  I claim that there exists some $a\in[0,1]$ such that $f_{n,a}\in I$ for all $n$.  To prove this, suppose no such $a$ exists; for each $a$, let $n_a$ be minimal such that $f_{n_a,a}\not\in I$.  By compactness, finitely many of the intervals $(a-1/n_a,a+1/n_a)$ cover $I$.  But then the product of the corresponding $f_{n_a,a}$s is $0$, contradicting primeness of $I$ since each $f_{n_a,a}$ is not in $I$.
So, we have a point $a\in[0,1]$ such that $f_{n,a}\in I$ for all $n$.  It follows that every function that vanishes in a neighborhood of $a$ is in $I$, since every such function is divisible by some $f_{n,a}$.  I now claim that in fact $I$ contains every function that vanishes at $a$, and thus is maximal.  To prove this, suppose that $f\in C([0,1],\mathbb{R})$ is a function which vanishes at $a$.  To show that $f\in I$, it suffices to show that $f^2\in I$ since $I$ is prime.
Replacing $f$ by $f^2$, we may assume $f\geq 0$ and we wish to show $f\in I$.
Fix an increasing sequence $(a_n)$ converging to $a$ with $a_0=0$.  Let $F$ be the set of all $A\subseteq\mathbb{N}$ such that there exists $g\in I$ such that $g\geq 0$ everywhere and $g\geq f$ on $[a_{2n},a_{2n+1}]$ for all $n\not\in A$.  It is easy to see that $F$ is a filter on $\mathbb{N}$, and it contains all cofinite sets since $I$ contains all functions that vanish in a neighborhood of $a$.  Note also that if $A\subseteq\mathbb{N}$, then we can construct a function $g$ which is $f$ on $[a_{2n},a_{2n+1}]$ for all $n\not\in A$ and $0$ outside of small neighborhoods of these intervals, and similarly we can construct a function $h$ with the same property with respect to $\mathbb{N}\setminus A$.  Then $gh=0$ so either $g\in I$ or $h\in I$, so either $A\in F$ or $\mathbb{N}\setminus A\in F$.
Since by hypothesis, $F$ cannot be a nonprincipal ultrafilter on $\mathbb{N}$, the only remaining possibility is that $F$ is the improper filter, i.e. $\emptyset\in F$.  So there is a nonnegative function $g_1\in I$ such that $g_1\geq f$ on $[a_{2n},a_{2n+1}]$ for all $n$.  Similarly, there is a nonnegative function $g_2\in I$ such that $g_2\geq f$ on $[a_{2n-1},a_{2n}]$ for each $n$.  Adding up $g_1$ and $g_2$, we get a nonnegative element of $I$ which is bounded below by $f$ on all of $[0,a]$.  We can similarly get a nonnegative element of $I$ that is bounded below by $f$ on all of $[a,1]$.  Adding these functions together, we get a function $g\in I$ such that $g\geq f$ on all of $[0,1]$.  Now note that $f^2/g$ extends continuously to all the points where $g$ vanishes, since $f$ also vanishes at those points and $f^2/g$ is bounded above by $f$ outside them.  Thus $f^2$ is a multiple of $g$ and hence is in $I$.  Since $I$ is prime, this means $f\in I$, as desired.
A: I haven't found a construction in ZF, but I found this paper which explores the spectrum of $C(X, \mathbb R)$ for $X$ an arbitrary topological space. It gets a bit heavy when the interaction with the Stone-Cech compactification shows up and partially ordered groups/rings appear, and I couldn't find a constructive approach to finding a prime ideal in $C(X,\mathbb R)$ either. But the relationship between
$$
\mathfrak m_x = \{ f \in C(X,\mathbb R) \, | \, f(x) = 0 \}
$$
and
$$
\mathfrak n_x = \{ f \in C(X,\mathbb R) \, | \, \exists V \text{ neighborhood of } x \, \mathrm{s.t.} f|_V = 0 \} 
$$
seems to be extensively studied.
I'm curious to see if one could simplify the paper for the case of $C([0,1],\mathbb R)$ (so that the need for the Stone-Cech compactification goes away, simplifying many results) and shed some light on this question that has been triggering me (and probably a lot of other people) for many years. Let me know if you bump into anything interesting.
Hope that helps,
