Boolean Algebras, Stone Duality, and the Prime Ideal Theorem

For $a,b,c\in B$, split $a\wedge \mathrm{\neg }c$ by $b\vee \mathrm{\neg }b=1$. Its two pieces lie respectively below $b\wedge \mathrm{\neg }c$ and $a\wedge \mathrm{\neg }b$. Split $c\wedge \mathrm{\neg }a$ the same way. Joining these four inequalities gives $a\mathrm{△}c\le (a\mathrm{△}b)\vee (b\mathrm{△}c)$. Also $a\mathrm{△}a=0$ and $a\mathrm{△}b=b\mathrm{△}a$. Since an ideal contains $0$, is downward closed and is closed under joins, these identities prove reflexivity, symmetry and transitivity of ${\sim }_I$.

For $a,b,c,d\in B$, expand $(a\wedge c)\wedge \mathrm{\neg }(b\wedge d)$ using $\mathrm{\neg }(b\wedge d)=\mathrm{\neg }b\vee \mathrm{\neg }d$. The resulting pieces lie below $a\wedge \mathrm{\neg }b$ and $c\wedge \mathrm{\neg }d$. The reverse difference has pieces below $b\wedge \mathrm{\neg }a$ and $d\wedge \mathrm{\neg }c$. Hence $(a\wedge c)\mathrm{△}(b\wedge d)\le (a\mathrm{△}b)\vee (c\mathrm{△}d)$. Moreover $(\mathrm{\neg }a)\mathrm{△}(\mathrm{\neg }b)=a\mathrm{△}b$. Thus equivalent inputs give equivalent meets and complements; the identity $a\vee c=\mathrm{\neg }(\mathrm{\neg }a\wedge \mathrm{\neg }c)$ gives the same for joins.

Steps 1.1 and 1.2 make every proposed operation a function on classes. Each Boolean identity in the quotient is the class of that identity in $B$, so the quotient is Boolean. The map $q$ preserves each operation by its definition and is onto because every class has the form $[a]$. Finally $[a]=[0]$ if and only if $a\mathrm{△}0=a\in I$, proving the kernel assertion. If $I=B$, every pair is equivalent and the quotient has one element.

Let $h$ be as in the statement. If $a{\sim }_{I}b$, preservation of the operations gives $h(a)\mathrm{△}h(b)=h(a\mathrm{△}b)=0$. For any Boolean elements $u,v$, $u\mathrm{△}v=0$ implies $u\wedge \mathrm{\neg }v=v\wedge \mathrm{\neg }u=0$, hence $u\le v\le u$ and $u=v$. Therefore $\bar{h}([a])=h(a)$ is well defined. Substituting this formula into each quotient operation proves preservation of both bounds, meet, join and complement, and $\bar{h}q=h$. Any factorization must take $[a]$ to $h(a)$ because $q$ is onto, proving uniqueness without a choice of representatives. QED.

The displayed set contains $1$ using $n=0$, contains each $s\in S$ using $n=1$, and is upward closed. Concatenating two finite lists witnessing membership of $b,c$ gives a finite meet below $b\wedge c$, so it is a filter. Any filter containing $S$ contains each finite meet, including $1$, and therefore every element of the displayed set. This proves minimality, including $⟨\mathrm{\varnothing }⟩=\{1\}$.

Suppose $U$ is maximal proper and $b\mathrm{\notin }U$. Then $⟨U\cup \{b\}⟩$ is improper. Step 1.1 gives $u\wedge b=0$ for some $u\in U$, combining all old factors into $u$, with $u=1$ if there are none. Consequently $u\le \mathrm{\neg }b$, so $\mathrm{\neg }b\in U$. A proper filter cannot contain both $b$ and $\mathrm{\neg }b$, since their meet is $0$. Conversely, if $U$ decides every complementary pair, any larger filter contains some $b\mathrm{\notin }U$ together with $\mathrm{\neg }b\in U$ and is improper.

A prime filter decides complementary pairs because $1=b\vee \mathrm{\neg }b\in U$. Conversely, if a proper filter decides pairs and neither $b$ nor $c$ belongs to it, both complements do, so $\mathrm{\neg }(b\vee c)=\mathrm{\neg }b\wedge \mathrm{\neg }c$ belongs to it; thus $b\vee c\mathrm{\notin }U$. This proves primality from pair decision.

