Exact Consistency Strength of the Proper Forcing Axiom

Exact Consistency Strength of the Proper Forcing Axiom

Definitions and mathematical statement

A forcing notion $P$ is proper when, for sufficiently large regular $\theta$, every countable elementary submodel $M\prec H(\theta)$ containing $P$ and every $p\in P\cap M$ admit an extension $q\le p$ that is $M$-generic: each dense set $D\in M$ has $D\cap M$ predense below $q$. PFA states that for every proper $P$ and every family of $\aleph_1$ dense subsets of $P$, a filter meets them all. The problem asks for a large-cardinal theory $T$ with matching consistency implications \[ \operatorname{Con}(T)\ \longleftrightarrow\ \operatorname{Con}(\mathrm{ZFC}+\mathrm{PFA}). \] An upper consistency construction alone is not a matching lower bound, and the target does not prespecify a particular large cardinal as the answer.

Formulation and concept references: [S1].

Short English statement

Exactly how strong a large-cardinal assumption is needed, in consistency terms, for the Proper Forcing Axiom?

Research attempt

Current frontier.

The 2025 Oberwolfach report gives the familiar supercompact upper consistency bound and emphasizes the gap with current lower bounds. Its equiconsistencies concern specified strengthenings of PFA, together with additional assumptions, not plain PFA [S1]. Moore's discussion includes the substantial consequence that PFA implies determinacy in $L({\mathbb{R}})$ [S2], Theorem 6.15. We use these as bounds and obstructions, not as matching consistency implications. In particular, a theorem constraining a particular forcing construction of PFA is not automatically a theorem extracting a supercompact inner model from every model of PFA.

Attack route.

A lower-bound strategy would extract coherent normal fine measures on sets of small subsets, then build an iterable inner model. A different strategy might show that any sufficiently general PFA-forcing construction starts from a supercompact cardinal; this still requires a reduction of arbitrary consistency to that construction. We test the first route by separating filters from ultrafilters and by checking whether the obvious candidate cardinal, the ambient $\omega_2$, could even carry the desired measures. The test identifies a genuine obstruction before any unsupported inner-model assertion is made.

Attempt.

Recall that a supercompact cardinal $\kappa$ carries, for each $\lambda\ge\kappa$, a normal fine $\kappa$-complete ultrafilter on \[ P_\kappa(\lambda)=\{x\subseteq\lambda:|x|<\kappa\}. \] Fine means that $\{x:\alpha\in x\}$ belongs to the ultrafilter for every $\alpha<\lambda$. Normality is closure under diagonal intersections, equivalently the regressive-function property in this setting. Ultrafilter means every subset of $P_\kappa(\lambda)$ is decided. The combination, not any one property separately, is the large-cardinal input [E1].

There is a tempting false shortcut: normal fine complete filters are easy to obtain. For every uncountable regular $\kappa$, the club filter on $P_\kappa(\lambda)$ is fine, normal, and $\kappa$-complete. Fineness follows from the club of sets containing a prescribed ordinal. Intersections of fewer than $\kappa$ clubs are club by successive closure and regularity; the analogous diagonal closure proves normality. These filters exist in ZFC at $\kappa=\omega_2$, without PFA or a large-cardinal assumption. Thus a construction producing only these properties has not reached the needed consistency strength.

Lemma (ambient successor obstruction). There is no nonprincipal $\kappa$-complete ultrafilter on a successor cardinal $\kappa$. First, such an ultrafilter $U$ is uniform: any subset of size $<\kappa$ is a union of fewer than $\kappa$ singletons, whose complements lie in $U$, and so cannot belong to $U$. Suppose $\mu<\kappa$ and $2^\mu\ge\kappa$. Choose distinct subsets $A_\alpha\subseteq\mu$ for $\alpha<\kappa$. For each $i<\mu$, $U$ chooses one of \[ \{\alpha:i\in A_\alpha\},\qquad\{\alpha:i\notin A_\alpha\}. \] The intersection of the chosen $\mu$ sets belongs to $U$ by $\kappa$-completeness, but contains at most one ordinal because the $A_\alpha$ are distinct. This contradicts uniformity. Therefore $2^\mu<\kappa$ for every $\mu<\kappa$. At a successor $\kappa=\nu^+$, Cantor's theorem gives $2^\nu\ge\nu^+=\kappa$, the required contradiction.

In particular, a fine $\omega_2$-complete ultrafilter on $P_{\omega_2}(\omega_2)$ cannot exist in the ambient universe. To see this directly from the lemma, push it forward by $x\mapsto\sup x<\omega_2$. Fineness makes this pushforward contain every tail of $\omega_2$; it is nonprincipal and $\omega_2$-complete. This is impossible by the successor obstruction.

A putative lower-bound proof must consequently construct an inner model $W$ with its own power sets and cardinal structure. The ordinal that is $\omega_2$ externally can be inaccessible or supercompact internally; there is no contradiction in that possibility. But the inner-model construction, coherence of its measures, and iterability are exactly the substantial missing arguments. They cannot be replaced by saying that a reflection filter in the PFA universe "is a measure."

Dense-set counting check. A second proposal forces a partial ultrafilter and invokes PFA to meet all decision requirements. PFA supplies a filter meeting a family of size $\aleph_1$ for a proper forcing. A complete ultrafilter on $P_\kappa(\lambda)$ must decide $2^{|P_\kappa(\lambda)|}$ subsets in the relevant model; no compression of those requirements to $\aleph_1$ dense sets has been given. Moreover, properness of the proposed partial-ultrafilter forcing and preservation of $\kappa$-completeness require proofs. Finite consistency of choices yields neither uncountable completeness nor a well-founded ultrapower.

Stress test.

The report's theorem that certain proper iteration constructions of PFA require a supercompact starting cardinal has a construction hypothesis. Removing it would be a new lower-bound theorem, not an application of the quoted result [S1]. Likewise its results for strengthened forcing axioms and bedrock assumptions cannot be used for the exact theory $\mathrm{ZFC}+\mathrm{PFA}$ without proving those extra assumptions follow from PFA. The ambient-successor obstruction concerns measures in the outer universe only; it does not refute a possible supercompact inner model. Finally, no numerical experiment is relevant to the required relative-consistency and iterability assertions.

Outcome.

Outcome: Exploratory approach with unresolved gap. The attempted direct measure extraction fails for an explicit reason: the filter properties available without large cardinals do not give an ultrafilter, and the desired measure cannot live on the ambient successor cardinal. The analysis isolates the need for an inner-model construction and rules out a dense-set-counting shortcut. It does not improve either consistency bound, identify a matching large-cardinal theory, or assert an equiconsistency not contained in the cited sources.

Sources

• S1 Oberwolfach Report 2025/2, Equiconsistencies between strengthenings of PFA and strengthenings of supercompact cardinals. https://ems.press/content/serial-article-files/51347. Catalogue formulation source.
• S2 Status source for Exact Consistency Strength of the Proper Forcing Axiom. https://pi.math.cornell.edu/~justin/Ftp/ICM.pdf. Catalogue research/status reference; not a proof endorsement.
• E1 Matteo Viale and Christoph Wei

  \ss

  , On the consistency strength of the proper forcing axiom, Advances in Mathematics 228 $2011$, 2672--2687; supercompactness and restrictions on forcing constructions of PFA. https://arxiv.org/abs/1012.2046. Research reference; consulted 27 September 2026.