Choice and forcing boundary

The Boolean prime ideal principle is an assumption when invoked. The equivalences with arbitrary-language first-order compactness and compact Hausdorff product compactness are proved over ZF: each implication uses the principle on its own antecedent side. Those equivalences do not constitute a proof of BPI from ZF. AC implies BPI proves the separate implication from AC to BPI by extending proper filters with Zorn's lemma.

Choice-free regular open completion of forcing preorders constructs the regular-open completion of a set forcing preorder's separative quotient in ZF. It uses the downward-open topology on conditions, rather than an existence assertion for ultrafilters. Smaller conditions are stronger; compatibility requires a common stronger condition. A forcing filter is nonempty, upward closed and internally downward directed. The zero of the completion is omitted from its forcing order. These conventions do not identify an arbitrary preorder with a Boolean algebra or presuppose binary meets in the original preorder.

The relative nonimplication from BPI to AC is assigned to the later SET-21 development. No such nonimplication is proved or assumed here, and no result from the recorded catalogue supplies any of the arguments on this page. The empty Stone space and trivial Boolean algebra are allowed in the Boolean statements; the forcing statements explicitly concern nonempty preorders. The compact Hausdorff product theorem proves nonemptiness for nonempty factors under its BPI assumption, rather than presuming an arbitrary choice function.