Halpern–Läuchli and BPI Without Choice

Write $U_m=\mathrm{\forall }{a}_1\cdots \mathrm{\forall }{a}_m$, $X_m=\mathrm{\exists }{x}_1\cdots \mathrm{\exists }{x}_m$, $E_m=\mathrm{\exists }{A}_1\cdots \mathrm{\exists }{A}_m$, and $V_m=\mathrm{\forall }{x}_1\cdots \mathrm{\forall }{x}_m$. For $d>1$ there is a bridge $\mathrm{\forall }{a}_d{E}_{d-1}{V}_{d-1}\mathrm{\exists }{x}_d{⊢}_d\mathrm{\exists }{A}_d{U}_{d-1}{X}_{d-1}\mathrm{\forall }{x}_d$: Rule 3 moves $E_{d-1}$ left of $\mathrm{\forall }{a}_d$; Rule 1 rearranges the middle as $(\mathrm{\exists }{A}_i\mathrm{\forall }{x}_i{)}_{i=1}^{d-1}\mathrm{\forall }{a}_d\mathrm{\exists }{x}_d$; Rule 2 changes all $d$ matched pairs to $(\mathrm{\forall }{a}_i\mathrm{\exists }{x}_i{)}_{i=1}^{d-1}\mathrm{\exists }{A}_d\mathrm{\forall }{x}_d$; Rule 1 moves each earlier $\mathrm{\exists }{x}_i$ past later universal $a$-symbols and commutes the existential symbols to give $U_{d-1}\mathrm{\exists }{A}_d{X}_{d-1}\mathrm{\forall }{x}_d$; and Rule 3 moves $\mathrm{\exists }{A}_d$ left of $U_{d-1}$.

Derivations in $L_{d-1}$ lift through either outside matched pair: $W{⊢}_{d-1}{W}^{\mathrm{\prime }}$ implies both $\mathrm{\forall }{a}_{d}W\mathrm{\exists }{x}_d{⊢}_d\mathrm{\forall }{a}_d{W}^{\mathrm{\prime }}\mathrm{\exists }{x}_d$ and $\mathrm{\exists }{A}_{d}W\mathrm{\forall }{x}_d{⊢}_d\mathrm{\exists }{A}_d{W}^{\mathrm{\prime }}\mathrm{\forall }{x}_d$. It suffices to lift one rule step. Rules 1 and 2 apply unchanged inside the context. For Rule 3, Rule 1 first rearranges its adjacent prefix of $a$- and $A$-symbols into a universal block followed by an existential block, Rule 3 exchanges the blocks, and Rule 1 restores the required order. The outside coordinate remains a complete ordered pair; induction on the finite derivation length proves both implications.

If $d=1$, the asserted derivation is exactly $\mathrm{\forall }{a}_1\mathrm{\exists }{x}_1{⊢}_1\mathrm{\exists }{A}_1\mathrm{\forall }{x}_1$, an instance of Rule 2.

Suppose $d>1$ and the result holds in dimension $d-1$. Rule 1 gives $U_d{X}_d{⊢}_d\mathrm{\forall }{a}_d{U}_{d-1}{X}_{d-1}\mathrm{\exists }{x}_d$. Lift the induction hypothesis by the first implication in step 1.2, apply the bridge from step 1.1, and lift the induction hypothesis by the second implication in step 1.2; thus $\mathrm{\forall }{a}_d{U}_{d-1}{X}_{d-1}\mathrm{\exists }{x}_d{⊢}_d\mathrm{\forall }{a}_d{E}_{d-1}{V}_{d-1}\mathrm{\exists }{x}_d{⊢}_d\mathrm{\exists }{A}_d{U}_{d-1}{X}_{d-1}\mathrm{\forall }{x}_d{⊢}_d\mathrm{\exists }{A}_d{E}_{d-1}{V}_{d-1}\mathrm{\forall }{x}_d$. Rule 1 finally commutes the $A$-symbols and the $x$-symbols to obtain $E_d{V}_d$.

Every intermediate word lies in $L_d$: elementary commutation changes no coordinate's selected pair, Rule 2 replaces one legal ordered pair by the other, and Rule 3 is invoked only with its result in $L_d$. Steps 1.3 and 2.1 therefore prove the assertion for every positive $d$.

