In Jech one can find a lower bound for the consistency strength of PFA in terms of large cardinals. I don't have my copy of Jech in front of me at the moment, but as I recall the presentation of this fact goes something like this:


* It's stated and proven that PFA implies the failure of $\square \_{\kappa}$ for all $\kappa > \omega$.
* It's stated that a result of Magidor's shows that PFA implies the failure of a weaker version of square, but the proof of this is not given in the chapter (it might appear later in the book, I can't remember).
* It's stated that a result of Schimmerling's proves that the failure of this weak version of square implies the existence of a model with countably many Woodin cardinals, and this is also not proved in the chapter.


My question is whether this weaker version of square is necessary to get a lower bound in terms of large cardinals, or whether there is some large cardinal lower bound on the consistency strength of "square fails everywhere" itself?



What is the consistency strength of the failure of square, in terms of large cardinals
My understanding is that the weaker form of square was initially needed to get a better lower bound on the consistency strength of PFA but that, with improvements in our understanding of the fine structure of the current inner models, the original form of square now suffices to give the best lower bounds.


There are two versions of square (each with their associated ``weak square'' heierarchy): $\square\_\kappa$ (formulated by Jensen) and $\square (\kappa)$ (formulated by Todorcevic). It is immediate from their definitions that $\square\_\kappa$ implies $\square (\kappa^+)$ ($\square\_\kappa$ and $\square (\kappa^+)$ are both statements about sequences of length $\kappa^+$ --- the apparent shift in indexing is purely notational). Todorcevic's theorem is that PFA implies the failure of $\square (\kappa)$ for every regular $\kappa > \omega\_1$. It is often cited in the weaker form stated in item 1 of the question.


Traditionally, lower bounds on PFA have been obtained through the failure of $\square\_\kappa$ at
a single singular strong limit cardinal. To my knowledge, there is currently no method for obtaining better lower bounds on PFA. 


It was somewhat of a breakthrough when it was realized that the failure of $\square (\kappa)$ at successive values of $\kappa$ was apparently more powerful than the failure of successive instances of $\square\_\kappa$. That it took so long for this to be noticed may be due to the fact that Todorcevic's result was commonly cited in its weaker form. I don't believe, however, that this gives an improved lower bound on the consistency strength of PFA. It does, however, yield more strength from the failure of any form of square at cardinals below $\aleph\_\omega$.


It is at least my impression that it *should* be the case that the failure of square at all cardinals has a much higher strength than and individual failure of $\square (\kappa)$ or
$\square\_\kappa$. Whether the global failure of $\square\_\kappa$, $\square (\kappa)$ or the weak forms of square mentioned above yield different consistency strengths is a matter which is completely open and for which there is only wild speculation.


