Forcing Orders, Names, and Generic Extensions

For $(n,q)\in \omega \times P$, let $E_{n,q}=\{r\in D_n:r\le q\}$. These sets are nonempty by density. AC selects $h(n,q)\in E_{n,q}$; this is the sole AC use. Recursively set $p_0=p$ and $p_{n+1}=h(n,p_n)$. Thus $p_{n+1}\le p_n$ and $p_{n+1}\in D_n$.

Define $G=\{q\in P:\mathrm{\exists }n(p_n\le q)\}$. It contains p and is upward closed. If q,r have witnesses n,m, then $p_{\max (n,m)}\in G$ strengthens both. Hence G is a filter and $p_{n+1}\in G\cap D_n$ for every n.

If e is supplied, instead define h(n,q) as $e(k)$ for the least k with $e(k)\in D_n$ and $e(k)\le q$. Such k exists by density and surjectivity, and is unique by leastness. This rule and the recursion and verification above require only ZF.

Set $D_n=e(n)$ if e(n) is a dense subset of P, and $D_n=P$ otherwise. Every ground-model dense subset occurs. For q in P let $h(n,q)=e(k)$ for the least k such that $e(k)\in D_n$ and $e(k)\le q$. Transitivity gives $P\subseteq M$, so surjectivity of e and density ensure such k exists. This is a uniquely defined rule, not a choice function obtained by AC. Recursively put $p_0=p$ and $p_{n+1}=h(n,p_n)$.

Put $G=\{q\in P:\mathrm{\exists }n{p}_n\le q\}$. Then p belongs to G; transitivity gives upward closure; and the term with index max(n,m) strengthens any two members witnessed by n,m. Thus G is a filter. Each $p_{n+1}\in D_n\cap G$, so F1 makes G M-generic. Neither the sequence nor G is asserted to be an element of M.

Induct externally in actual membership rank on $\tau \in M$. Whether every entry is a pair with second coordinate in P is absolute by transitivity and F3. Every first coordinate sigma then belongs to M and has smaller membership rank. By induction sigma is internally a name iff it is actually a name. F1 characterizes namehood by exactly these entry conditions in both universes; its stage-bound converse is available internally in M because M satisfies ZF. Thus namehood agrees, including the empty name.

For a name tau, its internal set of predecessor ranks plus one exists by internal Replacement. The induction hypothesis identifies each predecessor rank, and F2 and F3 identify ordinal successors and the union giving the supremum. Both rank recursions consequently give the same value at tau. The empty predecessor set gives zero on both sides. No comparison of the full power sets at a name stage entered either induction.

By membership induction suppose the assertion holds for each $y\in x$. The valuation equation for check x gives exactly $\{{\mathrm{val}}_G(\check{y}):y\in x,\mathrm{\exists }p\in G\}=\{y:y\in x\}=x$. The nonemptiness of G supplies the existential coefficient for every y. For x empty both sides are empty.

Apply step 1.1 to every p in P. The valuation equation gives ${\mathrm{val}}_G(\dot{G})=\{{\mathrm{val}}_G(\check{p}):p\in G\}=G$. For each $x\in M$, F1 puts check x in M, so step 1.1 puts x in M[G]. F1 also puts dot G in M, so its value G lies in M[G]. No genericity or directedness was needed for these identities.

If $x\in y\in M[G]$, write $y={\mathrm{val}}_G(\tau )$ for a name $\tau \in M$. By F1 some $⟨\sigma ,p⟩\in \tau$ has $p\in G$ and $x={\mathrm{val}}_G(\sigma )$. Transitivity of M, applied through the Kuratowski pair, gives $\sigma \in M$; F2 says that sigma is a name. Thus $x\in M[G]$, proving transitivity.

