We complete our introduction to the principle ISP and its relatives as well as their connections to supercompact cardinals and the proper forcing axiom. As a consequence of our analysis we give a proof that all known forcing constructions of models satisfying PFA require very large cardinals.