Proper forcing axiom

Summary

The proper forcing axiom, PFA, is a strong extension of Martin's axiom at $\aleph_1$. It replaces the countable chain condition by the much weaker condition of properness. It says that for each proper forcing notion one can meet $\aleph_1$ dense sets with a single filter; the precise definition is given separately. Its consistency is known only from a large cardinal hypothesis, a supercompact cardinal. It decides many questions of combinatorial set theory, and it implies that $2^{\aleph_0} = \aleph_2$.