Filter closure and upward closure give $b\wedge c\in U$ exactly when both $b,c\in U$; primality gives $b\vee c\in U$ exactly when at least one belongs to $U$. Pair decision gives ${\chi }_U(\mathrm{\neg }b)=1-{\chi }_U(b)$, and properness gives ${\chi }_U(0)=0$, ${\chi }_U(1)=1$. These are precisely all homomorphism identities into $2$. Conversely a bound-preserving homomorphism indicator satisfies the complementary-pair identity, giving pair decision.

The operation $F\mapsto \{\mathrm{\neg }f:f\in F\}$ is an inclusion-preserving bijection from filters to ideals: complementation reverses inequalities, sends meets to joins, and exchanges $1$ with $0$; applying it twice returns $F$. It preserves properness and maximality. For a pair-deciding $U$ its image is $B\setminus U$. This complement is prime because $a\wedge b\mathrm{\notin }U$ implies at least one of $a,b$ is not in $U$. Conversely, for a prime ideal $I$, primality applied to $b\wedge \mathrm{\neg }b=0$ and properness give exactly one of $b,\mathrm{\neg }b$ in $I$. Its complement is consequently a pair-deciding filter, hence an ultrafilter. Maximal ideals correspond to maximal filters by the bijection, completing both assertions. The trivial algebra has no proper filters or ideals, so those quantified assertions are vacuous there. QED.

For $b\mathrm{\ne }0$, the finite nonempty set $\{c:0<c\le b\}$ has a minimal member: a strict descending sequence cannot have more distinct terms than this finite set. Such a minimal member is an atom. If atoms $a,d$ have nonzero meet, minimality gives $a\wedge d=a=d$. Thus distinct atoms are disjoint.

Put $s=\bigvee \{a\in A:a\le b\}$. This finite join is at most $b$. If $b\wedge \mathrm{\neg }s\mathrm{\ne }0$, step 1.1 gives an atom $d\le b\wedge \mathrm{\neg }s$. Then $d\le b$ puts $d\le s$, contradicting $d\le \mathrm{\neg }s$ and $d\mathrm{\ne }0$. Hence $b=s$.

Write $\varphi (b)=\{a\in A:a\le b\}$. Meets correspond to intersections by the definition of lower bound. For an atom $a$, the equation $a=(a\wedge b)\vee (a\wedge \mathrm{\neg }b)$ implies exactly one of $a\le b$ and $a\le \mathrm{\neg }b$, since each piece is $0$ or $a$. Therefore complements correspond to set complements, and joins correspond to unions by De Morgan's law; bounds correspond to $\mathrm{\varnothing },A$. Step 2.1 proves injectivity. For $T\subseteq A$, distinct-atom disjointness gives $\varphi (\bigvee T)=T$: an atom outside $T$ meets that finite join in $0$. This proves surjectivity. If $B$ is trivial, $A=\mathrm{\varnothing }$ and both algebras have one element.

For an ultrafilter $U$, finiteness makes $a=\bigwedge U$ a member of $U$, so $a\mathrm{\ne }0$ and $U=\{b:a\le b\}$. If $0<c<a$, then $c\mathrm{\notin }U$, so F2 gives $\mathrm{\neg }c\in U$ and $a\le \mathrm{\neg }c$, contradicting $0<c\le a$. Hence $a$ is an atom. Conversely the upward filter generated by an atom is proper and decides every pair by step 3.1, so F2 makes it an ultrafilter. Two atoms generating the same filter each lie above the other and are equal. QED.

Let $I$ be a proper ideal of $B$. By F2 its quotient map $q:B\to B\mathrm{/}I$ has kernel $I$, so $q(1)\mathrm{\ne }q(0)$ because $1\mathrm{\notin }I$. BPI therefore provides a prime ideal $J$ in $B\mathrm{/}I$. The inverse image $q^{-1}(J)$ contains $I$, is downward and join closed by monotonicity and join preservation, contains $0$ and excludes $1$. If $a\wedge b$ is in it, then $q(a)\wedge q(b)\in J$, so primality of $J$ gives $a$ or $b$ in the inverse image. This proves prime extension.

