Relative consistency of BPI without Urysohn's lemma

Assume $\mathrm{Con}(\mathrm{Z}\mathrm{F})$. By [F4] obtain a possibly externally ill-founded model $M$ of $\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H}$. All constructions in the next steps are interpreted internally in $M$.

Inside $M$, let $A=\{⟨0,q⟩:q\in {\mathbb{Q}}^M\}$, ordered by the rational order of $M$, and represent sets by tagged objects $⟨1,S⟩$. Define the tagged ZFA hierarchy by $X_0=A$, $X_{\alpha +1}=A\cup \{⟨1,S⟩:S\subseteq X_{\alpha }\}$ and unions at limits, and put $u{\in }_{\ast }⟨1,S⟩$ exactly when $u\in S$. Interpreted inside $M$, this is a model of ZFA+AC: the usual tagged constructions give Extensionality, Pairing, Union and Power Set; translated Separation and Replacement are instances in $M$ (Collection bounds the construction ranks of Replacement images); minimal construction rank gives Foundation; the tagged copy of ${\omega }^M$ gives Infinity; and an $M$-well-order of every underlying member set gives the tagged choice function. This internal tagged construction does not require $M$ to be externally transitive.

In this ZFA+AC interpretation form the rational-ordered finite-support Läuchli model of [F1]. The automorphism group and all finite stabilisers are the objects computed internally by $M$. Thus [F1] gives their internal extreme amenability, and the arbitrary-ground formulation [F2] gives BPI in the hereditarily symmetric interpretation.

By [F3] the same interpretation contains the certified Urysohn obstruction, so BPI and that certified sentence hold together there.

By [F4], the conjunction of BPI with the certified sentence transfers to an atom-free model of $\mathrm{Z}\mathrm{F}$. Therefore $\mathrm{Con}(\mathrm{Z}\mathrm{F})\Rightarrow \mathrm{Con}(\mathrm{Z}\mathrm{F}+\mathrm{B}\mathrm{P}\mathrm{I}+\mathrm{\neg }\mathrm{U}\mathrm{R}\mathrm{Y})\mathrm{.}$ This is an external relative-consistency construction. The model supplied by completeness need not be transitive; the internal tagged interpretation and the arbitrary-ground BPI theorem are precisely what makes the construction apply. No unprovided uniform proof-code reduction for the subsequent permutation and Pincus constructions is asserted.