Induct on the subname relation. Every member of the valuation of tau is the valuation of some sigma below tau, so F3 gives its rank as the supremum of their value-ranks plus one. By induction this is at most the supremum of ${\mathrm{rk}}_P(\sigma )+1$ over all subnames sigma, which F2 identifies with ${\mathrm{rk}}_P(\tau )$. With no selected subnames the value rank is zero and the inequality still holds. This includes both the empty name and empty G.

A set T of names has a common stage bound by F2, so S(T) is a name. By F3, each tau in T occurs in its valuation with every condition, and G nonempty therefore gives exactly $S(T{)}_G=\{{\tau }_G:\tau \in T\}$. Apply this three times: the two inner values are $\{{\sigma }_G\}$ and $\{{\sigma }_G,{\tau }_G\}$, and the outer value is their unordered pair, precisely the Kuratowski ordered pair.

Replacement on I makes the set of pair names in the statement. Step 1.1 and F1 give its S-value as $\{⟨i,({\tau }_i{)}_G⟩:i\in I\}$. Each index i has exactly one family value, so this is the graph of the claimed function even when different indices have equal values. Internal Pairing, product and Replacement perform these same finite constructions in M; F2–F4 and transitivity identify their outputs. Finally F1 applied to the set alpha gives the ordinal check identity, with no ordinal-preservation assertion about arbitrary names.

For input names s,t let C be the union of their descendant cones, including s,t. It is a set: iterate the operation adjoining first coordinates of pair entries through omega and take the union; Replacement and Union suffice. It is closed under subnames. On $C\times C$ assign the complexity $c(u,v)=(\max ({\mathrm{rk}}_B(u),{\mathrm{rk}}_B(v)),\min ({\mathrm{rk}}_B(u),{\mathrm{rk}}_B(v)))$ and order these ordinal pairs lexicographically. Any nonempty set of them has a least first coordinate and then a least second coordinate. Lowering either name rank strictly while retaining the other strictly lowers this sorted pair.

Recurse on the set $\{E,I\}\times C\times C$, with a triple preceding another whenever its complexity is smaller. The relation is well-founded by step 1.1 and setlike because its whole domain is a set. In I(u,v), every requested E(u,w) has w a subname of v; in E(u,v), the requested I(w,v) or I(w,u) lowers respectively the rank of u or v, allowing the coordinate swap. Thus every requested value is at smaller complexity. The sets of requested terms are set images of the pair entries, and completeness supplies their unique joins and meets. F3 gives existence and uniqueness of E and I on this domain.

For two descendant-closed sets the intersection is descendant-closed. Induction on the same ordinal-pair complexity shows their recursive values agree for all pairs in the intersection, since the defining clauses request only subname pairs there. The values therefore do not depend on the cone chosen. A single formula saying that a set-domain recursion on the canonical cone has a specified output defines the global atomic values. Any rival satisfies these clauses on each cone and agrees by uniqueness. No order of all pairs of names was claimed to be setlike.

Now induct externally through one fixed finite formula. Atomic values are definable by step 3.1. Negation, conjunction and other finite Boolean operations preserve definability and uniqueness. For an existential whose matrix value is already a definable class function, Separation on B forms the set of attained matrix values over all names, and completeness gives its unique supremum. This is a new defining formula for each fixed formula, not a uniform truth predicate. The same construction inside a ground model uses only its internally formed cones, images and subsets of B, so internal completeness suffices and no external completeness is inferred.

For any filter G on atomless P, $P\setminus G$ is dense. Given p, choose two incompatible refinements q,r of p. They cannot both be in G, since internal directedness would give a common stronger condition. At least one therefore lies in $P\setminus G$ below p. This is one finite existential argument for each p, not a simultaneous choice function.

If G were in M, internal Separation would make the actual set $D=P\setminus G$ an element of M. Step 1.1 makes D dense, while genericity would require $G\cap D\mathrm{\ne }\mathrm{\varnothing }$, impossible by its definition. Thus G is not in M. For singleton forcing, its unique filter P belongs to M and meets every dense set, exhibiting the failure when atomlessness is removed.