Relative consistency of BPI with failure of Stone's theorem

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 following constructions are interpreted internally in $M$.

In $M$ choose its countable rational ordered Urysohn metric structure $U_{\mathbb{Q}}^{<}$ and let $A=\{⟨0,u⟩:u\in U_{\mathbb{Q}}^{<}\}$, carrying the transported order and metric. Represent sets by tagged objects $⟨1,S⟩$ and form the class hierarchy $X_0=A$, $X_{\alpha +1}=A\cup \{⟨1,S⟩:S\subseteq X_{\alpha }\}$, with unions at limits and membership in a tag given by membership in its second coordinate. Internally this satisfies ZFA+AC: tagged set operations give the elementary axioms and Power Set; translated Separation and Replacement follow in $M$, with Collection bounding construction ranks; minimal construction rank gives Foundation; and $M$'s well-orders give tagged choice functions. No external well-foundedness of $M$ is used.

Form Corson's ordered-rational finite-support permutation model inside this ZFA+AC interpretation. The group, topology, finite stabilisers and their extreme amenability are all computed internally. Hence [F1], using the arbitrary-ground form of the fixed-point theorem, gives BPI in the hereditarily symmetric interpretation. By [F2] that interpretation also contains the certified rational metric space and its open cover with no point-finite open refinement.

By [F3], the conjunction of BPI with the certified sentence transfers from this permutation model to an atom-free model of $\mathrm{Z}\mathrm{F}$. Consequently $\mathrm{Con}(\mathrm{Z}\mathrm{F})\Rightarrow \mathrm{Con}(\mathrm{Z}\mathrm{F}+\mathrm{B}\mathrm{P}\mathrm{I}+\text{there is a metrizable nonmetacompact space})\mathrm{.}$ This is Corson's external relative-consistency construction. Completeness did not supply a transitive model; the internal tagged interpretation and the arbitrary-ground BPI theorem provide the required bridge. No application of the formal proof-reduction interface, and hence no unprovided uniform code map, is asserted.

A space that is not metacompact has an open cover with no point-finite open refinement. Every locally finite open refinement is point-finite, so that cover has no locally finite open refinement either. The space is therefore not paracompact, and Stone's theorem fails in the transferred model.