For a proper filter $F$, let $I=\{\mathrm{\neg }f:f\in F\}$, a proper ideal by F3. Step 1.1 gives a prime ideal $J\supseteq I$. The ultrafilter $U=B\setminus J$ contains $F$: for $f\in F$, $\mathrm{\neg }f\in J$ precludes $f\in J$ because $J$ is proper. Thus BPI also gives filter extension.

Conversely, if prime extension holds, apply it to the proper ideal $\{0\}$ of any nontrivial $B$ to get BPI. If filter extension holds instead, apply it to the proper filter $\{1\}$ and use F3 to take the complement of the resulting ultrafilter. Trivial algebras have neither proper ideals nor proper filters and are excluded by F1. No infinite family of choices is made in any implication. QED.

Assume BPI. A proper set filter on $S$ is exactly a proper Boolean filter in $\mathcal{P}(S)$: meets are intersections, the unit is $S$ and zero is $\mathrm{\varnothing }$. Its maximal proper Boolean extension supplied by F1 is therefore a set ultrafilter by F3. This also covers all possible instances when $S=\mathrm{\varnothing }$, since then no proper filter exists.

Assume UFL and fix a proper Boolean filter $F$ in $B$. Let $E$ be the set of pairs $(C,h)$ with $C\subseteq B$ a finite Boolean subalgebra and $h:C\to 2$ a Boolean homomorphism. Every finite subset $K$ of $B$ is contained in a finite subalgebra: enumerate $K$ as $b_1,\dots ,b_n$, form the at most $2^n$ meets choosing $b_i$ or $\mathrm{\neg }{b}_i$, and take all joins of these cells. Distributivity partitions $1$ into those cells; their joins are closed under all Boolean operations and contain $K$. No simultaneous enumeration of all finite subsets is required.

On $E$ impose requirements $D_b=\{(C,h):b\in C\}$ for $b\in B$ and $T_f=\{(C,h):f\in C,h(f)=1\}$ for $f\in F$. A finite list of requirements mentions finitely many $b$ and $f$. Choose a finite subalgebra containing them by step 1.2. Their filter meet $u$ is nonzero, including $u=1$ if no $f$ occurs. F2 supplies an atom $a\le u$ in that subalgebra. The character $h(c)=1$ exactly when $a\le c$ meets all listed requirements. This proves FIP, including nonemptiness of $E$ for the empty list. By F4 these sets generate a proper set filter; UFL gives an ultrafilter $W$ containing it.

A set ultrafilter $W$ decides every subset $H\subseteq E$: if $H\mathrm{\notin }W$, adjoining it makes an improper filter by maximality, so a finite intersection from $W$ is disjoint from $H$, putting $E\setminus H$ in $W$. Both cannot belong to $W$. For each $b$, the two disjoint fibres $D_{b,i}=\{(C,h):b\in C,h(b)=i\}$ partition the $W$-large set $D_b$. Exactly one fibre is in $W$ by this decision property. Define $v(b)$ to be its unique label.

Intersect the large fibres for $b,c,b\wedge c$ and their domains. Their intersection is nonempty by properness. At any pair $(C,h)$ in it, $v(b\wedge c)=h(b\wedge c)=h(b)\wedge h(c)=v(b)\wedge v(c)$. The same argument with $b,c,b\vee c$ proves join preservation; with $b,\mathrm{\neg }b$ it proves complement preservation. Since every local character takes $0$ to $0$ and $1$ to $1$, so does $v$. The requirements $T_f$ force $v(f)=1$ for all $f\in F$.

The set $U=v^{-1}(\{1\})$ is a proper Boolean filter containing $F$, by the identities in step 4.1. It decides complementary pairs. Any larger filter would contain some $b$ with $v(b)=0$ and also $\mathrm{\neg }b\in U$, hence contain zero; thus $U$ is maximal proper. F1 now gives BPI. Properness of $F$ excludes the trivial algebra; the finitely many witness selections above are valid in ZF, and the labels in step 3.1 are unique. QED.

Let $P$ consist of the proper filters $G\supseteq F$, ordered by inclusion. This is a set of subsets of $B$ and inclusion is reflexive, antisymmetric and transitive. It is nonempty because $F\in P$. The empty chain has upper bound $F$.