For $B_i\subseteq T_i$ and $n_i<\omega$, put ${\mathcal{C}}_i(n_i,B_i)=\{B_i\cap \{u:t{\le }_{T_i}u\}:t\in T_i(n_i)\}$. Interpret a word from left to right: $\mathrm{\exists }{A}_i$ means “there is $A_i\subseteq B_i$ that is $n_i$-dense”; $\mathrm{\forall }{x}_i$ ranges over $A_i$; $\mathrm{\forall }{a}_i$ ranges over ${\mathcal{C}}_i(n_i,B_i)$; and $\mathrm{\exists }{x}_i$ ranges over $a_i$. At the empty word assert $(x_1,\dots ,x_d)\in Q$. Let $W(\mathbf{n},\mathbf{B})$ be the resulting sentence, and let $\mathrm{\Phi }(W,\mathbf{n},p)$ say that $W(\mathbf{n},\mathbf{B})$ holds whenever every $B_i$ is $p$-dense.

If a subformula has $A_i$ only through a quantifier $\mathrm{\forall }{x}_i\in A_i$, replacing $A_i$ by $A_i^{\mathrm{\prime }}\subseteq A_i$ preserves its truth, because fewer values of $x_i$ must be checked. Repeating this argument proves simultaneous monotonicity in every such coordinate.

Rule 1 preserves the scheme: like quantifiers commute, and a witness for $\mathrm{\exists }\alpha \mathrm{\forall }\beta$ is independent of $\beta$ and therefore witnesses $\mathrm{\forall }\beta \mathrm{\exists }\alpha$. The side condition that the result lies in $L_d$ ensures that all variable domains in step 1.1 are already defined when used.

Rule 2 is pointwise valid. If $\mathrm{\forall }{a}_i\in {\mathcal{C}}_i(n_i,B_i)$ there is $x_i\in a_i$ satisfying the tail, choose one witness from each member of this one finite cone family and collect the witnesses as $A_i$; it lies in $B_i$, meets every height-$n_i$ cone, hence is $n_i$-dense, and the tail holds for all its members. Conversely, an $n_i$-dense $A_i\subseteq B_i$ meets every cone in ${\mathcal{C}}_i(n_i,B_i)$, so a member of the intersection supplies the matched existential. Finite induction supplies the finitely many witnesses and uses no choice axiom.

Consider Rule 3 with $1\le r<d$, after relabelling its permutation: $W=(\mathrm{\forall }{a}_i{)}_{i=1}^r(\mathrm{\exists }{A}_i{)}_{i=r+1}^{d}V$ and $W^{\mathrm{\prime }}=(\mathrm{\exists }{A}_i{)}_{i=r+1}^d(\mathrm{\forall }{a}_i{)}_{i=1}^{r}V$. Assume $\mathrm{\forall }\mathbf{k}\mathrm{\exists }p\mathrm{\Phi }(W,\mathbf{k},p)$. Because a $p^{\mathrm{\prime }}$-dense set is $p$-dense when $p^{\mathrm{\prime }}\ge p$, let $F(\mathbf{k})$ be the least witness exceeding every $k_i$. For fixed $\mathbf{n}$, define $G(0)={\max }_{i>r}{n}_i$ and $G(j+1)=F(n_1,\dots ,n_r,G(j),\dots ,G(j))$. This uses least natural witnesses and recursion on $\omega$, not a choice function.

Put $m={\prod }_{i=1}^r\mathrm{\mid }{T}_i(n_i)\mathrm{\mid }$ and $p_j=G(m-j)$ for $0\le j\le m$. Given $p_0$-dense $B_i$, enumerate the $m$ tuples of height-$n_i$ roots in the first $r$ trees; their associated cone tuples may repeat. Before any tuple is processed, take $A_i^0=B_i$ for $i>r$. These sets are $p_0$-dense and the preservation requirement for the empty list is vacuous.

