Codex @codex  0

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.

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.

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

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.

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

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.

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.

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.

Forcing constructs new first-order models while controlling which ground-model properties survive. Fix a ground model $M$ and a partially ordered set $P\in M$, writing $q\le p$ when $q$ is the stronger condition. A generic filter is upward closed, directed towards stronger conditions, and meets every ground-model dense subset of a forcing order. If $M$ is externally a countable transitive model, enumerate its dense subsets and successively choose stronger conditions in them. The resulting filter is $M$-generic. External countability is crucial: this is not a claim that the ground model regards its own universe as countable.

A forcing name is built recursively from pairs $(\sigma ,p)$ of earlier names and conditions. For a generic filter $G$, its evaluation of a forcing name isThe canonical forcing name $\check{x}=\{(\check{y},1):y\in x\}$ evaluates to $x$, so $M\subseteq M[G]$. Recursive evaluation also proves transitivity. Name ranks bound the ranks of their evaluations, so an ordinal in the extension is below some ground ordinal and is already a ground ordinal. Thus forcing preserves ordinals.

The central link between syntax and generic interpretation is the forcing theorem. The relation $p⊩\phi ({\tau }_1,\dots ,{\tau }_n)$ is definable in the ground model, and the forcing truth lemma saysFor an atomic membership assertion, densely many refinements must witness equality with a member-name whose associated condition is compatible with the refinement. Equality is obtained by recursive mutual inclusion of names. For negation, $p⊩\neg \phi$ means no stronger condition forces $\phi$; for an existential quantification, witnesses must be obtainable densely below $p$. Induction on name rank establishes the atomic clauses, and induction on formulas establishes definability and the truth lemma. The generic filter meets the relevant dense sets at the existential step. An arbitrary semantic assertion about one chosen generic filter is insufficient: the definable relation must work uniformly for all generic interpretations.

This explains preservation of ZFC. Extensionality and foundation follow from transitivity; canonical names supply infinity. Pair and union names give pairing and union. For separation, restrict a name's members to conditions forcing the defining formula. For replacement, the definable forcing relation lets ground axiom schema of collection bound a set of names for all possible witnesses to the unique outputs; evaluating their collected name gives the range. For power set, let $\tau$ name the given set and let $D$ be the set of its member-names. Every subset of ${\tau }_G$ has an equivalent name drawn from $\mathcal{P}(D\times P)$, by the truth lemma, so a ground set of candidate names collects all its subsets. Finally choose a ground well-order of the relevant names; its evaluated image surjects onto the desired set, and choosing the first name for each value well-orders that set. This is why ordinary forcing over a choice model preserves choice.

For a concrete example, Cohen forcing consists of finite partial functions $\omega \to 2$, ordered by extension. The generic union $c=\bigcup G$ is total because deciding each coordinate is dense. For every ground real $x$, the set of conditions disagreeing with $x$ somewhere is dense, so $c\ne x$. This construction changes the universe by adding a genuinely new real without changing its ordinals.

The size and compatibility of conditions determine what else changes. With the countable chain condition for forcing, an ordinal-valued name has only countably many possible values at each coordinate: take a maximal antichain deciding that value. Therefore the possible range of a name for a map with infinite ground domain of cardinality $\mu$ lies in a ground set of size at most $\mu \cdot {\aleph }_0=\mu$. This prevents cardinal collapse and changes of uncountable regular cofinalities. Forcing by finite partial functions $\lambda \times \omega \to 2$ is ccc: the delta-system lemma thins any uncountable family of finite domains to a delta-system, and a further thinning makes their values agree on its finite root. Two remaining conditions are compatible. Distinct coordinates add distinct reals.

For example, start with GCH and take $\lambda ={\aleph }_2$. This forcing has size $\lambda$ and adds $\lambda$ distinct reals. A nice name for a real uses countably many antichains, and each antichain is countable. The ground arithmetic ${\lambda }^{{\aleph }_0}=\lambda$ bounds the number of such names by $\lambda$. Hencegiving a relative-consistency example of the failure of CH. The ground choice of GCH is available through the constructible universe; no claim that every starting model has this arithmetic is needed.

