---
tag: 35XTXNEWQ9
kind: concept
name: Proper forcing axiom
msc: ["03E57", "03E50"]
sources:
  - url: https://en.wikipedia.org/wiki/Proper_forcing_axiom
same_as:
  wikidata: Q749043
  wikipedia: Proper forcing axiom
---

## Summary

The proper forcing axiom, PFA, is a strong extension of [[Martin's axiom|V8KGT8MRFE]] 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|KJT0AXWQXP]] 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$.

## Explanations

### L1 human

A forcing axiom says that certain constructions of length $\omega_1$ can always be completed.
Martin's axiom allows this for a narrow class of construction methods, the ccc ones.
The proper forcing axiom allows it for a much wider class, the proper ones, which include all ccc methods and all countably closed ones.
With this freedom, many open-ended questions about sets of size $\aleph_1$ get definite answers.