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?

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.

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,