Relative consistency of BPI without Choice over ZF

A standard finite refutation $R$ of $\mathrm{Z}\mathrm{F}+\mathrm{B}\mathrm{P}\mathrm{I}+\mathrm{\neg }\mathrm{A}\mathrm{C}$ contains only finitely many ZF schema instances. Fix this particular $R$, and let $\mathrm{\Delta }$ consist of those instances together with $\mathrm{\neg }\mathrm{A}\mathrm{C}$; BPI is retained as its single displayed target sentence. This is an external extraction from one alleged finite proof, not a claimed uniform construction formalized in PA.

Since $\mathrm{\Delta }$ is now one externally fixed fragment, F2 gives one finite ZFC proof that the basic Cohen symmetric construction has a set interpretation satisfying $\mathrm{\Delta }$. Append the fixed set-theoretic proof F3 to the same finite construction, enlarging the finite source fragment for the finitely many forcing, cardinal, name-rank, and symmetry instances occurring in F3. The result is a finite ZFC proof that this set interpretation also satisfies BPI, hence a finite ZFC proof of a model of $\mathrm{\Delta }+\mathrm{B}\mathrm{P}\mathrm{I}$. No effective dependence of this proof on arbitrary input codes is used.

Relativize every line of the fixed refutation $R$ to that set interpretation and append the ordinary finite satisfaction induction for the finitely many formulas occurring in $R$. This gives a finite contradiction proof in ZFC. No countable-transitive-model inference is made.

F1 says the assumed consistency of ZF implies consistency of the ZFC+GCH source and therefore of ZFC, contradicting step 3.1. Hence no standard finite target refutation exists, which is exactly the displayed external relative-consistency implication. The resulting consistent extension contains BPI and $\mathrm{\neg }\mathrm{A}\mathrm{C}$, so, under the same antecedent, ZF+BPI cannot prove AC.