For a nonempty chain $\mathcal{C}\subseteq P$, put $G=\bigcup \mathcal{C}$. It contains $F$ and $1$ and excludes $0$. If $a\in G$ and $a\le b$, a member containing $a$ also contains $b$. If $a,b\in G$, two chain members witnessing this are comparable, so one contains both and their meet. Thus $G\in P$ and bounds the chain.

Apply F2, with AC supplied by F1 and its poset hypotheses checked in steps 1.1 and 2.1, to obtain a maximal $U\in P$. Every proper filter extending $U$ also extends $F$ and belongs to $P$, so maximality in $P$ is maximal properness in $B$. This application of Zorn is the use of AC.

For a nontrivial $B$, start with the proper filter $\{1\}$; step 3.1 gives an ultrafilter whose complement is a prime ideal by F3. This is BPI by F4. For the trivial algebra there is no proper initial filter and BPI makes no existence demand. QED.

If $b\le ̸c$, the element $d=b\wedge \mathrm{\neg }c$ is nonzero, and $\{a:d\le a\}$ is a proper filter. F2 extends it to $U$ with $b\in U$ and $c\mathrm{\notin }U$, since otherwise $d\wedge c=0$ would belong to $U$. Thus $[b]\subseteq ̸[c]$. Together with the Boolean identities in F1, this shows that $b\mapsto [b]$ is an injective Boolean homomorphism, reflecting order.

If $U,V$ are distinct ultrafilters, some $b$ belongs to exactly one; the other contains $\mathrm{\neg }b$. The disjoint open sets $[b]$ and $[\mathrm{\neg }b]$ separate them, so $X$ is Hausdorff.

Consider a cover $\{[b]:b\in H\}$ with no finite subcover. No finite join from $H$ is $1$, since F1 would make those finitely many clopens cover $X$. Hence every finite meet from $\{\mathrm{\neg }b:b\in H\}$ is nonzero, including the empty meet (otherwise $B$ is trivial and the empty subcover suffices). Their upward closure is a proper filter: concatenation of finite lists gives meet closure, and no witness meet is zero. F2 extends it to an ultrafilter $U$. For every $b\in H$, $\mathrm{\neg }b\in U$ forces $U\mathrm{\notin }[b]$, contradicting the cover. Thus every basic cover has a finite subcover.

Given an arbitrary open cover $\mathcal{O}$, let $H$ consist of all $b$ such that $[b]\subseteq O$ for some $O\in \mathcal{O}$. The basis property in F1 makes these sets a cover; step 1.3 gives finitely many covering basic sets. For each of this finite list take one containing member of $\mathcal{O}$. These form a finite subcover, proving compactness with only finite choice.

For a clopen $K\subseteq X$, all basic clopens contained in $K$, together with the open set $X\setminus K$, cover $X$. Step 2.1 supplies a finite subcover; intersecting its union with $K$ gives $K=[b_1]\cup \cdots \cup [b_n]=[b_1\vee \cdots \vee b_n]$. If the finite list is empty, $K=\mathrm{\varnothing }=[0]$. Hence the embedding in step 1.1 is onto all clopens. If $B$ is trivial, $X=\mathrm{\varnothing }$ and both algebras have one element; the same identities and compactness conclusion hold. QED.

For $x\in X$, the clopens containing $x$ include $X$, exclude $\mathrm{\varnothing }$, are upward and intersection closed, and decide each pair $C,X\setminus C$. By F2 this is an ultrafilter, so ${\eta }_X$ is defined. If $x\mathrm{\ne }y$, Hausdorffness gives an open neighborhood of $x$ avoiding $y$, and the clopen basis gives a clopen $C$ containing $x$ but not $y$. Thus ${\eta }_X(x)\mathrm{\ne }{\eta }_X(y)$.

Let $U$ be an ultrafilter of clopens. Its finite intersections are members of $U$ and are nonempty, so its closed sets have FIP, including the empty intersection $X$. F3 supplies $x\in \bigcap U$. If a clopen $C$ containing $x$ were absent from $U$, F2 would put $X\setminus C$ in $U$, contrary to the choice of $x$. Hence $U={\eta }_X(x)$. This point is unique by step 1.1.

