# Statement
**Proper Forcing Axiom ($\text{PFA}$)**:
for every [[proper forcing|proper]] forcing notion $(\mathbb{P},\leq)$, if $\mathcal{D}$ is a collection of $\aleph_1$ dense subsets of $\mathbb{P}$, then there is a $\mathcal{D}$-[[generic filter]] on $\mathbb{P}$.
# Consistency
Unlike [[Martin's axiom]], which is equiconsistent with $\text{ZFC}$, the $\text{PFA}$ has very high consistency strength, slightly below that of a [supercompact](Supercompact.md "Supercompact") cardinal.
**Theorem.** If there is a supercompact cardinal then there is a generic extension in which that supercompact is $\aleph_2$ and $\text{PFA}$ holds.
On the other hand, <a href="http://www.math.uni-bonn.de/people/pholy/acc_accepted.pdf" class="external autonumber">[2]</a> proves a *quasi lower bound* on the consistency strength of the $\text{PFA}$, which is at least the existence of a proper class of [[subcompact]] cardinals.
<a href="https://ac.els-cdn.com/S0001870811002635/1-s2.0-S0001870811002635-main.pdf?_tid=86c2030e-cca4-11e7-b23b-00000aab0f26&acdnat=1511039455_137e37101cda34d46bb0f195cbe43148" class="external autonumber">[3]</a> also shows that all known methods of forcing $\text{PFA}$ requires a [[Strongly compact]] cardinal, and if one wants the forcing to be proper, a supercompact is required.
Current lower bound (September 2024): $\mathrm{ZF}+\mathrm{AD}_{\mathbb{R}}$+ $\Theta$ is regular $\geq$ $\mathrm{ZFC}$ + proper class of [[Woodin]]s + proper class of [[strong]] cardinals.
# Implications
- [[Martin's Axiom]].
- $2^{\aleph_0}=\aleph_2$
- The continuum (i.e. $\aleph_2$) has the [[Tree property]].
- Every two $\aleph_1$-dense sets of reals are isomorphic.
- Failure of the [[Square principles|square principle]] $\Box_\kappa$ for every uncountable cardinal $\kappa$
- Consistency of [[Axiom of determinacy]].
- [[Open coloring axiom]]
# Statements equivalent to $\text{PFA}$
- If $\mathcal{M} = \left(M ; ∈, (R_i \mid i < ω_1) \right)$ is a transitive model, $φ(x)$ is a $Σ_1$-formula and $\mathbb{Q}$ is a proper forcing such that $\Vdash_\mathbb{Q} φ(\mathcal{M})$, then there is in $V$ a transitive $\bar{\mathcal{M}} = (\bar{M} ; ∈, (\bar{R}_i \mid i < ω_1 ))$ together with an elementary embedding $j : \bar{\mathcal{M}} → \mathcal{M}$ such that $φ(\bar{\mathcal{M}})$ holds.{% cite Bagaria2017a %}
- There is a *Laver function*