Forcing

Forcing extends a model of set theory by adjoining a filter generic for a partially ordered set of finite or otherwise controlled approximations.

In standard forcing notation, $q\le p$ says that $q$ is stronger than $p$: the smaller condition carries more information.

In Jerusalem notation, $p\le q$ says that $q$ is stronger than $p$: the larger condition carries more information.

Two forcing conditions are compatible when they have a common stronger extension. In standard notation this means that some $r$ satisfies $r\le p,q$; in Jerusalem notation for forcing it means that some $r$ satisfies $p,q\le r$.

Two forcing conditions are incompatible when they have no common stronger extension.

A subset $D$ of a forcing order $\mathbb{P}$ is dense when every $p\in \mathbb{P}$ has a stronger extension $q\le p$ in $D$.

A filter $G\subseteq \mathbb{P}$ is generic over a model $M$ when it meets every dense subset of $\mathbb{P}$ belonging to $M$.

If $G$ is a generic filter over a countable transitive model $M$, the generic extension $M[G]$ consists of the interpretations by $G$ of all forcing names in $M$.

The forcing theorem identifies truth in a generic extension with the forcing relation: a formula is true in $M[G]$ exactly when some condition in $G$ forces it.

A countable transitive model is a countable set $M$ such that membership on $M$ is the actual membership relation, $M$ is transitive, and $(M,\in )$ satisfies the specified axioms of set theory.

Cohen forcing consists of finite partial approximations to a new subset or function, ordered by reverse inclusion. Meeting the ground-model dense sets makes the union a total generic object.

An eventually different condition is a finite sequence together with finitely many ground-model functions that all newly appended coordinates must avoid. The generic union eventually differs from every ground-model function.

The order $\mathrm{Fn}(X,Y,\kappa )$ consists of partial functions $p:X\rightharpoonup Y$ with $|\mathrm{dom}p|<\kappa$, ordered by reverse inclusion so that larger functions are stronger conditions.

A forcing order has the $\kappa$-chain condition when every antichain has cardinality below $\kappa$. It preserves cardinals and cofinalities at least $\kappa$.

A forcing order has the countable chain condition when every antichain in a forcing order is countable. Such forcing preserves cardinals and cofinalities at least ${\aleph }_1$.

A forcing order is $\kappa$-closed when every decreasing sequence of conditions of length below $\kappa$ has a lower bound. Countably closed forcing adds no new countable sequences of ground-model elements and in particular adds no new real numbers.

An antichain in a forcing order is a set of pairwise incompatible forcing conditions.

A subset of a forcing order is centered when every finite collection of its conditions has a common stronger extension.

A forcing order is sigma-centered when it is the union of countably many centered subsets. Every sigma-centered forcing has the countable chain condition for forcing.

A Hechler condition is a pair $(s,f)$ consisting of a finite sequence $s\in {\omega }^{<\omega }$ and a function $f\in {\omega }^{\omega }$. An extension lengthens the stem, increases the side function, and places every new stem value above the old side function. The generic union is a dominating real.

A function $d\in {\omega }^{\omega }$ dominates $h\in {\omega }^{\omega }$ when $d(n)>h(n)$ for all but finitely many $n$. A dominating real over a ground model dominates every such function belonging to that model.

For a forcing order with the countable chain condition for forcing, a real can be represented by a nice name determined by a countable antichain in a forcing order for each natural-number coordinate. This bounds the number of reals in the extension in terms of the size of the forcing order.