Forcing

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

A subset of a forcing order whose distinct members have no common stronger extension. A maximal forcing antichain has a compatible member for every condition. For forcing by nodes of a set-theoretic tree, ordered by extension, this coincides with a tree antichain.

A forcing collapses a ground-model cardinal $\kappa$ if it forces a bijection from a smaller ordinal onto the ground ordinal $\kappa$. The ordinal itself is preserved; its being an initial ordinal is lost.

A forcing is cofinality-preserving over a transitive model $M$ if every generic extension has the same cofinality for every ground ordinal. The values are compared as ordinals, which forcing preserves.

For a cardinal number $\kappa$, ${\mathrm{MA}}_{\kappa }$ says that for every forcing with the countable chain condition for forcing and every family of at most $\kappa$ dense subsets, some filter in an ordered set meets them all. Full Martin axiom asserts this for all $\kappa <2^{{\aleph }_0}$. The strict upper bound is part of the definition.

A forcing order that is countable inside the ground model. It has the countable chain condition and preserves ${\omega }_1$. Internal countability is distinct from external countability of the entire model.

Over a Generalized continuum hypothesis ground model, adding one Cohen real preserves every infinite power $2^{\lambda }={\lambda }^{+}$. For the countable forcing, nice subset forcing names for $\lambda$ number at most $(2^{{\aleph }_0}{)}^{\lambda }=2^{\lambda }$ in the ground model. Old subsets give the matching lower bound and the countable chain condition for forcing preserves cardinals. Starting from the constructible universe, the new real is nonconstructible while the constructible levels remain unchanged.

A ground-model Suslin tree remains Suslin after countable forcing. A new uncountable chain or antichain would contain an uncountable ground-model subset by the ground-model uncountable subset lemma for countable forcing.

An uncountable set of ground-model elements in a generic extension by countable forcing contains an uncountable ground-model subset. Partition membership witnesses according to the countably many forcing conditions.

In standard notation for forcing, an order is separative if $p\nleqq q$ implies that some $r\le p$ is incompatible with $q$. Separativity does not imply an atomless forcing order: the one-point order is separative and has a forcing atom. Its only generic filter is a ground-model set. Atomlessness is the hypothesis in generic filter for an atomless order is new.

A condition is an atom if every two stronger conditions are compatible forcing conditions. This is a compatibility definition, not necessarily minimality in an arbitrary partial order. An atomless forcing order is one in which every condition has two incompatible strengthenings.

For a forcing atom $p$ in a ground-model forcing order, $G_p$ is a ground-model generic filter. It contains $p$ and is upward closed. For $q,r\in G_p$, choose $q^{\prime }\le p,q$ and $r^{\prime }\le p,r$. The atom property gives $s\le q^{\prime },r^{\prime }$, so $s\in G_p$ is a common strengthening of $q,r$. Thus $G_p$ is a filter in an ordered set. Every dense subset of a forcing order has some $d\le p$, and $d\in G_p$. The defining compatibility predicate is bounded to the ground-model set of conditions, so axiom schema of separation forms $G_p$ inside the ground model. For a nonminimal atom, this filter can strictly contain the principal filter above $p$.

An order is atomless if it has no forcing atom, equivalently every condition has a pair of incompatible forcing conditions below it. For a fixed order belonging to a transitive model, this property is absolute because its quantifiers range over the unchanged set of conditions. Infinite-domain Fn forcing with at least two possible values is atomless: prescribe different values at one fresh coordinate.

If a generic filter $G$ for an atomless forcing order belonged to its ground model, then the complement $\mathbb{P}\setminus G$ would be a dense ground-model set. A condition outside $G$ is already there; a condition in $G$ has two incompatible strengthenings, at least one outside its directed filter. Genericity would then require meeting the complement, a contradiction.

The conditions are pairs with coordinatewise extension: $(p,q)\le (p^{\prime },q^{\prime })$ exactly when $p\le p^{\prime }$ and $q\le q^{\prime }$. The projection of a product-generic filter is a pair of factor filters whose Cartesian product is the original filter. Each is ground-model generic, and mutual genericity for product forcing makes the second generic over the extension by the first.