For each clopen $C$, the definitions give ${\eta }_X^{-1}([C])=C$. Thus ${\eta }_X$ is continuous on the basic opens, hence on their unions. Surjectivity in step 2.1 gives ${\eta }_X[C]=[C]$ as well. Every open set of $X$ is a union of clopens, so its image is a union of basic open sets; the inverse of the bijection is continuous. If $X=\mathrm{\varnothing }$, its clopen algebra is trivial, its ultrafilter space is empty, and the empty map is the asserted homeomorphism. The inverse is defined by the unique common point, without choice. QED.

If $V$ is an ultrafilter of $C$, its inverse image under $h$ contains $1$, excludes $0$, and is upward and meet closed by F3. It decides complements because $h(\mathrm{\neg }b)=\mathrm{\neg }h(b)$ and $V$ decides complements. Such a proper filter is maximal: adjoining a missing $b$ includes both it and its complement. Thus $h^{\ast }(V)$ is an ultrafilter. For each $b$, $(h^{\ast }{)}^{-1}([b])=[h(b)]$, since $b\in h^{-1}[V]$ exactly when $h(b)\in V$. Hence $h^{\ast }$ is continuous. Equivalently its character is ${\chi }_V\circ h$, with this order of composition.

The inverse image of a clopen $D\subseteq Y$ is open by continuity of $f$ and closed because its complement is the inverse image of the open complement of $D$. Preimages preserve intersections, unions, complements and the empty and whole sets. Thus $f^{\ast }$ is a Boolean homomorphism.

For composable maps $h:B\to C$ and $k:C\to D$, $(k\circ h{)}^{-1}[V]=h^{-1}[k^{-1}[V]]$, so $(k\circ h{)}^{\ast }=h^{\ast }\circ k^{\ast }$. The identical preimage computation proves the composition law for continuous maps, and the identity map has identity preimage on every subset. Thus both assignments are contravariant functors on the stated objects.

For $b\in B$, the identity of step 1.1 says $(h^{\ast }{)}^{\ast }({ϵ}_B(b))=[h(b)]={ϵ}_C(h(b))$. For $x\in X$ and a clopen $D\subseteq Y$, membership of $D$ in $(f^{\ast }{)}^{\ast }({\eta }_X(x))$ means $x\in f^{-1}[D]$, equivalently $f(x)\in D$; hence $(f^{\ast }{)}^{\ast }{\eta }_X={\eta }_{Y}f$. These are the two naturality equations, and F1 and F2 make their components isomorphisms. The formulas also apply to empty Stone spaces and trivial algebras whenever the indicated maps exist, since bound preservation is required throughout. QED.

Assume BPI and finite satisfiability of $T$. The set $2^P$ is nonempty, with the constant-zero valuation as an explicit member. The subsets whose membership depends on finitely many coordinates form a Boolean algebra $A$: a union or intersection of two such sets depends on the union of their finite supports, and complement has the same support. The truth set $\mathrm{⟦}\varphi \mathrm{⟧}$ of any finite formula is in $A$, by recursion on its connectives. Finite satisfiability says every finite intersection of the truth sets of members of $T$ is nonempty. Their finite intersections and upward closure therefore form a proper Boolean filter in $A$, including $2^P$ from the empty intersection.

Separately, assume propositional compactness and take a nontrivial Boolean algebra $B$. Use letters $p_b$ for $b\in B$ and the theory consisting of $p_1$, $\mathrm{\neg }{p}_0$, and all equations $p_{\mathrm{\neg }b}\leftrightarrow \mathrm{\neg }{p}_b$, $p_{b\wedge c}\leftrightarrow (p_b\wedge p_c)$ and $p_{b\vee c}\leftrightarrow (p_b\vee p_c)$. Any finite fragment names finitely many Boolean elements. As in finite distributive expansion, the joins of all cells obtained by choosing each named element or its complement form a finite subalgebra containing them. It is nontrivial because it contains distinct $0,1$. By F2 an atom gives a character on that subalgebra, satisfying every equation in the fragment. Extend the letter valuation by zero outside that subalgebra. Thus the theory is finitely satisfiable.

Under BPI, F1 extends the filter of step 1.1 to an ultrafilter $U$. For $p\in P$, set $v(p)=1$ precisely when $\{w:w(p)=1\}\in U$. An ultrafilter decides complements: adjoining a missing element makes a filter improper, so an old element is disjoint from it, forcing its complement into the old filter. Together with finite meet closure, this gives $a\wedge b\in U$ exactly when both $a,b\in U$, and $a\vee b\in U$ exactly when at least one belongs to $U$. Recursion on formulas now proves $v(\varphi )=1$ exactly when $\mathrm{⟦}\varphi \mathrm{⟧}\in U$, checking negation, conjunction and disjunction by these identities and both truth constants by properness. All truth sets from $T$ lie in $U$, so $v$ satisfies $T$.

