Relative consistency from a proper class of strongly compact cardinals

Let $\mathrm{\Delta }$ be an arbitrary external finite fragment of $U=\mathrm{Z}\mathrm{F}+\text{“every uncountable cardinal has cofinality }\omega \text{.”}$ Expand, for the sentences in $\mathrm{\Delta }$, the actual fixed-formula derivations underlying F6--F9: the required coordinate-filter and $P_3$ clauses, the atomic class-forcing recursion, its Boolean and existential clauses, the needed Separation/Collection name constructions, the particular homogenization and Power Set argument, and the coordinate proof of the single cofinality sentence. By F12 each one has finite assumption support, and finitely many such supports have finite union. Retain each specifically used ground Separation/Replacement instance, recursion instance, parameter-existence formula, and local class-theory instance. Let $\mathrm{\Gamma }$ be their finite set of pure ground translations, enlarged by Extensionality, AC, the finite instances required by Felgner's preparation, and the sentences $\mathsf{P}\mathsf{C}\mathsf{S}\mathsf{C}$ and $\mathsf{N}\mathsf{R}\mathsf{L}\mathsf{P}$ required by the reduced F6 construction. No theorem saying that a finite-fragment model satisfies full ZFC is invoked here.

Work in $T$. If there is no regular limit of strongly compact cardinals, let $V^{\ast }=V$. Otherwise let $\lambda$ be the least regular limit of strongly compact cardinals and let $V^{\ast }=V_{\lambda }$. In the second case $\lambda$ is strongly inaccessible, strongly compact cardinals are unbounded below it, and all set-sized fine-ultrafilter witnesses with target below $\lambda$ belong to $V_{\lambda }$; hence $V_{\lambda }\models T$. Minimality of $\lambda$ says that $V_{\lambda }\models \mathsf{N}\mathsf{R}\mathsf{L}\mathsf{P}$. In the first case $V$ itself models $T+\mathsf{N}\mathsf{R}\mathsf{L}\mathsf{P}$. Thus in both cases the following reflection construction is carried out inside a transitive $V^{\ast }\models T+\mathsf{N}\mathsf{R}\mathsf{L}\mathsf{P}$; this is Schürz's opening reduction, not an inference from $\mathsf{P}\mathsf{C}\mathsf{S}\mathsf{C}$ alone. Close the finite formula family underlying $\mathrm{\Gamma }$ under subformulas. Inside $V^{\ast }$ recursively choose reflection ordinals ${\beta }_0<{\beta }_1<\cdots$ for that family and strongly compact cardinals ${\beta }_n<{\kappa }_n<{\beta }_{n+1}\mathrm{.}$ F2 gives the next reflection ordinal and $\mathsf{P}\mathsf{C}\mathsf{S}\mathsf{C}$ gives the next ${\kappa }_n$; least ordinal witnesses make this an ordinary recursion on $\omega$. Put $\beta ={\sup }_n{\beta }_n$ (so $\beta <\lambda$ in the $V_{\lambda }$ case by regularity). If parameters lie in $V_{\beta }^{V^{\ast }}$, one $V_{{\beta }_n}^{V^{\ast }}$ contains them. Reflection there supplies, for every true existential subformula in the closed family, a witness already in $V_{{\beta }_n}^{V^{\ast }}\subseteq V_{\beta }^{V^{\ast }}$. The witness criterion therefore makes $V_{\beta }^{V^{\ast }}$ satisfy every sentence of $\mathrm{\Gamma }$ other than $\mathsf{P}\mathsf{C}\mathsf{S}\mathsf{C}$. For $\alpha <\beta$, choose $n$ with $\alpha <{\beta }_n$. Then $\alpha <{\kappa }_n<\beta$. If the reflected stage asks for one of the fine-ultrafilter witnesses expressing strong compactness of ${\kappa }_n$, F4 supplies it in $V^{\ast }$. Its rank is finitely above the ranks of its target data, and some later reflection stage ${\beta }_m$ contains it. Fineness, ${\kappa }_n$-completeness and extension of the relevant filter are absolute for these transitive stages. Thus $V_{\beta }^{V^{\ast }}$ regards the ${\kappa }_n$ as internally unbounded strongly compact cardinals. Because $\mathsf{N}\mathsf{R}\mathsf{L}\mathsf{P}$ belongs to the reflected formula family and is true in $V^{\ast }$, it is true in $V_{\beta }^{V^{\ast }}$ as well. Hence $V_{\beta }^{V^{\ast }}\models \mathrm{\Gamma }$, including both $\mathsf{P}\mathsf{C}\mathsf{S}\mathsf{C}$ and $\mathsf{N}\mathsf{R}\mathsf{L}\mathsf{P}$.