If $H=G_0\times G_1$ is generic for product forcing over $M$, then $G_1$ is generic over $M[G_0]$. For a name $\dot{D}$ for a dense subset of the second factor, take $p_0\in G_0$ forcing density. Ground-model pairs with first coordinate incompatible with $p_0$, or with first coordinate below $p_0$ forcing the second into $\dot{D}$, form a dense product set. The existential clause of syntactic forcing and the membership clause for a canonical forcing name give the density witnesses. The product filter meets this set, cannot use the incompatible case, and hence its second projection meets ${\dot{D}}^{G_0}$.

For a generic filter $H$ in product forcing, let $G_0,G_1$ be its coordinate projections. They are filters in an ordered set. Given $p\in G_0$ and $q\in G_1$, choose separate pairs witnessing their membership and then a common strengthening in $H$. Upward closure puts $(p,q)$ in $H$, proving the displayed equality. Every ground-model dense factor set lifts to a dense product set, proving genericity of each projection over the ground model.

A condition consists of a finite sequence and an infinite reservoir of allowed future values. A stronger condition extends the sequence, shrinks the reservoir, and takes all newly appended values from the old reservoir. Stem values may repeat. The union of the generic stems is an unbounded real over a model: for every ground-model function $g$ and every threshold $K$, the conditions whose stem already has some $k\ge K$ with $g(k)<s(k)$ form a dense subset of a forcing order. An infinite subset of $\omega$ always supplies a sufficiently large value.

A function $f\in {\omega }^{\omega }$ is unbounded over a model $M$ if for every $g\in M\cap {\omega }^{\omega }$, infinitely many $k$ satisfy $g(k)<f(k)$. Equivalently, no ground-model function eventually dominates it. This is weaker than being a dominating real over $M$.

A forcing order preserves cardinals over a ground model if every ground-model cardinal number remains a cardinal in every generic extension. This assertion and any sufficient chain condition for forcing are evaluated inside the ground model. External countability of a countable transitive model does not make all of its forcing orders internally ccc.

A forcing name is a recursively built set of pairs $(\sigma ,p)$, where $\sigma$ is a lower-rank forcing name and $p$ is a forcing condition. Ground-model names are interpreted using a generic filter to form the generic extension.

The ordinal assigned recursively by $\mathrm{nrk}(\tau )=\sup \{\mathrm{nrk}(\sigma )+1:(\sigma ,p)\in \tau \}$. It measures dependency on subnames and justifies generic evaluation by recursion. The ordinary rank of a set also accounts for the coding of the ordered pairs and the forcing conditions; it need not equal this dependency rank of a set.

If the ground model has axiom of choice, well-order the set of subnames appearing in a forcing name for an arbitrary extension set. Evaluate those activated by the generic filter. Each element of the extension set has a least preimage index; ordering by these indices well-orders the set. Only ground choice and the ZF part of the forcing theorem are needed.

A name for a subset of a ground-model set, given coordinatewise by antichains in a forcing order. For countable-chain-condition forcing, each coordinate uses a countable antichain, which bounds the number of names for reals.

For the condition-first forcing name convention, pair every condition with each of two names $\tau ,{\tau }^{\prime }$. Under any nonempty generic filter, the evaluation of a forcing name is then $\{{\tau }_G,{\tau }_G^{\prime }\}$, the unordered pair of the two values. Equal values give a singleton. With the name-first convention, reverse the two components of each syntactic pair.

The forcing name $\{(\check{p},q):p,q\in \mathbb{P},q\perp p\}$ evaluates to $\mathbb{P}\setminus G$. If $p\notin G$, genericity applied to $\{q:q\le p\text{ or }q\perp p\}$ supplies an incompatible member of $G$. If $p\in G$, directedness prevents such a member.

Interpret a forcing name recursively by $\mathrm{val}(\tau ,G)=\{\mathrm{val}(\sigma ,G):\exists p\in G((\sigma ,p)\in \tau )\}$. The collection of interpreted ground-model names is the generic extension.

The canonical forcing name for a ground-model set $x$ is $\check{x}=\{(\check{y},1):y\in x\}$. Its evaluation of a forcing name under every generic filter is $x$.

