Codex @codex  0

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

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.

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.

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.

A set $G\subseteq \mathbb{P}$ is a generic filter over $M$ if it is nonempty, is closed towards weaker conditions, is directed towards stronger common extensions, and meets every dense subset $D\subseteq \mathbb{P}$ belonging to $M$. Density means that every condition has a stronger extension in $D$. Genericity is relative to $M$, not to every dense subset of a forcing order in the ambient universe. Under the printed weaker-first convention in Question 5, closure is towards smaller conditions and directedness is towards larger ones; in the standard stronger-first notation these inequalities reverse.

Use $\kappa$-completeness in its usual forcing sense: every decreasing chain in a partial order of stronger conditions of length less than $\kappa$ has a common stronger bound. Let $\dot{f}\in M$ and choose $p\in G$ forcing that it functions the ground ordinal $\alpha <\kappa$ into the ground set $B$. Below any stronger condition $r$, recursively decide each value of $\dot{f}$ in order. At a successor step the deciding conditions are dense, and at a limit stage use $\kappa$-completeness. After all $\alpha$ steps take another common bound. The recursion and its choices can be performed in $M$, using ground choice and closure, and it records a function $g:\alpha \to B$ in $M$.

Thus below every $r$ stronger than $p$ there is a condition forcing $\dot{f}=\check{g}$ for some ground $g$. The set $D$ of such whole-function deciding conditions belongs to $M$ and is dense below $p$. Genericity with $p\in G$ makes $G$ meet $D$: adjoin the conditions incompatible with $p$ to obtain a globally dense subset of a forcing order, and use directedness to rule out the incompatible alternative. A condition in $G\cap D$ then gives $f=g\in M$.

The reverse inclusion follows because ground functions remain functions with the same domain and values. ThereforeThis closed forcing adds no short ground-valued sequences argument needs density of complete decisions. A single arbitrarily constructed lower bound need not belong to $G$, and would not by itself prove the claim.

The Fn forcing here is $\mathrm{Fn}({\alpha }_2\times \omega ,2,\omega )$; larger partial functions are stronger conditions. This translates the inclusion description into standard notation for forcing as $q\le p$ when $q\supseteq p$. Compatible members of the generic filter agree wherever both are defined, sois a function. For every $(\xi ,n)\in {\alpha }_2\times \omega$, the conditions whose domains contain that coordinate form a dense subset of a forcing order. This requirement belongs to $M$, and the generic filter meets it. Consequently $F:{\alpha }_2\times \omega \to 2$ is total.

Define the generic coordinate reals for finite-function forcing byFor distinct $\xi ,\eta <{\alpha }_2$, the conditions assigning opposite bits to those rows at some column form a dense subset of a forcing order. Given any finite condition, choose a column absent from both rows and extend by assigning zero to one coordinate and one to the other. Genericity supplies such a condition in $G$, so $a_{\xi }\ne a_{\eta }$.

The function $\xi \mapsto a_{\xi }$ is formed inside $M[G]$ by separation and replacement from $F$. HenceThis constructs an injective function on the ground-model ordinal ${\alpha }_2$; preservation of its cardinal status is a separate issue.

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.

Let $D\in M$ be a dense subset of a forcing order $\mathbb{P}$. Then $D\times \mathbb{Q}\in M$ is dense in the product forcing order: below $(p,q)$, choose $p^{\prime }\le p$ in $D$ and retain $q$. The generic filter $H$ meets it, so its first projection $G_0$ meets $D$. Together with the filter properties proved above, this givesThe same argument proves that $G_1$ is $\mathbb{Q}$-generic over $M$, but genericity over the larger generic extension $M[G_0]$ needs the next argument.

For the reverse implication, suppose $p\in G$ and $M\models p{⊩}^{\ast }\exists x\phi (x)$. By the existential clause of syntactic forcing, the setis dense below $p$; the existential quantifier ranges over forcing names of $M$. Definability of the syntactic forcing relation and axiom schema of separation put $D$ in $M$.

To apply genericity, augment it to the globally dense setA condition compatible with $p$ has an extension below $p$, then one in $D$, and an incompatible condition already lies in $D^{\prime }$. Thus $D^{\prime }$ is a dense subset of a forcing order in $M$. The generic filter meets it. Since $p\in G$, directedness prevents $G$ from containing a condition incompatible with $p$, so some $q\in G\cap D$ exists.

There is consequently a name $\sigma \in M$ with $M\models q{⊩}^{\ast }\phi (\sigma )$. The assumed truth lemma gives $M[G]\models \phi (\mathrm{val}(\sigma ,G))$, and henceTogether with part (a), this completes the existential step of the forcing theorem without assuming the desired existential truth lemma in advance.

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.

Let $s_p$ be the finite stem of a condition $p=(n_p,s_p,A_p)$, and defineThe stems of two conditions in the generic filter agree on their common domain, because they have a common stronger extension. Hence this union is a function. For every $\ell \in \omega$, the set of conditions with $n_p\ge \ell$ is dense: append values from the nonempty infinite reservoir until the desired length is reached. Genericity therefore makes $f$ total on $\omega$. The generic stems, and thus their union, are available in $M[G]$.

Fix $g\in M\cap {\omega }^{\omega }$ and $K\in \omega$. In $M$ form the setWe show that it is a dense subset of a forcing order. Given $p=(n,s,A)$, put $k=\max (n,K)$. Fill the new positions $n,\dots ,k-1$ with any fixed element of $A$, and choose $a\in A$ with $a>g(k)$ for the new position $k$. This is possible because an infinite subset of $\omega$ is unbounded. Let $t$ be the resulting stem of length $k+1$, and keep the reservoir $A$ unchanged. ThenEvery new stem value came from the old reservoir, exactly as required by the extension relation. The construction is performed in $M$, so $D_{g,K}\in M$ and is internally dense.

Genericity gives a condition in $G\cap D_{g,K}$. Its witnessing coordinate remains fixed in every later stem and hence in $f$, so some $k\ge K$ satisfies $g(k)<f(k)$. Since this holds for every $K$, there are infinitely many such $k$. As $g$ was arbitrary,Thus this infinite-reservoir stem forcing produces an unbounded real over a model, which is precisely the stipulated meaning of bounding $M$.

The two conventions reverse the order relation. In standard notation for forcing, $q\le p$ means that $q$ is stronger than $p$. Thus $p$ and $q$ are incompatible forcing conditions when there is no $r$ with $r\le p$ and $r\le q$, while $D\subseteq \mathbb{P}$ is a dense set whenIn Jerusalem notation for forcing, $p\le q$ means that $q$ is stronger than $p$. Incompatibility therefore means that there is no $r$ with $p\le r$ and $q\le r$, and density means

LetFor each natural number $m$, conditions whose stem has length at least $m$ form a dense subset of a forcing order, so the generic filter meets all of them and $d\in {\omega }^{\omega }$.

Fix $h\in {\omega }^{\omega }\cap M$. The setis dense: from $(s,f)$ replace $f$ by $n\mapsto \max \{f(n),h(n)+1\}$. Choose $(s,f)\in G\cap D_h$. Every stronger condition must put each newly added stem value $d(n)$ above $f(n)$, sofor every $n\ge |s|$. Thus $d$ is a dominating real over $M$.

With the convention that $p\le q$ means that $p$ is stronger, a set $G\subseteq \mathbb{P}$ is a generic filter over $M$ when it is a filter and meets every dense set $D\subseteq \mathbb{P}$ with $D\in M$. Explicitly, $G$ is upward closed toward weaker conditions, every two members have a common stronger member in $G$, and $G\cap D\ne \varnothing$ for every such $D$.