On the consistency strength of the proper forcing axiom

TL;DR

This paper explores the implications of the proper forcing axiom (PFA) on certain combinatorial principles related to large cardinals, establishing that PFA implies these principles for  and that forcing PFA necessitates a supercompact cardinal.

Contribution

It demonstrates that PFA implies combinatorial principles for  and shows that forcing PFA from large cardinals requires a supercompact cardinal, clarifying the consistency strength of PFA.

Findings

PFA implies combinatorial principles for .

Forcing PFA from large cardinals requires a supercompact cardinal.

Proper forcing to obtain PFA is optimal in terms of consistency strength.

Abstract

Recently the second author introduced combinatorial principles that characterize supercompactness for inaccessible cardinals but can also hold true for small cardinals. We prove that the proper forcing axiom PFA implies these principles hold for $\omega_2$. Using this, we argue to show that any of the known methods for forcing models of PFA from a large cardinal assumption requires a strongly compact cardinal. If one forces PFA using a proper forcing, then we get the optimal result that a supercompact cardinal is necessary.