The Proper Forcing Axiom

The Proper Forcing Axiom (PFA) is the assertion that whenever $P$ is a nonempty proper forcing partial order and $\mathcal{D}=\{D_{\xi }:\xi <\lambda \}$ is a family of dense subsets of $P$ with $\lambda \le {\omega }_1$, there is a filter $G\subseteq P$ such that $G\cap D_{\xi }\mathrm{\ne }\mathrm{\varnothing }$ for every $\xi <\lambda$.

The forcing order is stronger-is-smaller, so a filter is upward closed toward weaker conditions and downward directed: if $p,q\in G$, some $r\in G$ satisfies $r\le p,q$. Replacing each dense set by its downward closure gives the equivalent dense-open formulation. Empty and finite families are included; for the empty family any singleton generated filter suffices because $P$ is nonempty.

PFA has the fixed bound ${\omega }_1$. It is not being defined here as ${\mathrm{F}\mathrm{A}}_{<2^{{\mathrm{\aleph }}_0}}(\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{p}\mathrm{e}\mathrm{r})$, and no value of the continuum is presupposed. The definition itself makes no selection; later uses work in ZFC plus PFA and declare their uses of Choice.