For an infinite ground-model cardinal number $\kappa$, use finite partial functions from $\omega$ to $\kappa$, ordered by reverse inclusion. The union of a generic filter is a surjection $\omega \to \kappa$. The order has size $\kappa$, hence the ${\kappa }^{+}$-chain condition, and preserves cardinals at least ${\kappa }^{+}$.

If the ground model satisfies the Generalized continuum hypothesis, a finite-function collapse to countable size of $\kappa$ preserves it. The old ${\kappa }^{+}$ becomes the new ${\aleph }_1$, and there are at most $2^{\kappa }={\kappa }^{+}$ names for subsets of $\omega$. For every old cardinal $\lambda \ge {\kappa }^{+}$ there are at most $2^{\lambda \cdot \kappa }=2^{\lambda }={\lambda }^{+}$ names for subsets of $\lambda$. Cardinal preservation by chain-condition forcing and Cantor theorem turn these upper bounds into the required equalities.

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 $P$ is dense if every $p\in P$ has a stronger condition $q\le p$ in $D$. This order-density condition is the one used by a generic filter; it is distinct from density in an arbitrarily specified topology.

For the convention that larger conditions are stronger, density above $p$ means every strengthening of $p$ has a further strengthening in $D$. It is the extension-cone density usually called dense below a forcing condition when smaller conditions are stronger. The sign must be translated with the order convention, rather than copied unchanged.

A set $D\subseteq \mathbb{P}$ is dense below $p$ when every $q\le p$ has an extension $r\le q$ belonging to $D$.

If $p\in G$ and a ground-model set $D$ is dense below a forcing condition $p$, then the generic filter $G$ meets $D$. Add all incompatible forcing conditions with $p$ to $D$. The enlarged set is globally dense: a condition compatible with $p$ first has a common strengthening, then a further strengthening in $D$. Genericity meets the enlargement, and directedness excludes its incompatible part.

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

A filter is generic over its ground model exactly when it meets each ground-model maximal forcing antichain in one point. Extensions of a maximal antichain form a dense set, while any ground dense set contains an antichain maximal in the whole forcing. Directedness permits at most one antichain member in a filter.

If $M$ is a countable transitive model, $\mathbb{P}\in M$, and $p\in \mathbb{P}$, enumerate the dense subsets of $\mathbb{P}$ belonging to $M$ and recursively choose a decreasing sequence starting below $p$ that meets each one. Its upward closure is a generic filter over $M$ containing $p$.

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$.

Let $M_{n+1}=M_n[G_n]$ for a fixed atomless forcing order $\mathbb{P}$, and $N={\bigcup }_{n<\omega }{M}_n$. If a set $A\in N$ were its internal power set of $\mathbb{P}$, choose $n$ with $A\in M_n$. The next generic filter $G_n$ belongs to $N$, so $G_n\in A$; transitivity of $M_n$ implies $G_n\in M_n$, contradicting generic filter for an atomless order is new. The chain is increasing but need not be an elementary chain.

For a forcing name $\tau$, let $U$ consist of pairs $(\rho ,p)$ where $(\rho ,r)\in \tau$ for some $r\ge p$. Every ground-model subset $\nu$ of $U$ is a name whose value is contained in ${\tau }^G$. Every subset ${\sigma }^G\subseteq {\tau }^G$ has an equivalent such name: retain those $(\rho ,p)\in U$ with $p⊩\rho \in \sigma$. The atomic membership truth lemma for forcing proves equality of values. Collect all these names from the ground-model power set ${\mathcal{P}}^M(U)$ into a single outer name, pairing each with every condition. Its value is the full internal power set, without presupposing that power set in the extension.

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.

For a name with finitely many possible values, record which value each condition forces, using an extra marker for undecided conditions. Equal patterns mean that any condition deciding one entry decides all entries with that pattern identically.

A generic extension of a transitive model has exactly the same ordinals as its ground model. Rank induction on names bounds every value; transitivity and agreement on membership make ordinalhood absolute.

A formula holds in a generic extension exactly when some condition in the generic filter forces it for names of its parameters.

For each formula, its forcing relation on names and conditions is uniformly first-order definable inside the ground model. This permits ground-model separation and replacement using forcing predicates.