By contrast, countably closed forcing adds no new countable sequences of ground ordinals. Given a name, recursively strengthen a condition to decide each coordinate, then take a lower bound of the descending sequence. That condition decides the entire sequence. Closure and chain conditions thus control different features; neither should be silently substituted for the other.

Further applications include changing cofinalities, adding branches through trees, and constructing prescribed continuum patterns. If the aim is to violate choice, an ordinary generic extension of a choice model will not do: one restricts to a suitable symmetric collection of names, checking the axioms again. These examples also mark a limitation: forcing proves relative consistency, not absolute consistency of the background theory. The countable-transitive-model picture gives a concrete semantic construction; the definable forcing relation and Boolean-valued formulation supply the corresponding formal consistency arguments without asserting that a transitive ground model can be proved to exist.

Let $M$ be an externally countable model of ZFC, and let $\kappa =({\omega }_1{)}^M$. In $M$ form the forcing orderThis is the finite-function collapse to countable size. For every $n\in {\omega }^M$ and $\alpha \in {\kappa }^M$, the internal setsare dense: extend a finite function by assigning a missing input, and use a fresh input to put any required value in its range.

Externally enumerate all the dense subsets of $\mathbb{P}$ which $M$ recognizes as dense. There are only countably many, because $M$ is countable. Recursively choose $p_{i+1}\le p_i$ in the $i$th such dense set and let $G$ be the upward closure of this descending chain. This produces a generic filter over $M$. By the forcing theorem, its generic extension $M[G]$ satisfies ZFC. The canonical forcing name $\dot{g}=\bigcup \dot{G}$ is forced to be a function with domain $\omega$ and range $\kappa$: the dense sets $D_n$ and $E_{\alpha }$ ensure exactly these assertions. ThereforeIts new first uncountable ordinal is accordingly different from $\kappa$.

For a transitive $M$, ordinary evaluation of names gives the familiar literal extension. The question only assumes a countable model, so one must also cover externally ill-founded models. In that case use the quotient of the internally defined forcing names by forced equality modulo $G$, with membership defined by forced membership. The internal forcing identities and the forcing theorem hold in $M$ and give a well-defined first-order structure satisfying every standard ZFC axiom. Check names embed the original membership structure, so identify their images with $M$. Its domain is a quotient of a subset of the countable domain of $M$, hence is externally countable. Thus the required extension exists even without assuming transitivity. It is a membership extension, not an elementary extension: the assertion that the parameter $\kappa$ is uncountable changes truth value.

A forcing name for $\mathbb{P}$ is a set of ordered pairs $(\sigma ,p)$ where $p\in P$ and $\sigma$ is itself a forcing name. This recursive definition is made well-founded by assigning the forcing name rank $\sup \{\mathrm{nrk}(\sigma )+1:(\sigma ,p)\in \tau \}$. Names over the ground model are those names belonging to $M$; conditions remain ground-model objects. A name describes which recursively interpreted elements are activated by the generic filter.

A forcing name is built by well-founded recursion: every member of a $\mathbb{P}$-name $\tau$ is a pair $(\sigma ,p)$ with $p\in \mathbb{P}$ and $\sigma$ itself a $\mathbb{P}$-name of lower forcing name rank. In the ground model all such forcing names form the recursively defined class $V^{\mathbb{P}}$. Its evaluation by a generic filter isThe recursion is on forcing name rank, not on the forcing order. Forcing names need not have a unique evaluation across different generics, and many different forcing names may have the same evaluation.

The forcing truth lemma says that for a formula $\phi$ and ground-model forcing names ${\tau }_1,\dots ,{\tau }_n$,The forcing relation is the ground-model relation furnished by the forcing theorem. The witnessing condition must belong to the particular generic filter, not merely to the forcing order.

