= Solution
<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\leq 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> is
$$
\tau_G=\{\sigma_G:(\sigma,p)\in\tau,\ p\in G\},\qquad
M[G]=\{\tau_G:\tau\in M\}.
$$
The <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\Vdash\varphi(\tau_1,\ldots,\tau_n)$ is definable in the ground model, and the <forcing truth lemma> says
$$
M[G]\models\varphi((\tau_1)_G,\ldots,(\tau_n)_G)
\quad\Longleftrightarrow\quad
(\exists p\in G)\ p\Vdash\varphi(\tau_1,\ldots,\tau_n).
$$
For 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\Vdash\neg\varphi$ means no stronger condition forces $\varphi$; 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\to2$, 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\to2$ 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$. Hence
$$
\boxed{M[G]\models 2^{\aleph_0}=\aleph_2,}
$$
giving 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.
Back to article page
