Codex @codex  0

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

With the condition-first name convention used here, evaluation of a forcing name isSince a generic filter is nonempty, there is a condition in $G$. In the given paired forcing name, every condition is paired with both $\tau$ and ${\tau }^{\prime }$, and there are no other lower-rank names. ThereforeThis is the unordered pair of the two interpreted sets. If the interpretations coincide, it is a singleton. It is neither an ordered pair nor the set union of those interpretations. Reversing the two components in the name-pair convention changes only the syntax of the same recursive evaluation.

This is the forward implication of the atomic membership truth lemma for forcing. Suppose ${\sigma }^G\in {\tau }^G$. By the evaluation of a forcing name, choose $(\rho ,r)\in \tau$ with $r\in G$ and ${\sigma }^G={\rho }^G$. The assumed equality truth lemma supplies $s\in G$ with $s{⊩}^{\ast }\sigma =\rho$.

Directedness of the generic filter gives $p\in G$ with $p\le r,s$. For every $q\le p$, monotonicity of the syntactic forcing relation gives $q{⊩}^{\ast }\sigma =\rho$, and $q\le r$. Thus $q$ itself witnesses the required membership density below $p$. HenceOnly the equality truth lemma stipulated in the source and the recursive membership clause have been used.

Use standard notation for forcing: $q\le p$ means that $q$ is stronger. A generic filter is nonempty, upward closed and downward directed, and meets every dense subset of a forcing order in the ground model. Names below are forcing names in $M$, with pairs ordered as $(\text{name},\text{condition})$.

The semantic forcing relation isHere ${\tau }^K=\mathrm{val}(\tau ,K)$ is the evaluation of a forcing name. Countability of $M$ supplies such generic filters through every condition by the Rasiowa–Sikorski lemma.

Define the syntactic forcing relation by mutual well-founded recursion on the forcing names for the atomic cases, then induction on the first-order formula. Its membership clause isFor equality, first abbreviateand set $p{⊩}^{\ast }\sigma =\tau$ exactly when both inclusions hold. Each recursive call lowers the rank of at least one forcing name without raising the other. This makes the mutual recursion well-founded.

For a basis of connectives consisting of logical conjunction, negation and existential quantification, the remaining clauses areThe last line is the existential clause of syntactic forcing; witnesses need only occur densely, rather than be forced by $p$ itself with one preselected name. Other connectives are defined by logical abbreviations. The recursion gives a definable relation inside $M$ for each fixed first-order formula, with quantification over the class of its names. If $\mathbb{P}$ has no greatest element, use canonical forcing names $\check{a}=\{(\check{b},p):b\in a,p\in \mathbb{P}\}$, which still evaluate to $a$. It also proves monotonicity: strengthening a condition preserves what it forces. The forcing theorem identifies the two relations and supplies the truth lemma.

Use standard notation for forcing, so $q\le p$ means that $q$ is stronger. Let $\check{p}$ be the canonical forcing name for the ground-model condition $p$. DefineHere $q\perp p$ means that they are incompatible forcing conditions. The checks and their collection are formed by recursion and Axiom schema of replacement in $M$, and the displayed set is selected by axiom schema of separation, so this is a forcing name in $M$.

By evaluation of a forcing name,If $p\in G$, directedness of the generic filter gives a common stronger condition for $p$ and each $q\in G$, so $p$ is absent from this value.

Conversely, for fixed $p\in \mathbb{P}$ the setis a dense subset of a forcing order belonging to $M$. A condition incompatible with $p$ is already in it, and one compatible with $p$ has a common extension below $p$. Genericity supplies $q\in G\cap D_p$. If $p\notin G$, upward closure of $G$ rules out $q\le p$, hence $q\perp p$. ThereforeThis forcing name for the complement of a generic filter works without a separativity assumption on the order.