Suppose $j<m$ cone tuples have been processed and $A_i^j\subseteq B_i$ is $p_j$-dense for every $i>r$, with the tail $V$ true for all earlier tuples. Apply $\mathrm{\Phi }(W,(n_1,\dots ,n_r,p_{j+1},\dots ,p_{j+1}),p_j)$ to the next cone tuple and to $B_1,\dots ,B_r,A_{r+1}^j,\dots ,A_d^j$. It yields $A_i^{j+1}\subseteq A_i^j$ that are $p_{j+1}$-dense and make $V$ true for the new tuple. Step 2.1 preserves all earlier instances. Finite induction gives final sets $A_i^m$ working for all cone tuples.

Since $p_m=G(0)\ge n_i$ for $i>r$, each $A_i^m$ is $n_i$-dense: extend any height-$n_i$ node to height $p_m$ and use $p_m$-density. Hence the $A_i^m$ witness the leading existential block of $W^{\mathrm{\prime }}$, and the universal block holds because step 4.1 processed every root tuple. Therefore $\mathrm{\Phi }(W^{\mathrm{\prime }},\mathbf{n},p_0)$ holds. The vector $\mathbf{n}$ was arbitrary, proving Rule 3 preserves the quantified scheme.

A derivation is finite. Apply steps 2.2, 2.3, or 5.1 successively to its rule steps; transitivity gives the displayed implication for $W{⊢}_d{W}^{\mathrm{\prime }}$.

Let $W_0=\mathrm{\forall }{a}_1\cdots \mathrm{\forall }{a}_d\mathrm{\exists }{x}_1\cdots \mathrm{\exists }{x}_d$ and $W_1=\mathrm{\exists }{A}_1\cdots \mathrm{\exists }{A}_d\mathrm{\forall }{x}_1\cdots \mathrm{\forall }{x}_d$. By classical logic, the scheme $S(W_0):=\mathrm{\forall }\mathbf{n}\mathrm{\exists }p\mathrm{\Phi }(W_0,\mathbf{n},p)$ either holds or fails.

Assume first that $S(W_0)$ holds. By F2 and F3, $S(W_1)$ holds. Fix $k$, take $\mathbf{n}=(k,\dots ,k)$, and obtain a corresponding $p$.

Assume instead that $S(W_0)$ fails. Then some vector $\mathbf{n}$ satisfies: for every $p$ there are $p$-dense $B_i$ for which $W_0(\mathbf{n},\mathbf{B})$ is false. Unwinding the negated endpoint word gives roots $t_i\in T_i(n_i)$ whose cones $a_i=B_i\cap \{u:t_i{\le }_{T_i}u\}$ satisfy ${\prod }_i{a}_i\subseteq {\prod }_i{T}_i\setminus Q$.

Apply $\mathrm{\Phi }(W_1,\mathbf{n},p)$ from step 2.1 with $B_i=T_i$, which is $p$-dense because it contains every node. The interpretation supplies $k$-dense $A_i\subseteq T_i$ such that every tuple in ${\prod }_i{A}_i$ lies in $Q$. Hence $Q$ contains a $k$-matrix; since $k$ was arbitrary, alternative 1 holds.

Put $h={\max }_i{n}_i$ for the vector from step 2.2 and fix $k<\omega$. Take $p=h+k$, extend each of the finitely many $t_i$ to a node $s_i\in T_i(h)$, and put $C_i=a_i\cap \{u:s_i{\le }_{T_i}u\}$. Every height-$(h+k)$ extension of $s_i$ is dominated by $B_i$, and its dominating member belongs to $C_i$; hence $C_i$ is $(h,k)$-dense. Also ${\prod }_i{C}_i\subseteq {\prod }_i{a}_i$ lies in the complement of $Q$. Thus alternative 2 holds for this single $h$ and every $k$, including $k=0$.

The two cases in step 1.1 are exhaustive, and steps 3.1 and 3.2 prove the respective alternatives. No infinite choice was used: only finitely many cone roots were extended in step 3.2.

Induct on $q$. For $q=1$, take $n=2$: the sole color contains ${\prod }_i{T}_i(1)$, a $(0,1)$-matrix inside the truncation.

Assume the assertion for $q$, with witness $k>0$, and suppose for contradiction that the truncation assertion fails for $q+1$. For every $n>0$ there is then a bad $(q+1)$-coloring of ${\prod }_i(T_i\upharpoonright n)$, meaning one with no monochromatic $(h,1)$-matrix for $h<n$.

