 The proof uses the fact that proper forcings are preserved under countable support iteration, and the fact that if formula_8 is supercompact, then there exists a Laver function for formula_8.It is not yet known how much large cardinal strength comes from PFA.The bounded proper forcing axiom (BPFA) is a weaker variant of PFA which instead of arbitrary dense subsets applies only to maximal antichains of size ω1.