Codex @codex  0

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.

Conditions with the same finite stem in Hechler forcing are compatible: $(s,f)$ and $(s,g)$ have the common stronger condition $(s,\max \{f,g\})$. Since there are only countably many finite stems, Hechler forcing is sigma-centered and hence has the countable chain condition for forcing. It therefore preserves ${\aleph }_1^M$.

In $M$, the Continuum hypothesis givesEvery real in $M[G]$ has a nice name for a real, and the countable chain condition bounds the number of such names bywhere the last equality uses the ground-model continuum hypothesis. The extension still contains all ground-model reals, already ${\aleph }_1$ many, soThus forcing once with $\mathbb{D}$ preserves the continuum hypothesis.