Order all bad finite colorings by restriction. A restriction is still bad, each level is finite because its coloring domain is finite, and step 1.2 gives a node at every positive level; adjoining the empty coloring as root makes a height-$\omega$ finite-level tree.

Apply F3 using A1. Its branch is a coherent sequence of bad colorings, whose union is a $(q+1)$-coloring $c$ of the full product: every tuple belongs to a sufficiently high finite truncation, and coherence makes its color independent of that choice.

Let $Q$ be the union of the first $q$ color classes of $c$. Apply F2. Either the last color contains an $(h,1)$-matrix, or $Q$ contains a $k$-matrix for the induction witness $k$.

In the first case, thin each coordinate of the $(h,1)$-matrix to finitely many nodes, one dominating witness for each member of the finite height-$(h+1)$ cone frontier. The finite product is still monochromatic and is contained in some truncation, contradicting that branch node's badness.

In the second case write the $k$-matrix as ${\prod }_i{A}_i\subseteq Q$. Since $A_i$ dominates $T_i(k)$ and $T_i(k)$ dominates $T_i\upharpoonright k$, choose on the finite truncation a map $f_i(x)\in A_i$ with $x\le f_i(x)$. Pull the $q$ colors on $Q$ back along ${\prod }_i{f}_i$. The induction hypothesis gives a monochromatic $(h,1)$-matrix in the truncated domain; its coordinatewise image is still $(h,1)$-dense and lies in one of the first $q$ colors. After finite thinning it lies in some branch truncation, again contradicting badness.

Both dichotomy cases contradict step 1.2. Hence a truncation witness exists for $q+1$, and induction proves the first assertion for every positive $q$. AC entered only at step 3.1; all selections in steps 5.1–5.2 are ZF and finite.

For the terminal form, fix the truncation witness $n$ and a coloring of ${\prod }_i{T}_i(n)$. On each finite $T_i\upharpoonright n$, select an extension map $g_i(x)\in T_i(n)$ with $x\le g_i(x)$ and pull the coloring back along ${\prod }_i{g}_i$. A monochromatic $(h,1)$-matrix from the first assertion maps coordinatewise to an $(h,1)$-matrix in ${\prod }_i{T}_i(n)$ of the original color.

The finitely many atoms of $A$ have join $1$. At least one has $e$-value $1$, since $e(1)=1$; at most one does, since distinct atoms have meet $0$ whereas two value-$1$ atoms would have meet of value $1$. Let $a$ be this unique atom.

The atoms of $C$ below $a$ have join $a$: intersect the atomic decomposition of $1_C$ with $a$. Because $a\mathrm{\ne }0$, at least one such $C$-atom $c$ is nonzero. This chooses one element from one finite nonempty set, not a choice function on a family.

Define $e^{\mathrm{\prime }}(x)=1$ exactly when $c\le x$. Since $c$ is an atom, it lies below exactly one of $x,\mathrm{\neg }x$, and $c\le x\wedge y$ exactly when both $c\le x$ and $c\le y$; hence $e^{\mathrm{\prime }}$ preserves $0,1,\mathrm{\neg },\wedge$, and therefore $\vee$. Thus $e^{\mathrm{\prime }}:C\to \mathbf{2}$ is a Boolean homomorphism.

For $x\in A$, the selected $A$-atom $a$ lies below exactly one of $x,\mathrm{\neg }x$, and $c\le a$. If $e(x)=1$, uniqueness in step 1.1 forces $a\le x$, hence $e^{\mathrm{\prime }}(x)=1$; if $e(x)=0$, then $e(\mathrm{\neg }x)=1$, so $a\le \mathrm{\neg }x$ and $e^{\mathrm{\prime }}(x)=0$. Therefore $e^{\mathrm{\prime }}\mathrm{\mid }A=e$.

Given a finite $F\subseteq B$, take $C=⟨A\cup F⟩$. The cell description makes $C$ finite, step 4.1 extends the original diagram to $C$, and its domain contains $F$; this is precisely extension across $F$. It is not called a diagram deciding $F$, because the preceding definition reserves that phrase for a diagram whose domain is exactly $⟨F⟩$.

