How do I apply the Boolean Prime Ideal Theorem? I have become aware of an amazing phenomenon from a myriad of questions and answers here on MathOverflow: many of the results that I would typically prove using the Axiom of Choice can actually be proved using the logically weaker Boolean Prime Ideal Theorem.  Apparently, the following can be proved using the BPI theorem:


*

*Every nonzero commutative unital ring contains a prime ideal

*Every field has an algebraic closure

*The Hahn-Banach Theorem

*Every formally real field can be totally ordered
I tempted to believe that almost every application of the Axiom of Choice that I would use in my everyday work actually follows from the Boolean Prime Ideal Theorem (except for those obviously equivalent to the Axiom of Choice, such as: every epimorphism in the category of sets is split).  
Thus I wish to ask: Given that I know how to prove many "everyday" mathematical statements using the Axiom of Choice, how can I learn to prove them with the weaker Boolean Prime Ideal Theorem?

To make the question more precise, let's suppose that I know how to prove a result using Zorn's Lemma.  Is there some standard method that I can use to put in just a bit more work and extract the same theorem using the BPI theorem?  
The best I can think to do would be to use the restatement of the BPI theorem as the existence of ultrafilters.  I have only ever seen this stated as being equivalent to the existence of an ultrafilter on every set.  So first I should probably ask: does the BPI theorem that every filter on a ("nice enough") poset is contained in an ultrafilter?
If I have a poset $\mathcal{P}$ satisfying the usual Zorn property, the nice thing about Zorn's lemma is that it gives me an actual maximal element of the poset $\mathcal{P}$.  The problem I see with existence of ultrafilters in $\mathcal{P}$ is that I do not obtain an actual element of $\mathcal{P}$, but a (rather large) subset.  Is there a standard way that I can translate this back into an element of my poset $\mathcal{P}$?  (For instance, should I pass to a least upper bound, because the posets that usually arise in Zorn applications are upper-complete?)
For instance, let's consider the first of the examples on the list above.  Say $R$ is a commutative unital ring, and let $I \subsetneq R$ be a proper ideal of $R$.  How can I prove using the BPI theorem that there is a prime ideal of $R$ containing $I$?  I would typically consider the poset $\mathcal{P}$ of proper ideals of $R$ containing $I$, use Zorn's lemma to produce a maximal element $M$ of $\mathcal{P}$ (which will actually be a maximal ideal), and then prove that $M$ is prime.  Supposing that the BPI theorem really gives me existence of ultrafilters in $\mathcal{P}$, I would probably start by considering the filter $\mathcal{F}$ of ideals containing $I$, and then pass to an ultrafilter containing this.  Is there some way for me to obtain a prime ideal from such an ultrafilter?  (And as I asked above, do I really obtain such an ultrafilter from the BPI theorem?)
I have included the "reference-request" tag because I would be satisfied with a reference to a survey paper that would teach me how to effectively apply the BPI theorem in a number of instances (including the ones above).  While I would certainly be interested in references that show how to prove the above results (and any others!) using the BPI theorem, this would not be the kind of answer that I seek.  
 A: When I attempt to prove a result using BPI, my first attempt is usually to translate the problem into a satisfiability problem in propositional logic and use the Compactness Theorem (which is equivalent to BPI).
For example, to prove that every commutative ring $R$ has a prime ideal, consider the theory with one proposition $P_a$ for every $a \in R$ and the axioms:
$$P_0, \lnot P_1, P_a \land P_b \to P_{a+b},P_a \to P_{ab}, P_{ab} \to P_a \lor P_b.$$ It's not difficult to show that this theory is finitely satisfiable. By the Compactness Theorem, the theory is satisfiable and, given a truth assignment that satisfies this theory, the set of all $a \in R$ such that $P_a$ is true forms a prime ideal of $R$.
Other examples of this trick can be found in my answers here and here.
This is not similar to Zorn's Lemma but I would contend that almost all similar maximality principles tend to give more than BPI would. The Consequences of the Axiom of Choice Project lists a great deal of equivalent statements to BPI (Form #14), very few bear much resemblance to Zorn's Lemma. Also note that all of them have some form of "finiteness" aspect to them which can be difficult to incorporate into maximality principles.
A: I think that there is no general method to extract  a "BPI" argument from a  "Zorn" argument.   But I think that in many  cases it is easiest to phrase the BPI argument in terms of propositional logic, as follows: 
Start with a list of yes/no questions that the desired object (the prime ideal $M$ of your ring, the linear order of your field, etc) should answer: 


*

*Is $x$ in $M$? Is $y$ in $M$? (for all ring elements) 

*Is $x \le y$? Is $p \le q$? (for all field elements.  Of course you could be more economical and only ask questions of the form "Is $x\ge 0$?")

*etc. 


Associate each question with a propositional variable, or in algebraic terms: with a generator of a free Boolean algebra. 
Now write a wishlist of relations between the answers to these questions.  If $\bar x$ is the variable/generator corresponding  to the question "Is $x\in M$?", for any $x$ in the ring, then you want $\bar x \wedge \bar y \to \overline {x-y}$. (In the algebraic formulation, this is an element of the free algebra.  "$\wedge$" and "$\to$" are  the obvious binary operations on Boolean algebras, "$-$" is ring subtraction.) 
The characteristic property of primeness is represented by the Boolean term $\overline{xy} \to (\bar x \vee \bar y)$.  The characteristic property for linearity is represented by $\hat x \vee \widehat{-x}$, if $\hat x$ is the generator for the question "$x\ge 0$".  
Collect your wishlist in a filter, and find an ultrafilter extending this filter.  All generators/questions in the ultrafilter will get the answer "true"/"yes", hence also all formulas on your wishlist will get the value "true". 
It seems to me that this method also works for Hahn-Banach. Your questions about the desired function $f$ (bounded by $\varphi$) will be of the form "Is $f(x) \le r$" for all vectors $x$ and all real   numbers $r$. Your wishlist includes statements of the form $\overline{f(x) \le r}$ whenever $r=\varphi(x)$, or $\overline{f(x)\le r} \to \overline{f(y) \le s}$ whenever $y=\lambda x$, $\lambda>0$, $s=\lambda r$. 