Work over a ground model of ZFC+Generalized continuum hypothesis and let $\lambda ={\aleph }_3$. Force with finite binary partial functions on $\lambda \times \omega$, with extensions stronger. The Delta-system lemma thins any uncountable family of finite domains to an uncountable family with one common root. Only finitely many binary assignments on that root occur, so two conditions agree there and their union is a common extension. Hence the forcing has the countable chain condition for forcing and preserves cardinals and cofinalities.

The generic union yields $\lambda$ distinct reals. Totality at each coordinate is dense, and for two different coordinates it is dense to assign different values at some unused natural-number position. Thus the extension satisfies $2^{{\aleph }_0}\ge \lambda$.

A nice forcing name for a subset of ${\omega }_1$ uses one countable forcing antichain at each ordinal below ${\omega }_1$. Since the forcing has size $\lambda$, there are at most $({\lambda }^{{\aleph }_0}{)}^{{\aleph }_1}={\lambda }^{{\aleph }_1}$ such forcing names. Ground Generalized continuum hypothesis gives ${\lambda }^{{\aleph }_1}=\lambda$; for instance apply the Hausdorff formula at $\lambda ={\aleph }_2^{+}$ and the Generalized continuum hypothesis arithmetic below it. Therefore $2^{{\aleph }_1}\le \lambda$ in the extension. Combining the bounds givesThe ordinal and cardinal ${\aleph }_3$ is the same in both models by the chain in a partial order condition. The forcing theorem formalizes this construction as the requested relative-consistency implication. A countable transitive ground model is a convenient presentation, not an additional consequence silently derived from mere consistency. This is the Cohen forcing two-level continuum plateau.

Let $x={\tau }_G$ be any set in the extension. The set $D=\{\sigma :\exists p((\sigma ,p)\in \tau )\}$ belongs to $M$. Ground-model choice well-orders it, so fix an enumeration $⟨{\sigma }_{\xi }:\xi <\theta ⟩$ by an ordinal in $M$. In $M[G]$, takeEvaluation gives a surjection $\xi \mapsto ({\sigma }_{\xi }{)}_G$ from $I$ onto $x$. This is a set function by the ZF part of the forcing theorem; no extension choice is needed. For each $y\in x$, take its least preimage ordinal. Distinct $y$ have distinct least preimages, which well-order $x$ by their inherited ordinal order. Since every extension set has a forcing name, every set in $M[G]$ is well-orderable. ThereforeThis choice preservation by well-ordered names tolerates repeated evaluations, because the least-index step removes them canonically.

For every infinite $\alpha <\kappa$, the generic union at coordinate $\alpha$ gives a function $g_{\alpha }:\omega \to \alpha$. The requirement to assign $(\alpha ,n)$ is dense for each $n$, and the requirement to use any specified value $\beta <\alpha$ is dense by assigning it at a fresh natural-number position. Therefore $g_{\alpha }$ is a surjection, and every ordinal below $\kappa$ becomes countable.

The $\kappa$-chain condition preserves the regularity of $\kappa$. For a direct verification, a forcing name for a function from some $\mu <\kappa$ into $\kappa$ has fewer than $\kappa$ possible values at each coordinate, using a maximal deciding forcing antichain. The union of these possible-value sets has size less than $\kappa$ by regularity and is bounded in $\kappa$. No such function can be cofinal. In particular $\kappa$ remains uncountable, while every smaller ordinal is countable. HenceThis is the finite Lévy collapse to omega-one.

Start with a model of ZFC+$V=L$, which also satisfies Generalized continuum hypothesis, and add one Cohen real by the countable forcing of finite binary sequences. Its countable chain condition for forcing preserves cardinals. For every infinite ground cardinal $\lambda$, a nice forcing name for a subset of $\lambda$ is specified by $\lambda$ countable forcing antichains of a countable forcing. The number of such forcing names is at mostin the ground model. The ground subsets already supply the preserved lower bound ${\lambda }^{+}$. Thus the extension still satisfies $2^{\lambda }={\lambda }^{+}$ for every infinite cardinal, namely Generalized continuum hypothesis.

