Extreme amenability yields BPI in finite-support permutation models

Carry out the argument in $M$. Let $B$ be an internally nontrivial Boolean algebra of the hereditarily symmetric interpretation, and choose a finite support $E$ for its entire structure; put $H=\mathrm{fix}(E)$. The induced action of $H$ on its underlying set preserves every algebra operation and constant, so acts by Boolean automorphisms. Each $b\in B$ is hereditarily symmetric and has a finite support of its own.

In $M$ let $S(B)$ be the set of prime ideals, represented by their characteristic functions in $2^B$. It is internally nonempty by [F2]. It is internally closed: failure of any condition in [F4] is witnessed by finitely many coordinates ($0$, $1$, a pair $a\le b$, a join or a meet), so every nonideal or nonprime subset has a basic product neighbourhood disjoint from $S(B)$. Internally, $2^B$ is compact by [F2] and [L1], and $S(B)$ is therefore compact with its subspace topology. Distinct subsets differ at a coordinate, whose two complementary cylinders separate them, so $S(B)$ is Hausdorff. AC is used in $M$ for BPI and the resulting product compactness; it is not assumed in the hereditarily symmetric interpretation.

For $h\in H$ and $P\in S(B)$ put $hP=\{hb:b\in P\}$. Boolean automorphisms preserve the prime-ideal conditions, so this defines an action on $S(B)$. To prove joint continuity, fix $(h_0,P_0)$ and a basic neighbourhood of $h_0{P}_0$ specifying membership on a finite set $C\subseteq B$. For each $b\in C$, take a finite support of $h_0^{-1}b$, and let $D$ be their finite union. Then $K=H\cap \mathrm{fix}(D)$ is open in $H$ for the pointwise-convergence topology on atoms. The coset $h_{0}K$ is open: its defining restrictions are $h(a)=h_0(a)$ for $a\in D$, within $H$. Let $V$ consist of prime ideals agreeing with $P_0$ on $h_0^{-1}C$. For $h=h_{0}k\in h_{0}K$ and $P\in V$, one has $h^{-1}b=k^{-1}{h}_0^{-1}b=h_0^{-1}b$ for $b\in C$, so $b\in hP$ exactly when $b\in h_0{P}_0$. Thus $(h_{0}K)\times V$ maps into the prescribed neighbourhood. This proves joint continuity; it does not assert openness of a prime ideal's point stabilizer.

Inside $M$, apply the Given extreme amenability of $H$ to the internally nonempty compact Hausdorff space of step 2.1 and the continuous action of step 2.2. Obtain a prime ideal $P$ fixed by every member of $H$.

The finite set $E$ supports $P$. Moreover every member of $P$ belongs to $B$ and hence is hereditarily symmetric. Thus $P$ is hereditarily symmetric by [F1], so belongs to the interpretation. The prime-ideal conditions are bounded formulas about $P$, $B$, their operations and their members. Relativising those bounded quantifiers to the hereditarily symmetric interpretation changes no witness: all elements of $B$ already lie there, and the operations are the same supported objects. Therefore the interpretation itself satisfies that $P$ is a prime ideal of $B$. No appeal to external transitivity is made.

The reasoning in steps 1.1--4.1 is an argument formalised inside the arbitrary model $M$. Since $B$ was an arbitrary internally nontrivial Boolean algebra of its hereditarily symmetric interpretation, the internal prime ideal furnished in step 4.1 establishes BPI there. The trivial algebra requires no prime ideal. This conclusion therefore applies equally to externally ill-founded models used in relative-consistency arguments.