Proper forcing axiom

Definition

Partial orders, dense sets and filters are as in Martin's axiom. For an uncountable set $\lambda$, let $[\lambda]^{\omega}$ be the set of countable subsets of $\lambda$. A set $C \subseteq [\lambda]^\omega$ is club if both conditions hold. It contains the union of each increasing sequence $x_0 \subseteq x_1 \subseteq \cdots$ of its members. Each countable subset of $\lambda$ is contained in a member of $C$. A set $S \subseteq [\lambda]^\omega$ is stationary if it meets each club subset of $[\lambda]^\omega$. A partial order $P$ is proper if forcing with $P$ preserves stationarity: for each uncountable $\lambda$, each stationary $S \subseteq [\lambda]^\omega$ stays stationary in the generic extension. The proper forcing axiom, PFA, is the following statement. Let $P$ be a proper partial order, and let $\mathcal{D}$ be a family of at most $\aleph_1$ dense subsets of $P$. Then some filter on $P$ meets every member of $\mathcal{D}$.