Proper forcing axiom

Statement

A forcing or partially ordered set P is proper if for all regular uncountable cardinals λ , forcing with P preserves stationary subsets of [ λ ] ω .

The proper forcing axiom asserts that if P is proper and D_α is a dense subset of P for each α<ω₁, then there is a filter G ⊆ P such that D_α ∩ G is nonempty for all α<ω₁.

The class of proper forcings, to which PFA can be applied, is rather large. For example, standard arguments show that if P is ccc or ω-closed, then P is proper. If P is a countable support iteration of proper forcings, then P is proper. Crucially, all proper forcings preserve ℵ 1 .

Consequences

PFA directly implies its version for ccc forcings, Martin's axiom. In cardinal arithmetic, PFA implies 2 ℵ 0 = ℵ 2 . PFA implies any two ℵ 1 -dense subsets of R are isomorphic, any two Aronszajn trees are club-isomorphic, and every automorphism of the Boolean algebra P ( ω ) /fin is trivial. PFA implies that the Singular Cardinals Hypothesis holds. An especially notable consequence proved by John R. Steel is that the axiom of determinacy holds in L(R), the smallest inner model containing the real numbers. Another consequence is the failure of square principles and hence existence of inner models with many Woodin cardinals.

Consistency strength

If there is a supercompact cardinal, then there is a model of set theory in which PFA holds. The proof uses the fact that proper forcings are preserved under countable support iteration, and the fact that if κ is supercompact, then there exists a Laver function for κ .

It is not yet known how much large cardinal strength comes from PFA.

Other forcing axioms

The bounded proper forcing axiom (BPFA) is a weaker variant of PFA which instead of arbitrary dense subsets applies only to maximal antichains of size ω₁. Martin's maximum is the strongest possible version of a forcing axiom.

Forcing axioms are viable candidates for extending the axioms of set theory as an alternative to large cardinal axioms.

The Fundamental Theorem of Proper Forcing

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 α : α ≤ κ ⟩ is a countable support forcing iteration based on ⟨ Q α : α < κ ⟩ and N is a countable elementary substructure of H λ for a sufficiently large regular cardinal λ , and P κ ∈ N and α ∈ κ ∩ N and p is ( N , P α ) -generic and p forces " q ∈ P κ / G P α ∩ N [ G P α ] ," then there exists r ∈ P κ such that r is N -generic and the restriction of r to P α equals p and p forces the restriction of r to [ α , κ ) 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 κ , and the Fundamental Theorem of Proper Forcing follows by taking α = 0 .