A model of this propositional theory yields $h:B\to 2$, $h(b)=v(p_b)$, preserving all Boolean operations and both bounds by the equations. Its zero fibre is a proper ideal; if $h(b\wedge c)=0$, the two values in $2$ cannot both be $1$, so one of $b,c$ lies in that ideal. Hence it is prime, proving BPI. Empty $P$ in the forward direction causes no difficulty: $2^P$ is a singleton, and finite satisfiability excludes the false truth set. Empty $T$ is satisfied by the constant-zero valuation. No infinite choice was used in the finite fragment argument. QED.

First embed $L$ into a disjoint tagged copy, so that further tags cannot collide with original symbols. Adjoin one distinguished seed constant to get $L_0$. Given $L_n$, introduce a different constant $c_{n,E}$ for each existential $L_n$-sentence $E=\mathrm{\exists }x\varphi$, and put $L_{n+1}=L_n\cup \{c_{n,E}:E\text{ as above}\}$. These are sets since finite strings on a set form a set; tagging by $(n,E)$ is injective. Let $H_n$ be all sentences $E\to \varphi [c_{n,E}\mathrm{/}x]$. Set $L_{\mathrm{\infty }}={\bigcup }_{n<\omega }{L}_n$ and $T_H=T\cup {\bigcup }_{n<\omega }{H}_n$. The stage recursion uses uniquely specified sets, not choices of an enumeration.

Fix a finite subset $K$ of the added axioms, and list it in nondecreasing stage order, ordering each finite same-stage block arbitrarily. Starting from $T$, first use F1 to allow all constants of $L_{\mathrm{\infty }}$ except the finitely many designated witness constants in this list. This is a consistent pure expansion. When adding an axiom at stage $n$, its designated constant occurs neither in $T$, nor in an earlier-stage axiom, nor in the matrix of any other axiom at stage $n$: those matrices are in $L_n$, whereas the new constants were introduced in $L_{n+1}$. It is therefore fresh in the current theory and its matrix. F2 adjoins it with its axiom preserving consistency. After finitely many additions every axiom of $K$ has been added and the language is $L_{\mathrm{\infty }}$. Thus $T\cup K$ is consistent in the union language.

If $T_H$ were inconsistent, F3 would give a finite proof using only finitely many axioms from the sets $H_n$. These form a finite $K$ as in step 2.1, contradicting its consistency. Hence $T_H$ is consistent. Every existential $L_{\mathrm{\infty }}$-sentence uses finitely many symbols, each introduced at some finite stage; the maximum of those finitely many stages places the sentence in some $L_n$. Its witness axiom is then in $H_n\subseteq T_H$. The seed ensures a closed term even when the original language has no constants, and the empty finite set of new axioms is covered by F1. QED.

Under BPI, let $T$ be finitely satisfiable. If $T⊢\mathrm{\perp }$, F7 gives a finite $T_0\subseteq T$ proving $\mathrm{\perp }$. Its assumed nonempty model contradicts F3. Thus $T$ is consistent, and F1 supplies $T_H$ and $L_{\mathrm{\infty }}$ as stated there. Let $S$ be the set of all $L_{\mathrm{\infty }}$-sentences. It is a set because sentences are finite strings on a set of symbols.

Separately, assume first-order semantic compactness. For propositional letters in a set $P$, take a language with one constant $c$ and unary predicates $R_p$ for $p\in P$. Translate $p$ to $R_p(c)$, commute with Boolean connectives, and translate true and false to $c=c$ and $\mathrm{\neg }(c=c)$. A propositional valuation gives a structure on $\{0\}$ by $c=0$ and $R_p=\{0\}$ or $\mathrm{\varnothing }$ according to the valuation. Structural induction on formulas shows its translated truths are exactly the propositional truths. Thus any finitely satisfiable propositional theory translates to a finitely satisfiable first-order theory. By the assumed compactness it has a nonempty model $M$. The function $p\mapsto 1$ exactly when $M\models R_p(c)$ is a valuation satisfying the original theory, by the same induction. F2 yields BPI. This also handles $P=\mathrm{\varnothing }$ and empty theories: the one-point interpretations and empty valuation still exist.

