It's well known that the nilradical of a commutative ring with identity $A$ is the intersection of all the prime ideals of $A$.

Every proof I found (e.g. in the classical "Commutative Algebra" by Atiyah and Macdonald) uses Zorn's lemma to prove that $x \notin Nil(A) \Rightarrow x \notin \cap_{\mathfrak{p}\in Spec(A)} \mathfrak{p}$ (the other way is immediate). Does anybody know a proof that doesn't involve it?

-
I don't know whether this is your goal, but if you are trying to do constructive algebra, then the trick is not to prove constructively the assertion that the nilradical is the intersection of all primes (this is impossible), but to (automatically?) rewrite every proof using this assertion into a proof that doesn't use it. Henri Lombardi and Thierry Coquand have written up examples of such rewriting. –  darij grinberg Jun 5 '10 at 16:28

Since you asked for a proof, let me complement Chris Phan's answer by outlining a proof that relies only on the Compactness Theorem for propositional logic, which is yet another equivalent to the Ultrafilter Theorem over ZF.

Let A be a commutative ring and let x ∉ Nil(A). To each element a ∈ A associate a propositional variable pa and let T be the theory whose axioms are

• p0, ¬p1, ¬px, ¬px2, ¬px3,...
• pa ∧ pb → pa+b for all a, b ∈ A.
• pa → pab for all a, b ∈ A.
• pab → pa ∨ pb for all a, b ∈ A.

Models of T correspond precisely to prime ideals that do not contain x. Indeed, if P is such an ideal, then setting pa to be true iff a ∈ P satisfies all of the above axioms, and conversely. So it suffices to show that T has a model.

Since xn ≠ 0 for all n, one can verify using ideals over finitely generated subrings of A that the theory T is finitely consistent, i.e. any finite subset of T has a model. (What I just swept under the rug here is a constructive proof of the theorem for quotients of Z[v1,...,vn].) The Compactness Theorem for propositional logic then ensures that T has a model.

-
Very nice. I think the prove for finitely generated rings (which does not use the axiom of choice) just uses that they are noetherian. –  Martin Brandenburg Jun 6 '10 at 8:31
Thank you, François! –  Wadim Zudilin Jun 7 '10 at 21:21
Wow, really useful, thanks! I'd like to gain experience with model theory, it seems really interesting... –  Daniele Turchetti Jun 8 '10 at 7:37
Since the compactness theorem for propositional logic for countable many variables is even true in ZF (mathoverflow.net/questions/81348) this shows that every countable ring satisfies "nilradical = intersection of prime ideals" in ZF, right? –  Martin Brandenburg Dec 1 '11 at 16:47
Yes, all you need in that case is Konig's Lemma (every infinite, finitely branching tree has an infinite path) which is true in ZF and much weaker systems. –  François G. Dorais Dec 1 '11 at 20:28

Y. Rav proved this using the Ultrafilter Principle ("Every filter on a set can be extended to an ultrafilter"), which is weaker than the Axiom of Choice. Theorem 4.1 of Variants of Rado's selection lemma and their applications, Math. Nachr. 79 (1977), 145--165 states:

Theorem 4.1. Let R be a ring, $\mathfrak{a}$ a proper ideal in R, and suppose that S is multiplicative subsemigroup of R which does not meet $\mathfrak{a}$. Then it follows from the Ultrafilter Principle that their exists a prime ideal $\mathfrak{p}$ in R such $\mathfrak{a} \subseteq \mathfrak{p}$ and $\mathfrak{p} \cap S= \emptyset$.

Rav also showed:

Corollary 4.4. The following statements are mutually equivalent in ZF set theory:
(a) Every filter on a set can be extended to an ultrafilter.
(b) In every commutative associative ring with identity, every proper ideal is included in some prime ideal.
(c) In every Boolean algebra, every proper ideal (resp. filter) is included in some prime ideal (resp. ultrafilter).
-

I assume the argument you have in mind is the folowing: suppose $f \in \cap \mathfrak{p}$; then to show that $f$ is nilpotent, it suffices to show that the localized ring $A_f$ is zero. And indeed, if $f$ is in every prime ideal of $A$, then $A_f$ has no prime ideals at all; since every nonzero ring has a maximal ideal by Zorn's Lemma, we must have $A_f = 0$.

This line of reasoning easily adapts to show that in fact, the statement that $\operatorname{Nil}(A) = \cap \mathfrak{p}$ implies that every nonzero ring has a prime ideal. Indeed, suppose that $A$ were nonzero with no prime ideals; then $\cap \mathfrak{p} = A$, so every element of $A$ is nilpotent. In particular, $1 = 1^n = 0$, so $A = 0$.

Following Eric Rowell's answer, this is very close to being equivalent to the axiom of choice (however, it does not obviously imply the existence of maximal ideals).

-
Although I am sure they are essentially the same argument, the argument in Atiyah-Macdonald is given before localization is introduced (and is less straightforward than the argument above). –  Charles Staats Jun 5 '10 at 17:33

This seems difficult as Krull's theorem (existence of maximal ideals) implies the Axiom of Choice. This is due to W. Hodges I think.

-