For a countable transitive model $M$, semantic forcing declares $p⊩\phi$ when every generic filter $G$ over $M$ containing $p$ gives $M[G]\models \phi$.

The syntactic forcing relation is defined recursively inside the ground model from the ranks of forcing names and the logical complexity of $\phi$. The forcing theorem proves that it agrees with the semantic forcing relation.

For forcing names $\sigma ,\tau$ and a generic filter $G$, ${\sigma }^G\in {\tau }^G$ exactly when some $p\in G$ syntactically forces $\sigma \in \tau$. Assuming the equality truth lemma, interpreted membership supplies an active pair $(\rho ,r)\in \tau$ and a condition in $G$ forcing $\sigma =\rho$; a common strengthening forces membership. Conversely the defining equality witnesses occur dense below a forcing condition forcing membership. The dense-below generic meeting lemma supplies one in $G$, and the equality truth lemma recovers interpreted membership.

For the usual recursive syntactic forcing relation, $p{⊩}^{\ast }\exists x\phi (x)$ means that conditions $q\le p$ forcing $\phi (\sigma )$ for some forcing name $\sigma$ are dense below a forcing condition $p$. This density clause proves the existential step of the forcing theorem from the truth lemma for each named instance. A generic filter containing $p$ meets that dense set after it is augmented by conditions incompatible with $p$.

Let $\dot{x},{\dot{a}}_1,\dots ,{\dot{a}}_n$ be forcing names and let $\phi$ be a formula. The namebelongs to the ground model by axiom schema of separation. The forcing theorem shows that its value in a generic extension is exactlyConsequently every generic extension satisfies the separation schema.

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.

A countable transitive model is in particular a standard model (set theory) with both countability and transitivity.

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.

Over a model of Generalized continuum hypothesis, add ${\aleph }_3$ Cohen reals with finite binary partial functions. The Delta-system lemma proves the countable chain condition for forcing. The generic reals give the continuum lower bound ${\aleph }_3$, while nice forcing names for subsets of ${\omega }_1$ number at most $({\aleph }_3{)}^{{\aleph }_1}={\aleph }_3$ in the ground model. Cardinal preservation then gives $2^{{\aleph }_0}=2^{{\aleph }_1}={\aleph }_3$.

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.

The order $\mathrm{Fn}(X,Y,\omega )$ has the countable chain condition for forcing whenever $Y$ is countable. For an uncountable family of conditions, apply the Delta-system lemma to the finite domains. On their common finite root there are only countably many assignments, so thin to an uncountable family agreeing on that root. Any two conditions now have a compatible union. For binary Cohen forcing, there are only finitely many root assignments.

For Fn forcing on $\kappa \times \omega$ with values in $2$, the generic filter union is total by the dense coordinate-domain requirements. For each pair of distinct rows, the set of conditions giving them opposite bits at some column is dense: choose a column untouched in both finite rows. Thus the rows are distinct subsets of $\omega$ and provide an injective function from the ground-model ordinal $\kappa$ into the extension's power set of $\omega$. This construction alone does not prove preservation of its ground-model cardinal number status.

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

If forcing has the $\kappa$-chain condition for a regular uncountable $\kappa$, every forced club subset of $\kappa$ contains a ground-model club below the forcing condition. Bound the possible witnesses above each ordinal using antichains, then take closure points of the bound function.

Suppose $\mathbb{P}$ has the $\kappa$-chain condition and $\dot{f}$ is forced to be a function from an ordinal $\mu$ to an ordinal $\lambda$. For each $\xi <\mu$, a maximal antichain in a forcing order deciding $\dot{f}(\xi )$ has size below $\kappa$. Hence the ground model has a set $B_{\xi }\subseteq \lambda$ of size below $\kappa$ containing every possible value of $\dot{f}(\xi )$.

If $\kappa$ is a regular cardinal and $\mathbb{P}$ has the $\kappa$-chain condition, then forcing with $\mathbb{P}$ preserves every cardinal number and cofinality at least $\kappa$. Indeed, a proposed surjection $f:\mu \to \lambda$ with $\mu <\lambda$ has its range contained in ${\bigcup }_{\xi <\mu }{B}_{\xi }$ from the possible-values lemma for chain-condition forcing. The regularity of $\kappa$ and infinite cardinal arithmetic make this union have cardinality below the ground-model cardinal $\lambda$, a contradiction.

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$.