Return to the consistent $T_H$ of step 1.1. Use one propositional letter $p_{\sigma }$ for each $\sigma \in S$. Form a propositional theory $\mathrm{\Delta }$ with: $p_{\tau }$ for every $\tau \in T_H$; $\mathrm{\neg }{p}_{\mathrm{\perp }}$; $p_{\mathrm{\neg }\sigma }\leftrightarrow \mathrm{\neg }{p}_{\sigma }$; $p_{\sigma \wedge \rho }\leftrightarrow (p_{\sigma }\wedge p_{\rho })$; and $(p_{{\sigma }_1}\wedge \cdots \wedge p_{{\sigma }_n})\to p_{\rho }$ whenever the finite sentence set $\{{\sigma }_1,\dots ,{\sigma }_n\}$ derives $\rho$. The empty conjunction for $n=0$ is true, so all sentence theorems are required. Derivability is witnessed by finite strings, hence the collection of these requirements is a set.

Fix a finite ${\mathrm{\Delta }}_0\subseteq \mathrm{\Delta }$. Only finitely many letters $p_{\sigma }$ occur; call their sentence indices $S_0$. Enumerate this finite set and apply F5 finitely many times, starting at $T_H$, to obtain a consistent extension $K$ deciding every $\sigma \in S_0$. Set $v(p_{\sigma })=1$ if the positive decision is in $K$, and $0$ otherwise, and give all other letters value $0$. Consistency and F6 prevent both decisions being in $K$, so the negative decision is in $K$ exactly when $v(p_{\sigma })=0$. Every listed $p_{\tau }$ with $\tau \in T_H$ has value $1$, since a negative decision would contradict $\tau \in K$. Also $v(p_{\mathrm{\perp }})=0$ whenever that letter occurs. For a negation coherence requirement, equal positive values for $\sigma ,\mathrm{\neg }\sigma$ contradict consistency, and equal negative values give $\mathrm{\neg }\sigma ,\mathrm{\neg }\mathrm{\neg }\sigma \in K$, again a contradiction by F6. For a conjunction requirement, a positive conjunction with a negative conjunct contradicts elimination, while two positive conjuncts and a negative conjunction contradict introduction. Thus all Boolean coherence requirements in ${\mathrm{\Delta }}_0$ hold. Finally, if all antecedent letters of a deduction requirement are true, their sentences belong to $K$. F7 transfers their finite derivation of $\rho$ to $K$, and consistency with F6 prevents $\mathrm{\neg }\rho \in K$; hence the conclusion letter is true. A false antecedent satisfies the implication automatically. When $n=0$, the same argument transfers the theorem proof to $K$. Therefore $v\models {\mathrm{\Delta }}_0$. Only finitely many decisions were made, not a simultaneous choice of completions for all finite subsets.

BPI and F2 now give a valuation $v\models \mathrm{\Delta }$. Put $H=\{\sigma \in S:v(p_{\sigma })=1\}$. It contains $T_H$ and omits $\mathrm{\perp }$. Negation coherence makes it complete. If $H⊢\rho$, F7 yields finitely many premises ${\sigma }_1,\dots ,{\sigma }_n\in H$ deriving $\rho$; the corresponding requirement of $\mathrm{\Delta }$ forces $\rho \in H$. Thus $H$ is deductively closed, and it is consistent because a proof of $\mathrm{\perp }$ would put $\mathrm{\perp }$ in $H$. For each $\mathrm{\exists }x\varphi \in H$, F1 supplies its witness implication $\mathrm{\exists }x\varphi \to \varphi (c)$ in $T_H\subseteq H$. Closure under derivability puts $\varphi (c)$ in $H$. The seed from F1 remains in the language. All hypotheses of F4 therefore hold, giving a nonempty set model of $H$ and hence, by reduct to the original language, a model of $T$. No language enumeration, infinite succession of decisions, or representative choice is used. Together with step 1.2 this proves the equivalence. QED.

