A prime ideal theorem is a theorem stating that every proper ideal is contained in some prime ideal. A prime ideal theorem is typically equivalent to the ultrafilter principle (UF), a weak form of the axiom of choice (AC).
We say ‘a’ prime ideal theorem (PIT) instead of ‘the’ prime ideal theorem, since we have not said what the ideals are in. There are several examples:
The PIT for rings is equivalent to UF.
The PIT for distributive lattices is equivalent to UF.
The PIT for Boolean algebras is equivalent to UF.
The PIT for rigs, which subsumes all of the above, is probably also equivalent to UF; in any case, it follows from AC.
One typically proves a prime ideal theorem with Zorn's Lemma, unless one is specifically trying to use something weaker.
A typical way in which these proofs work uses a Compactness Theorem for first-order logic (or Tychonoff theorem for compact Hausdorff spaces) as a stepping stone. These and the Boolean algebra PIT (better known as the Boolean prime ideal theorem, or BPIT) form a circle of ideas on which these logical or model-theoretic methods depend, so we’ll go into that equivalence first.
First, prime ideals in Boolean algebras (or Boolean rings) $B$ are the same as maximal ideals, and these just correspond to ultrafilters (see here). So UF, which says that every filter in $B = P X$ is contained in an ultrafilter, is just a special case of the BPIT: every ideal of $P X$ (consisting of negations of elements of a corresponding filter) is contained in a prime ideal. That the Tychonoff theorem for compact Hausdorff implies BPIT was proven here, noting that to prove that every proper ideal $I$ of $B$ is contained in a prime ideal, it suffices to find a prime ideal (or ultrafilter) of $B/I$, pulling it back along the quotient $B \to B/I$ to a prime ideal of $B$. This brings us full circle: BPIT implies UF implies Tychonoff(CH) implies BPIT.
Now let us prove that the Tychonoff theorem for CH spaces implies the PIT for rigs: that any proper ideal $I$ of $R$ is contained in a prime ideal of $R$. By passing to the quotient rig $R/I$, it suffices to show that $R/I$ has a prime ideal $P$, since the inverse image $\phi^{-1}(P)$ of a prime ideal $P$ along the quotient map $\phi: R \to R/I$ is again prime.
(UF) Any commutative ring $R$ has a prime ideal $P$.
To prove this, we are going to write down a propositional theory of “a prime ideal $P$ of $R$” (or, just as well, consider its Lindenbaum algebra?). Form a free Boolean algebra $Bool(U R)$ freely generated by the underlying set of $R$. So each $x \in U R$ corresponds to a generator $P_x \in Bool(U R)$, which we will think of as standing for a proposition $P_x =$ “$x \in P$”. The conditions that enforce “$P$ is a prime ideal” are then the axioms of our theory:
($P$ is closed under finite sums) $P_0$, $P_a \wedge P_b \Rightarrow P_{a+b}$.
($P$ is closed under multiplication by scalars) For each $b \in U R$, $P_a \Rightarrow P_{a b}, P_a \Rightarrow P_{b a}$.
($P$ is proper) $\neg P_1$.
(primality condition) $P_{a b} \Rightarrow (P_a \vee P_b)$.
These axioms (certain elements of $Bool(U R)$ then generate a filter $F$. As soon as we know $F$ is proper (“finite satisfiability of the theory”), the BPIT ensures that $F$ is contained in an ultrafilter $U$, corresponding to a model or a Boolean ring homomorphism $Bool(U R)/F \to \mathbf{2}$ out of the Lindenbaum algebra. For that model, the collection $\{a \in R: P_a \in U\}$ then forms a prime ideal $P$ of $R$, as desired. So:
(That the filter $F$ is proper.) This comes down to showing that any finitely generated commutative ring $R$ has a prime ideal. Now $R$ is of the form $\mathbb{Z}[x_1, \ldots, x_n]/I$ for some ideal $I$, so it comes down to showing that any ideal $I$ of $\mathbb{Z}[x_1, \ldots, x_n]$ is contained in a prime $p$. We argue by induction on $n$, and we permit ourselves to invoke WKL (weak König’s lemma), which follows from (UF) by the argument presented here. (…)
(To be continued, and probably radically rewritten later. I’m just learning of the equivalence between UF and very general prime ideals, including (and subsuming) those above, but I need to read more. One thing I’m looking at is here.)
Compare the maximal ideal theorem.