Let $B_n=⟨b(0),\dots ,b(n-1)⟩$ and let level $n$ consist of all homomorphisms $e:B_n\to \mathbf{2}$, ordered by restriction. Each level is finite: $e$ is determined by the bit string $(e(b(0)),\dots ,e(b(n-1)))$, even when the enumeration repeats elements.

Level $0$ has the unique homomorphism on $\{0,1\}$ because $B$ is nontrivial. By F2 every level-$n$ node extends to level $n+1$, so finite induction makes every level nonempty.

Diagram compactness implies the prime-ideal assertion as follows. For the supplied enumeration of $B$, use variables $y_n$ and enumerate the requirements $y_i=0$ when $b(i)=0$, $y_i=1$ when $b(i)=1$, and $y_i=\mathrm{\neg }{y}_j$, $y_i=y_j\wedge y_k$, or $y_i=y_j\vee y_k$ whenever the corresponding equality holds in $B$, including $y_i=y_j$ for repeated enumerates. Every finite set of requirements is satisfied by a homomorphism on the finite subalgebra generated by its finitely many mentioned elements, using F2. A total solution induces a well-defined homomorphism $B\to \mathbf{2}$, whose zero fibre is prime by F1.

Call a node good if it has extensions at arbitrarily high levels. The level-$0$ node is good by step 2.1. A good node has at least one good immediate successor: its possible successors have bit $0$ or $1$, and if both existing successors had finite extension bounds, their maximum would bound the parent. Recursively take the bit-$0$ good successor when it exists and otherwise the bit-$1$ good successor. This definable binary preference produces a coherent branch $(e_n)$ in ZF, without applying choice or general König's lemma.

For $x\in B$, define $e(x)$ to be the unique value $e_n(x)$ occurring once $x\in B_n$; surjectivity supplies such an $n$ and coherence makes the value independent of $n$ and of repetitions in $b$. Every finite Boolean calculation occurs in some $B_n$, where $e_n$ preserves it, so $e:B\to \mathbf{2}$ is a total homomorphism.

The set $I=e^{-1}(0)$ contains $0$, omits $1$, is downward closed and join-closed, and $x\wedge y\in I$ implies $e(x)e(y)=0$, hence $x\in I$ or $y\in I$. Thus $I$ is a proper prime ideal.

The prime-ideal assertion implies diagram compactness. For an enumerated finitely satisfiable diagram $\mathrm{\Gamma }$, let $F$ be the countable free Boolean algebra of finite terms in its variables and let $J$ be the ideal generated by $p$ for every requirement $p=0$ and by $\mathrm{\neg }p$ for every requirement $p=1$. The ideal is proper: an equation $1\le g_1\vee \cdots \vee g_m$ with generators $g_j$ would be contradicted by a two-valued valuation satisfying their finitely many requirements. Hence $F\mathrm{/}J$ is a nontrivial enumerated Boolean algebra. A prime ideal of $F\mathrm{/}J$ gives a homomorphism to $\mathbf{2}$ by value $0$ on the ideal and $1$ on its complement; composed with the variables, it satisfies every requirement in $\mathrm{\Gamma }$.

Steps 5.1, 6.1, and 2.2 prove the prime-ideal claim and both directions of the stated equivalence in ZF. The only infinite recursion, step 3.1, uses a fixed preference between two bits; all other witness collections occur over a single finite set.

Assume BPI and let $\mathcal{F}$ be a proper filter on a set $S$; if $S=\mathrm{\varnothing }$ there is no such filter. Put $I_{\mathcal{F}}=\{S\setminus A:A\in \mathcal{F}\}$. Filter closure makes this an ideal of $\mathcal{P}(S)$, and it is proper because $S\in I_{\mathcal{F}}$ would mean $\mathrm{\varnothing }\in \mathcal{F}$. Thus the quotient $\mathcal{P}(S)\mathrm{/}{I}_{\mathcal{F}}$ is a nontrivial Boolean algebra.