A proper ultrafilter $V$ on a set $S$ decides every subset $A$: if $A\mathrm{\notin }V$, maximality says the filter generated by $V\cup \{A\}$ contains the empty set. Thus some $B\in V$ is disjoint from $A$, so $S\setminus A\in V$. Both cannot occur. If $S$ is compact, the closed sets $\bar{B}$, $B\in V$, have FIP: any finite intersection contains the nonempty intersection of the corresponding members of $V$. F5 gives a point $s$ in all these closures. Every open neighborhood $N$ of $s$ belongs to $V$, since otherwise the closed complement belongs to $V$, contradicting $s\in \overline{S\setminus N}=S\setminus N$. When $S$ is Hausdorff there is at most one such limit: two distinct limits have disjoint neighborhoods, which cannot both be in a proper filter. Hence each ultrafilter on a compact Hausdorff space has a unique limit.

Assume BPI and that each $X_i$ is nonempty. Let $E$ be the set of all functions $s$ with finite domain contained in $I$ and $s(i)\in X_i$ on their domains. The empty function belongs to $E$. For a finite $J\subseteq I$ put $D_J=\{s\in E:J\subseteq \mathrm{dom}s\}$. This set is nonempty by finite choice in ZF; explicitly, induction on the size of $J$ extends a partial selection by one element from the next nonempty factor. Moreover $D_J\cap D_K=D_{J\cup K}$ and $D_{\mathrm{\varnothing }}=E$. Their supersets form a proper filter, which F1 extends to an ultrafilter $W$ on $E$.

Separately, assume compactness of all products of compact Hausdorff spaces. Given a finitely satisfiable set $\mathrm{\Gamma }$ of propositional formulas with letters in a set $P$, take $2^P$ with discrete two-point factors. Each factor is compact (an open cover has a subcover with at most two members) and Hausdorff (the two singletons separate its points), so the assumed principle makes $2^P$ compact. The space is nonempty even without the principle, since the constant-zero function is a valuation. For a finite formula $\varphi$, its truth set $C_{\varphi }$ is clopen: a letter's truth set is a coordinate singleton cylinder, negation takes complements, and conjunction and disjunction take finite intersections and unions. This structural induction applies also to truth constants, whose sets are the whole cube and the empty set. Finite satisfiability says precisely that the $C_{\varphi }$, $\varphi \in \mathrm{\Gamma }$, have FIP. F5 gives a point satisfying all of $\mathrm{\Gamma }$. By F2, BPI follows.

Returning to the BPI assumption in step 1.2, for $i\in I$ and $A\subseteq X_i$, put $A^{(i)}=\{s\in D_{\{i\}}:s(i)\in A\}$ and $V_i=\{A\subseteq X_i:A^{(i)}\in W\}$. These sets form a proper filter: inverse images preserve intersections and inclusions, $X_i^{(i)}=D_{\{i\}}\in W$, and ${\mathrm{\varnothing }}^{(i)}=\mathrm{\varnothing }\mathrm{\notin }W$. The two sets $A^{(i)}$ and $(X_i\setminus A{)}^{(i)}$ partition the $W$-large domain $D_{\{i\}}$. By step 1.1 exactly one is in $W$, so $V_i$ is an ultrafilter: adjoining any missing $A$ contradicts its already present complement. Step 1.1 supplies its unique limit $x_i\in X_i$. Replacement on this unique specification gives the function $i\mapsto x_i$ in ZF. It is an element of $X={\prod }_i{X}_i$, proving nonemptiness without choosing from a family of multiple limit points.

To prove compactness of this nonempty product, let $\mathcal{C}$ be a closed FIP family in $X$. The sets containing a finite intersection from $\mathcal{C}$ form a proper filter; F1 extends it to an ultrafilter $U$. For each $i$, the family $\{A\subseteq X_i:{\pi }_i^{-1}[A]\in U\}$ is an ultrafilter by inverse-image identities and the decision property in step 1.1. Its unique limit $y_i$ again defines a product point $y$. Each basic neighborhood of $y$ is a finite intersection of inverse images of coordinate neighborhoods, all of which belong to $U$. Thus every neighborhood of $y$ is in $U$. For $C\in \mathcal{C}$, if $y\mathrm{\notin }C$, its open complement would be in $U$ together with $C$, a contradiction. Therefore $y\in \bigcap \mathcal{C}$, and F5 proves compactness.