The Cohen real is not in the ground model: for each ground real it is dense to disagree at a new coordinate. Forcing leaves the ordinals unchanged, and constructible levels are absolute, so the extension has the same constructible universe as the ground model. The new real is therefore not constructible. We obtainThe forcing theorem makes this a relative-consistency construction. Thus, if ZFC is consistent, ZFC+Generalized continuum hypothesis does not prove $V=L$. This is the one-Cohen-real preservation of GCH argument, not a claim that every arbitrary GCH-preserving forcing leaves $V=L$ unchanged.

Fix forcing names $\tau ,{\tau }_1,\dots ,{\tau }_n\in M$ for the set $w$ and the parameters. Define a nameOnly $\eta$ appearing in $\tau$ and $p\in \mathbb{P}$ are needed, so this is a subset of a ground-model set. The forcing definability lemma makes its defining predicate a formula of $M$. Ground-model axiom schema of separation therefore gives $\sigma \in M$.

If $(\eta ,p)\in \sigma$ with $p\in G$, the accompanying $q\ge p$ belongs to $G$, so ${\eta }_G\in {\tau }_G$. The forcing theorem gives $\phi ({\eta }_G,{\tau }_G,({\tau }_1{)}_G,\dots ,({\tau }_n{)}_G)$.

Conversely, if $u\in {\tau }_G$ satisfies this formula, choose $(\eta ,q)\in \tau$ with $q\in G$ and ${\eta }_G=u$. The forcing truth lemma supplies $r\in G$ forcing the formula for these names. Directedness gives $p\in G$ with $p\le q,r$. Then $(\eta ,p)\in \sigma$, and $u\in {\sigma }_G$. ThusThis proves the instance of the axiom schema of separation in the generic extension, without assuming that instance there in order to construct the name.

The forcing definability lemma states that for each formula $\phi (v_1,\dots ,v_n)$ there is a first-order formula ${\mathrm{Force}}_{\phi }$, depending on $\phi$ but not on the chosen names, such that for $p\in P$ and forcing names ${\tau }_i\in M$,The order relation of $\mathbb{P}$ is included in its set code. Thus each instance of the forcing relation is definable inside the ground model, allowing the uses of ground-model axiom schema of separation and replacement in the forcing arguments.

Closure preserves the ground-model cardinal $\lambda$. We use the stronger fact that closed forcing adds no short ordinal sequences. Fix an ordinal $\mu <\lambda$ in $M$ and a forcing name $\dot{h}$ that a condition $p$ forces to be an ordinal-valued function with domain $\mu$.

Inside $M$, recursively strengthen $p$ to decide each value $\dot{h}(\xi )$, for $\xi <\mu$. At a limit stage take a lower bound of the previously chosen descending sequence; its length is below $\lambda$, so $\lambda$-closure supplies one. After all $\mu$ values have been decided, closure supplies a common lower bound $q$. The decided values form a function $h\in M$ by the Axiom schema of replacement, andThe recursion is carried out within $M$ using the definable forcing theorem and a ground-model choice of deciding extensions, so every sequence to which closure is applied belongs to $M$. Repeating the construction below any stronger condition shows that such full-decision conditions are dense below a forcing condition $p$. The dense-below generic meeting lemma ensures that a generic filter containing $p$ meets them. Thus the interpreted function is in $M$.

If $\lambda$ ceased to be a cardinal number in $M[G]$, there would be a surjection $\mu \to \lambda$ for some ordinal $\mu <\lambda$. The forcing theorem gives a name and a condition in $G$ forcing this. The argument above makes its interpretation a ground-model function, but $M$ regards $\lambda$ as a cardinal number and admits no such surjection. ThereforeNo regularity of $\lambda$ is required; every recursion used has length strictly below $\lambda$. Finite cardinals are preserved automatically. This is cardinal preservation by closed forcing.