Halpern and Lévy 1971: the Boolean prime ideal theorem does not imply the Axiom of Choice

Write BPI for the Boolean prime ideal theorem, that every nontrivial Boolean algebra has a prime ideal; over ZF this is equivalent to the ultrafilter lemma (UL), that every filter on a set extends to an ultrafilter.

If ZF is consistent, then ZF + BPI + (not AC) is consistent. So BPI does not imply the Axiom of Choice over ZF.

Halpern and Lévy (1971) prove this in the basic Cohen model, the first symmetric model Cohen built: adjoin countably many mutually generic Cohen reals and take the symmetric submodel with finite supports and the group of all permutations of the index set. The Axiom of Choice fails there, because the set of adjoined reals cannot be well-ordered. That BPI nevertheless holds is the difficult half, and it rests on the Halpern-Läuchli partition theorem for products of finitely many trees.

Combined with Feferman 1965: ZF does not prove that a free ultrafilter on the naturals exists ‡ this places UL strictly between ZF and AC, relative to the consistency of ZF: UL is not provable in ZF, and UL does not recover AC.

• Which Cohen model this is. The model is the one recorded in Cohen's first model: an infinite Dedekind-finite set of reals ‡, Jech's basic Cohen model. Jech's second Cohen model is a different construction, the atom-free analogue of Fraenkel's socks (Fraenkel's socks: ZF does not prove choice for countably many pairs ‡), and is not the model used here. The distinction matters: BPI holds in the basic Cohen model, so free ultrafilters on $\mathbb{N}$ exist there, which is why Feferman 1965: ZF does not prove that a free ultrafilter on the naturals exists ‡ must use a different symmetric model altogether.

• Not proved in this library. Neither the symmetric model nor the Halpern-Läuchli partition theorem is developed here.

• What would prove it. The forcing track of Cohen 1963: ZF does not prove the Axiom of Choice ‡, plus a Ramsey-theoretic component: the Halpern-Läuchli theorem, and the deduction of BPI in the symmetric model from it. The partition theorem is genuinely combinatorial and is not implied by the forcing machinery alone.

• Why it matters here. The proved choice cost of the ultrafilter lemma ↗ and The proved choice ledger: hypotheses, equivalences, and upper bounds ↗ both quote this result, and it is what licenses the library's habit of naming The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter ↗ as a separate statement instead of inlining it into its applications. A theorem proved from UL costs strictly less than The Axiom of Choice ↗, and "strictly" is exactly this item.

• Conditional discipline. Relative to the consistency of ZF. Note also the direction that is not claimed: the library proves AC implies UL, and cites this result for the failure of the converse; it proves neither the converse nor its failure.