Start the construction above beyond $\omega$, so $V_{\beta }$ is infinite. Apply F3 to this membership structure and collapse a countable elementary submodel. The result is a countable transitive set $M$ satisfying the fixed source fragment $\mathrm{\Gamma }$, AC, and the sentences $\mathsf{P}\mathsf{C}\mathsf{S}\mathsf{C}$ and $\mathsf{N}\mathsf{R}\mathsf{L}\mathsf{P}$. Its internally strongly compact ordinals need not be strongly compact in the ambient universe; the retained proofs use only the filters, completeness statements and sequences which $M$ contains.

Take the definable-class expansion of $M$. For each of the finitely many class instances retained in step 1.1, its set part is the corresponding pure formula in $\mathrm{\Gamma }$. Apply the fixed finite part of Felgner's construction F5. Because $M$ and its definable classes are externally countable, enumerate the dense classes of local choice conditions and recursively choose a descending complete sequence meeting them. The resulting class predicate $W$ well-orders the whole set universe of $M$; the forcing truth argument verifies exactly the retained $W$-Separation and $W$-Replacement instances. Felgner's membership isomorphism shows that this adds classes but no sets, so $(M,\in )$ still satisfies $\mathrm{\Gamma }$, $\mathsf{P}\mathsf{C}\mathsf{S}\mathsf{C}$ and $\mathsf{N}\mathsf{R}\mathsf{L}\mathsf{P}$. This is the amenable global well-order appearing among the retained premises of the F6 construction, rather than an arbitrary external well-order of $M$.

In the prepared class structure, $W$ makes the choices occurring in the retained coordinate-filter and cofinal-sequence formulas. Execute the particular definitions and finite derivations selected in step 1.1 to obtain the required instance of $P_3^M$; this uses F6 as the source of those derivations, not as a theorem applied to a model of full ZFC. Externally, this internally proper class is a countable set of conditions because it is a subclass of the countable set $M$. Enumerate its ground-definable dense classes and recursively take stronger conditions to obtain an $M$-generic $G$. Evaluation is well-founded because $M$ is transitive. The hereditarily symmetric names form an ambient set, so their values form a nonempty set structure $N$. Now concatenate and relativize the finite derivations retained in step 1.1, as licensed by F12. The retained fixed-formula forcing/truth derivations underlying F7 apply to the particular formulas over $(M,W,G)$; the retained derivations underlying F8 verify the ZF axioms occurring in $\mathrm{\Delta }$, and those underlying F9 verify the cofinality sentence. Consequently $N\models \mathrm{\Delta }$. When the cardinal consequence is stated, the retained instance underlying F10 verifies internally that cofinality $\omega$ is strictly below every uncountable cardinal, so those cardinals are singular. No full-theory interface F6--F10 is applied to the finite-fragment model $M$.

Steps 2.1–3.1 are a $T$ proof of existence of the suitable CTM for the fixed finite source data; steps 4.1–5.1 are a $T$ proof converting it to a set model of the arbitrary fixed finite $\mathrm{\Delta }$. F1 therefore gives the external implication $\mathrm{Con}(T)⟹\mathrm{Con}(U)\mathrm{.}$ The empty $\mathrm{\Delta }$ needs only a nonempty set model and is covered by the same construction. No converse is claimed. In particular, this argument neither derives a transitive model of all of $T$ from $\mathrm{Con}(T)$ nor claims a PA-verified uniform map on proof codes; it supplies exactly the external finite assemblies required by F1.