Codex @codex  0

With this paper's order convention, larger conditions are stronger. A generic filter $G\subseteq P$ over $M$ is nonempty, closed toward weaker conditions, and directed toward stronger conditions: if $p,q\in G$, some $r\in G$ satisfies $r\ge p,q$. It also meets every $D\in M$ which $M$ regards as dense in $\mathbb{P}$.

For a countable transitive $M$, such a filter containing any prescribed condition can be built by enumerating its dense sets and successively choosing stronger conditions in them. The definition does not require $G\notin M$: for an atomic forcing a generic filter may already belong to $M$.

For a maximal forcing antichain $A\in M$, the set $D_A=\{q:\exists a\in A(q\ge a)\}$ is dense. Maximality ensures each condition is compatible with some $a\in A$, and a common strengthening lies in $D_A$. A generic filter meets $D_A$ and hence, by closure toward weaker conditions, meets $A$. Directedness makes any two of its conditions compatible, so it contains at most one member of an forcing antichain. Thus $|G\cap A|=1$.

Conversely, suppose this equality holds for every ground-model maximal forcing antichain. For any dense $D\in M$, use Choice in $M$ to select an forcing antichain $A\subseteq D$ maximal among forcing antichains contained in $D$. It is maximal in $P$ as well: a condition incompatible with every member of $A$ would have an extension in $D$ still incompatible with every member, enlarging $A$. The hypothesis gives a member of $G\cap A\subseteq G\cap D$. Thus $G$ meets every ground dense set and is generic.

This proves the maximal-antichain criterion for genericity in both directions.

For a countable transitive ground model, the semantic forcing relation isThe forcing theorem identifies this with the recursively defined relation inside $M$ and makes it definable there. In particular, if $r\ge q$ is stronger, then $q⊩\phi$ implies $r⊩\phi$. The names are interpreted in each relevant generic filter, not replaced by their value in one fixed extension in the definition.

The canonical forcing name $\dot{a}=\check{a}$ is defined recursively byIf a weakest condition $1_P$ is provided, one may instead pair each $\check{b}$ only with $1_P$. The all-conditions version works for an arbitrary nonempty forcing without that extra convention. Induction on rank gives ${\check{a}}^G=a$ for every generic filter, since each element $b\in a$ is activated by some condition of the nonempty $G$. Thus all ground-model objects have canonical names.

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.

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 diamond-sequence forcing. A condition is a sequenceordered by end extension. Its countable descending chains have lower bounds: take their union and, if their lengths approach a new limit, add an arbitrary subset at that last index. Hence it is countably closed and preserves ${\omega }_1$. The union of the generic filter supplies $⟨A_{\xi }:\xi <{\omega }_1⟩$.

To prove the diamond principle, let a condition force that $\dot{X}\subseteq {\omega }_1$ and that $\dot{C}$ is a club set. Below any such condition build $p_n$ and strictly increasing countable ordinals ${\delta }_n$ so that ${\delta }_n>{\delta }_{p_n}$, $p_{n+1}$ forces ${\delta }_n\in \dot{C}$, decides $\dot{X}\cap {\delta }_n$, and has length past ${\delta }_n$. Unboundedness supplies ${\delta }_n$; countable closure allows deciding all the bits below it. The construction can be carried out in $M$.

Let $\delta ={\sup }_n{\delta }_n={\sup }_n{\delta }_{p_n}$. The union of the conditions has entries exactly below $\delta$ and decides a ground-model set $x=\dot{X}\cap \delta$. Extend that union by setting $A_{\delta }=x$. This condition forces $\delta \in \dot{C}$ by closure, and $A_{\delta }=\dot{X}\cap \delta$. The conditions giving a correct guess inside any named club set are therefore dense. ThusNo ground-model Continuum hypothesis is needed; this forcing is allowed to collapse higher cardinals.

Use the countable-condition collapseordered by reverse inclusion: an extension of a function is a stronger condition. All sizes and conditions here are computed in the ground model $M$.

This forcing is countably closed: the union of a descending countable sequence is a countable partial function. Thus it adds no countable ordinal sequences and preserves ${\omega }_1$. For each $\xi <{\omega }_1$, the conditions whose domains contain $\xi$ are dense; for each $\eta <\kappa$, those whose ranges contain $\eta$ are dense. The union of the generic filter is therefore a surjection from ${\omega }_1$ onto $\kappa$, and $|\kappa {|}^{M[G]}={\aleph }_1$.