Conversely assume UFL, and let $B$ be a nontrivial Boolean algebra. Let $X$ be the set of all homomorphisms $p:A_p\to \mathbf{2}$ whose domains are finite Boolean subalgebras of $B$, and put $D_b=\{p\in X:b\in A_p\}$. The set $X$ is nonempty, and every finite intersection $D_{b_1}\cap \cdots \cap D_{b_m}$ is nonempty: apply F4 from the unique map on $\{0,1\}$ to the subalgebra generated by the listed elements.

By BPI choose a prime ideal $P$ of the quotient from step 1.1, and let $J=\{A\subseteq S:[A{]}_{I_{\mathcal{F}}}\in P\}$. The quotient map shows that $J$ is a prime ideal of $\mathcal{P}(S)$ containing $I_{\mathcal{F}}$.

The finite-intersection property from step 1.2 makes the supersets of finite intersections of the $D_b$ a proper filter $\mathcal{G}$ on $X$. By UFL extend it to an ultrafilter $\mathcal{V}$. For each $b$, the two disjoint sets $D_{b,0}=\{p\in D_b:p(b)=0\}$ and $D_{b,1}=\{p\in D_b:p(b)=1\}$ partition $D_b\in \mathcal{V}$, so exactly one lies in $\mathcal{V}$.

Define $\mathcal{U}=\{A\subseteq S:S\setminus A\in J\}$. It is a proper filter, contains $\mathcal{F}$, and decides every $A\subseteq S$: primality applied to $A\cap (S\setminus A)=\mathrm{\varnothing }\in J$ puts $A$ or its complement in $J$, while properness prevents both. Any proper filter strictly extending $\mathcal{U}$ would contain some $A\mathrm{\notin }\mathcal{U}$ as well as $S\setminus A\in \mathcal{U}$, hence $\mathrm{\varnothing }$; therefore $\mathcal{U}$ is maximal and is an ultrafilter.

Define $h(b)=i$ when $D_{b,i}\in \mathcal{V}$. For any finite Boolean equation among elements of $B$, the intersection of their deciding sets lies in $\mathcal{V}$ and every partial homomorphism in it obeys that equation. If the selected bits violated it, intersecting the corresponding value cells would give the empty set in $\mathcal{V}$. Hence $h$ preserves $0,1,\mathrm{\neg },\wedge ,\vee$ and is a homomorphism $B\to \mathbf{2}$.

Its zero fibre $h^{-1}(0)$ is a proper ideal, and $h(a\wedge b)=h(a)h(b)=0$ implies one factor is zero, so the ideal is prime. Thus UFL implies BPI.

Steps 1.1–3.1 prove BPI implies UFL, and steps 1.2, 2.2, 3.2, and 4.1 prove UFL implies BPI, all in ZF. The empty-set UFL instance is vacuous and the trivial Boolean algebra is excluded exactly as in F1.

F1 is already a theorem of ZF: its word calculus, finite thinning, and common-height cone repair use only finite coded selections. This proves the Halpern--Läuchli clause without AC.

Under the separate construction hypotheses, F2 supplies a transitive symmetric model satisfying ZF, BPI, and failure of AC. Its BPI proof works with finite supports and forcing-name orbits, so no identification with a parameter-HOD presentation is needed.

Steps 1.1 and 1.2 prove the two assertions and keep their axiom bases distinct. The empty family of trees is excluded by F1's positive-dimension hypothesis, while the model clause treats every nontrivial Boolean algebra through BPI.

Suppose the displayed target were inconsistent and fix a standard finite refutation. It uses only finitely many displayed HL instances, or one use of the uniformly quantified F2 theorem after its standard coding. Replace each such occurrence by the corresponding fixed finite ZF derivation from F2. This is an external transformation of the alleged finite refutation; no arithmetized uniform proof transformer is needed.

The result is a refutation of $\mathrm{Z}\mathrm{F}+\mathrm{B}\mathrm{P}\mathrm{I}+\mathrm{\neg }\mathrm{A}\mathrm{C}$, contradicting F1 under the given consistency hypothesis. Hence the target is consistent whenever ZF is.

If BPI+HL implied AC over ZF, the target theory would prove both AC and its negation, contrary to step 2.1. This gives the stated conditional nonimplication without asserting any theory's consistency outright.

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.