Strict relative placement of BPI between ZF and Choice

F1 directly gives a consistent extension of ZF in which BPI holds and AC fails. Therefore, under the given consistency hypothesis, ZF+BPI cannot prove AC.

In the theory supplied by F2, let $\mathcal{C}$ be the cofinite filter on $\omega$. Every finite intersection of cofinite sets is cofinite and nonempty, including the empty intersection $\omega$, so $\mathcal{C}$ is proper by F4. If BPI held, F3 would extend $\mathcal{C}$ to an ultrafilter $U$. No principal ultrafilter extends $\mathcal{C}$: the ultrafilter generated by $n$ contains $\{n\}$, whereas $\omega \setminus \{n\}\in \mathcal{C}$. Thus $U$ would be free, contradicting F2.

Hence the F2 theory proves $\mathrm{\neg }\mathrm{B}\mathrm{P}\mathrm{I}$, yielding the first displayed consistency implication. If ZF proved BPI, that consistent extension of ZF would satisfy BPI as well, contradicting step 1.2. Together with step 1.1 this proves both conditional strictness claims.