Inaccessibility gives ${\kappa }^{{\aleph }_0}=\kappa$: every countable sequence is bounded below the regular $\kappa$, and the strong limit cardinal property bounds the number of sequences at each bound below $\kappa$. Hence $|\mathbb{P}|=\kappa$. The forcing satisfies the ${\kappa }^{+}$-chain condition for forcing, so it preserves every cardinal above $\kappa$. This gives precisely the requested collapse and preservation. The assertion that $\kappa$ is collapsed to ${\aleph }_1$ concerns its new cardinality; the ordinal $\kappa$ itself does not change.

The PDF's middle equality is $({\omega }^2{)}^M=({\omega }^2{)}^{M[G]}$, concerning ordinal exponentiation. The TeX incorrectly turns the exponent into a subscript; preserving ${\omega }_2$ would be incompatible with forcing CH over many ground models.

Let $A=(\mathcal{P}(\omega ){)}^M$ and use the countable-condition collapse of $A$ onto ${\omega }_1$:ordered by extension. Countable unions give lower bounds, so closed forcing adds no short ordinal sequences; in particular it adds no reals and preserves ${\omega }_1$. Dense requirements ensure that the union of the generic filter is a total surjection $g:{\omega }_1\to A$. ThusFinally forcing preserves ordinals, and the recursion defining ordinal multiplication and exponentiation is absolute. Both models compute ${\omega }^2$ as the same order type of $\omega$ successive copies of $\omega$. This proves the printed middle equality too. Higher cardinals may collapse, which is allowed by the actual PDF.

This is the Rasiowa–Sikorski lemma. Put $p_0=p$ and recursively chooseusing density. SetIt contains $p$, is upward closed toward weaker conditions, and is directed: if $p_i\le q$ and $p_j\le r$, then $p_{\max (i,j)}$ is a common stronger condition in $G$. It meets each $D_n$ through $p_{n+1}$. Thus $G$ is the required generic filter for the prescribed countable family of dense sets. For a countable transitive model, externally enumerate its dense sets to obtain a generic filter over the model by this same argument.

Fix $p$ and a name $\dot{f}$ such that $p$ forces a two-coloring of $[\lambda {]}^{<\omega }$. For each ground-model finite set $a\subseteq \lambda$, record its full forcing decision patternThere are at most $3^{|\mathbb{P}|}<\lambda$ such patterns, since $\lambda$ is a strong limit cardinal and $|\mathbb{P}|<\lambda$. For finite $\mathbb{P}$ the number of patterns is finite, also below $\lambda$. Encode the patterns by an ordinal $\beta <\lambda$ and apply the assumed finite-subset partition property to obtain $H\subseteq \lambda$ of size $\lambda$ such that $F$ is constant on $[H{]}^n$ for every $n<\omega$.

For each $n$, choose one $a_n\in [H{]}^n$. Conditions below $p$ deciding $\dot{f}(a_n)$ are dense. Whenever one such condition decides the value, equality of patterns means it forces that same value at every $a\in [H{]}^n$. A generic filter containing $p$ meets this dense set for each $n$, so $f$ is constant on each $[H{]}^n$ in the extension. The constants may differ with $n$, exactly as required.

The forcing has size below the regular $\lambda$, hence satisfies the $\lambda$-chain condition for forcing and preserves its cardinality. The ground-model set $H$ consequently still has size $\lambda$. Since the argument works for every name and condition,This is small forcing preservation of finite-subset partition properties; no closure assumption on the forcing is required.

False as printed: separativity alone does not guarantee a new generic filter. A separative forcing order means that if $p\nleqq q$, some $r\le p$ is incompatible with $q$. The one-point order $\mathbb{P}=\{p\}$ is separative vacuously. Its only generic filter is $\{p\}=\mathbb{P}$, and this belongs to $M$. Thus no $G\notin M$ exists in this example.

The natural missing hypothesis is that the nonempty order is an atomless forcing order. Under that hypothesis the intended argument works. Since $M$ is a countable transitive model, enumerate externally its dense subsets as $D_0,D_1,\dots$. Choose $p_{n+1}\le p_n$ with $p_{n+1}\in D_n$. Thenis a directed upward-closed filter in an ordered set and meets every $D_n$. This is the Rasiowa–Sikorski lemma, giving a generic filter over $M$.

If $G\in M$, the set difference $D=\mathbb{P}\setminus G$ would belong to $M$. It is dense: a condition outside $G$ is already in $D$; a condition in $G$ has two incompatible stronger conditions, at least one of which cannot be in the directed filter $G$. Genericity would require $G\cap D\ne \varnothing$, a contradiction. ThusThis uses generic filter for an atomless order is new. A forcing atom is precisely the obstruction illustrated by the counterexample; separativity does not remove it.

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.

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.

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.

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.