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.

muchhigher than we can currently reach. Essentially, so far, whenever you see a proof that PFA has such and such lower bound, what we have proved is that this follows from failures of square. Grigor Sargsyan gave a very nice talk at Luminy showing how to push these bounds as far as current descriptive inner model theory goes, you may want to ask him for a copy of his slides. – Andres Caicedo Jan 27 '11 at 16:28