Strong compactness and the product-measure extension interface

First work with a supplied transitive model $M$ of ZFC containing a strongly compact $\kappa$, and a supplied generic for its fair-coin probability algebra on $2^{\kappa }$. By F1, $\kappa$ is inaccessible in $M$, so its ground continuum is below $\kappa$. F2 makes $W=M[G]$ a transitive ZFC model with unchanged cardinals and continuum $\kappa$. These are precisely the separate preservation premises in F3. Applying F3 gives, for every cardinal $\lambda$ of $W$, a countably additive probability on $\mathcal{P}((2^{\lambda }{)}^W{)}^W$ agreeing with its cylinder product measure. Its null ideal is closed under every family in $W$ of length below the continuum. Thus $W$ satisfies the single first-order PMEA sentence. The empty coordinate product is included and has one point. No formal consistency implication has yet been drawn.

We specify the finite-fragment use of this construction. For any fixed finite set $\mathrm{\Delta }$ of ZFC axioms there is a finite set $\mathrm{\Gamma }$ of ZFC axioms such that the preceding construction over a countable transitive ground satisfying $\mathrm{\Gamma }$ and the strongly-compact-cardinal assertion gives a set extension satisfying $\mathrm{\Delta }$ and PMEA. To obtain $\mathrm{\Gamma }$, expand the proofs used in step 1.1, but replace the assertion of all ZFC in the extension by just the needed axiom instances. For each required Separation or Replacement instance use its explicit name construction in F4, applied to that particular formula; use Boolean truth only for this formula and its finitely many subformulas. Add the finite ground axiom instances used by these name constructions, by name-rank recursion and evaluation, and by their definability/absoluteness proofs. Internal satisfaction of every ZFC axiom at once is never a premise of this expansion.

The additional requirements in this expansion are finite. PMEA, countable additivity and closure under small indexed null families are each fixed first-order assertions about sets and functions; their universal cardinal and family variables are parameters, not an infinite list of formulas. The probability, Radon–Nikodym, fine-coordinate, density-vector and generic-cut proofs used in F3 consist of fixed first-order arguments, so their uses of Separation, Replacement and recursion require finitely many ground instances. The cardinal proof in F2 uses fixed formulas for the table of ordinal values, countable cylinder codes, Boolean vectors and the generic sequence of reals. Its appeal to extension ZFC is replaced by the finitely many instances actually used to form these graphs, powersets and enumerations. The same is done for the product pullback's function graph and for its countable-additivity argument. Include the elementary finite-set, ordinal and natural-number facts used for transitive-model absoluteness. Each called proof is finite; schema calls are expanded at their actual formulas, and structural inductions are single instances for the fixed defining formulas. Collecting the ground assumptions in these finite derivations, together with the fixed elementary axioms, gives $\mathrm{\Gamma }$. This is a syntactic finite-proof extraction, not an inference from a black-box statement conditional on a model of full ZFC. It proves the finite-fragment assertion in step 2.1, with all its parameters universally quantified.

Fix an alleged finite refutation $p$ from $T$. Let $\mathrm{\Delta }$ consist of the ZFC axiom instances occurring in $p$, and obtain $\mathrm{\Gamma }$ by steps 2.1–3.1. Work within $S$ and choose its strongly compact cardinal $\kappa$. Express strong compactness by its set-filter-extension definition, a single first-order formula $\mathrm{S}\mathrm{C}(\kappa )$. Apply F5 to $\mathrm{\Gamma }$, this formula and Extensionality, with a rank bound above $\kappa$. The resulting transitive rank segment $V_{\theta }$ satisfies $\mathrm{\Gamma }$ and $\mathrm{S}\mathrm{C}(\kappa )$ and contains $\kappa$. This invokes reflection for one fixed finite family, rather than reflection of the entire ZFC schema.

By F6 take a countable $H\prec (V_{\theta },\in )$ containing $\kappa$, and collapse it to a transitive set $M$. Its collapsed parameter $\bar{\kappa }$ satisfies $\mathrm{S}\mathrm{C}(\bar{\kappa })$ in $M$, and $M$ satisfies $\mathrm{\Gamma }$. External Foundation applies because the relation is actual membership; Extensionality transfers to $H$. Thus all collapse hypotheses hold. The ordinal $\bar{\kappa }$ need not be uncountable in the ambient universe: the large-cardinal and measure constructions are internal to $M$, exactly as in the supplied-ground arguments. No model of full ZFC with a strongly compact cardinal has been asserted.

Form in $M$ its random probability algebra $\mathbb{B}$ at $\bar{\kappa }$, using the construction included in $\mathrm{\Gamma }$. The nonzero preorder is nonempty. Since $M$ is countable, its subsets which it regards as dense in this preorder form an externally countable family. They are actually dense: density only quantifies over the same underlying condition set and order in the transitive model. Apply F7 to obtain a filter meeting every member of that family, hence an $M$-generic $G$. The set of names in $M$ and ambient rank recursion give the set $W=M[G]$. Steps 2.1–3.1 apply to this finite-adequate ground, so $W$ satisfies $\mathrm{\Delta }$ and PMEA. Only this finite target fragment is claimed here.

The nonempty set structure $W$ satisfies every assumption used in $p$, but $p$ derives contradiction. F8 rules this out. For this fixed $p$, steps 4.1–6.1 and soundness are finite derivations in $S$; together with the syntactic verification that $p$ is a refutation of $T$, they give a refutation of $S$. The transformation is effective: extract the finite axiom list from $p$, substitute its formulas into the fixed name and truth proof schemes, collect their finite assumptions, insert the corresponding finite reflection proof, and apply finite soundness. These are operations on finite formulas and proofs, so the same construction gives the usual arithmetized implication from existence of a $T$-refutation to existence of an $S$-refutation. Contraposition proves $\mathrm{Con}(S)\Rightarrow \mathrm{Con}(T)$, exactly the binding assertion. It asserts neither consistency premise, a ground-model PMEA implication, nor existence of a transitive model of full $S$.