---
tag: VY0F6FAA5S
kind: statement
role: theorem
name: The Fundamental Theorem of Proper Forcing
sources:
  - wikipedia: en:6250799@r1306783118
    locator: Proper forcing axiom, section The Fundamental Theorem of Proper Forcing
    note: adopted
    mention: wikipedia://en/6250799#JAAP
    sections: [Statement]
inventory: [P8Z1CH3DVR]
---

## Statement

The Fundamental Theorem of Proper Forcing, due to Shelah, states that any countable support iteration of proper forcings is itself proper. This follows from the Proper Iteration Lemma, which states that whenever $(P_\alpha)_{\alpha\leq\kappa}$ is a countable support forcing iteration based on $(Q_\alpha)_{\alpha<\kappa}$ and $N$ is a countable elementary substructure of $H_\lambda$ for a sufficiently large regular cardinal $\lambda$, and $P_\kappa\in N$ and $\alpha\in \kappa\cap N$ and $p$ is $(N,P_\alpha)$-generic and $p$ forces $q\in P_\kappa/G_{P_\alpha}\cap N[G_{P_\alpha}]$, then there exists $r\in P_\kappa$ such that $r$ is $N$-generic and the restriction of $r$ to $P_\alpha$ equals $p$ and $p$ forces the restriction of $r$ to $[\alpha,\kappa)$ to be stronger or equal to $q$.

This version of the Proper Iteration Lemma, in which the name $q$ is not assumed to be in $N$, is due to Schlindwein.

The Proper Iteration Lemma is proved by a fairly straightforward induction on $\kappa$, and the Fundamental Theorem of Proper Forcing follows by taking $\alpha=0$.