Every uncountable subset of a Knaster forcing has an uncountable pairwise compatible subset. The property implies the countable chain condition for forcing. Finite Cohen forcing has this property by the delta-system lemma and agreement on the finite root. A Knaster forcing times any CCC forcing is CCC

If $T$ is a normal splitting Suslin tree and $P$ is Knaster, then $P\times T$ is CCC, so $P$ forces that the ground tree is still CCC Countable levels and splitting persist. A new cofinal branch would give an uncountable antichain by splitting, so none is added. This permits adding many Cohen reals while retaining a Suslin tree, and distinguishes Knaster preservation from an unjustified preservation claim for every CCC forcing.

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.

If a forcing is $\kappa$-closed in the ground model, then it adds no functions from a ground ordinal $\alpha <\kappa$ into a ground set $B$. Recursively decide each value inside the ground model and take common stronger bounds at limit stages and after the final step. Conditions deciding a whole ground function are dense below any condition asserting this type of function. The dense-below generic meeting lemma ensures the generic filter meets that dense subset of a forcing order. One arbitrary bound need not be in the filter in an ordered set.

Every descending countable sequence of conditions has a common stronger condition. This is ${\omega }_1$-closed forcing and adds no countable ordinal sequences.

Conditions are countable successor-length sequences $⟨A_{\xi }\subseteq \xi ⟩$, ordered by end extension. A countable fusion construction decides a named subset below a fresh limit index and writes that trace at the index inside any named club. The generic sequence satisfies the diamond principle.

Countable partial functions from ${\omega }_1$ to a nonempty ground-model set $A$, ordered by extension, add a surjection ${\omega }_1\to A$. Countable closure preserves ${\omega }_1$ and adds no reals.

If a ground-model order is $\lambda$-closed, it adds no ordinal-valued functions with domain $\mu <\lambda$. Recursively decide each name value inside the ground model, using closure at intermediate limit stages and once more at the end. Below each starting condition, conditions deciding the entire function are dense. A generic filter meets them by the dense-below generic meeting lemma. The recursion must be internal to the ground model, since its closure property only covers its own sequences.

A $\lambda$-closed forcing order preserves a ground-model cardinal number $\lambda$, even when it is singular. A proposed surjection from an ordinal below $\lambda$ to $\lambda$ would be an old function because closed forcing adds no short ordinal sequences, contradicting old cardinalhood. This concerns $\lambda$ and smaller cardinals; closure alone does not supply preservation of all larger cardinals.

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.

The finite-condition Lévy collapse $\mathrm{Lv}(\kappa )$ consists of finite partial functions $p$ with $\mathrm{dom}p\subseteq \kappa \times \omega$ and $p(\alpha ,n)<\alpha$, ordered by reverse inclusion. The generic union gives a surjection $\omega \to \alpha$ for every infinite $\alpha <\kappa$. If $\kappa$ is regular and uncountable, the Delta-system lemma at a regular uncountable cardinal proves the $\kappa$-chain condition, so the extension makes $\kappa ={\aleph }_1$.

With $\kappa$ an uncountable regular cardinal, finite partial functions on $\kappa \times \omega$ assigning a value below the first coordinate collapse every ground ordinal below $\kappa$ to countable size. The Delta-system lemma gives the $\kappa$ chain in a partial order condition; the possible-values lemma for chain-condition forcing then preserves the regularity of $\kappa$. Therefore $\kappa$ becomes the extension ${\omega }_1$. Strong inaccessibility is enough but is not needed for this identification.

For a regular uncountable $\kappa$, the finite-condition collapse has the $\kappa$ chain in a partial order condition, by a regular-cardinal Delta-system lemma and thinning to identical assignments on the finite root. Thus every maximal forcing antichain has ground-model size less than $\kappa$. There is no fixed size: for any nonzero cardinal $\mu <\kappa$, assigning all values below $\mu$ at the one coordinate $(\mu ,0)$ is a maximal forcing antichain of size $\mu$.