Boolean Completion Theorem for Forcing Posets (Theorem # 6520)
Theorem
Let $(\mathbb P, \leq)$ be a separative forcing partial order. Then $\mathbb P$ densely embeds into a complete Boolean algebra $\operatorname{RO}(\mathbb P)$. Forcing with $\mathbb P$ and forcing with $\operatorname{RO}(\mathbb P) \setminus \{\varnothing\}$ give equivalent generic extensions. For a general forcing preorder, the same conclusion applies after first replacing $\mathbb P$ by its separative quotient.
Knowledge Status
Discrete Mathematics
Set Theory
Discussion
A result from set-theoretic forcing concerning boolean completion theorem for forcing posets, used in the [Set Theory II: Forcing](/page/Set%20Theory%20II%3A%20Forcing) notes.
Proof
[proofplan]
We put the forcing order topology on $\mathbb{P}$ by declaring the cones $N_p = \{q : q \leq p\}$ to be basic open sets, and then take the complete Boolean algebra of regular open subsets. The embedding sends a condition to the regular [open set](/page/Open%20Set) generated by its cone. Separativity is exactly what makes this embedding faithful: it reflects order and incompatibility. Density follows because every non-empty regular open set contains some basic cone. Finally, dense embeddings preserve generic filters and the recursive interpretation of names, giving the same generic extensions; for a preorder one first quotients by the usual separative equivalence.
[/proofplan]
[step:Build the regular open Boolean algebra from the forcing topology]
For each $p \in \mathbb{P}$, define the cone
\begin{align*}
N_p := \{q \in \mathbb{P} : q \leq p\}.
\end{align*}
The family $\mathcal{B} := \{N_p : p \in \mathbb{P}\}$ is a basis for a topology $\tau_{\mathbb{P}}$ on $\mathbb{P}$: if $r \in N_p \cap N_q$, then $r \leq p$ and $r \leq q$, hence $N_r \subset N_p \cap N_q$.
Let $\operatorname{RO}(\mathbb{P})$ be the collection of all regular open subsets of $(\mathbb{P}, \tau_{\mathbb{P}})$, that is,
\begin{align*}
\operatorname{RO}(\mathbb{P}) := \{U \subset \mathbb{P} : U = \operatorname{int}_{\tau_{\mathbb{P}}}(\overline{U}^{\,\tau_{\mathbb{P}}})\}.
\end{align*}
We use the standard regular-open algebra construction. For a [topological space](/page/Topological%20Space) $X$, the family $\operatorname{RO}(X)$ is ordered by inclusion, its Boolean complement is $U^* := \operatorname{int}_X(X \setminus U)$, and the join of a family $(U_i)_{i \in I}$ is obtained by regularizing the union:
\begin{align*}
\bigvee_{i \in I} U_i := \operatorname{int}_X\left(\overline{\bigcup_{i \in I} U_i}^{\,X}\right).
\end{align*}
The meet is then determined from complements and joins by De Morgan's law:
\begin{align*}
\bigwedge_{i \in I} U_i := \left(\bigvee_{i \in I} U_i^*\right)^*.
\end{align*}
The cited construction proves that these operations send regular open sets to regular open sets, satisfy the Boolean algebra laws, and give joins and meets for arbitrary index sets $I$. Applying it to $X = (\mathbb{P}, \tau_{\mathbb{P}})$ gives a complete Boolean algebra $\operatorname{RO}(\mathbb{P})$. In this case, for $U \in \operatorname{RO}(\mathbb{P})$ the complement is
\begin{align*}
\neg U := \operatorname{int}_{\tau_{\mathbb{P}}}(\mathbb{P} \setminus U).
\end{align*}
Define the map $e: \mathbb{P} \to \operatorname{RO}(\mathbb{P}) \setminus \{\varnothing\}$. For $p \in \mathbb{P}$, set
\begin{align*}
e(p) := \operatorname{int}_{\tau_{\mathbb{P}}}\left(\overline{N_p}^{\,\tau_{\mathbb{P}}}\right).
\end{align*}
Since $p \in N_p \subset e(p)$, the set $e(p)$ is non-empty for every $p \in \mathbb{P}$.
[/step]
[step:Show that the map preserves the forcing order]
Suppose $q \leq p$ in $\mathbb{P}$. Then $N_q \subset N_p$, hence
\begin{align*}
\overline{N_q}^{\,\tau_{\mathbb{P}}} \subset \overline{N_p}^{\,\tau_{\mathbb{P}}}.
\end{align*}
Taking interiors gives
\begin{align*}
e(q) = \operatorname{int}_{\tau_{\mathbb{P}}}\left(\overline{N_q}^{\,\tau_{\mathbb{P}}}\right) \subset \operatorname{int}_{\tau_{\mathbb{P}}}\left(\overline{N_p}^{\,\tau_{\mathbb{P}}}\right) = e(p).
\end{align*}
Thus $e$ is order-preserving when $\operatorname{RO}(\mathbb{P}) \setminus \{\varnothing\}$ is ordered by inclusion, with smaller Boolean elements representing stronger forcing conditions.
[guided]
We first check that the direction of the order is correct. In forcing notation, $q \leq p$ means that $q$ is stronger than $p$. The cone below $q$ is therefore contained in the cone below $p$:
\begin{align*}
N_q = \{r \in \mathbb{P} : r \leq q\} \subset \{r \in \mathbb{P} : r \leq p\} = N_p.
\end{align*}
Closure is monotone with respect to inclusion, so
\begin{align*}
\overline{N_q}^{\,\tau_{\mathbb{P}}} \subset \overline{N_p}^{\,\tau_{\mathbb{P}}}.
\end{align*}
Interior is also monotone with respect to inclusion, and therefore
\begin{align*}
e(q) = \operatorname{int}_{\tau_{\mathbb{P}}}\left(\overline{N_q}^{\,\tau_{\mathbb{P}}}\right) \subset \operatorname{int}_{\tau_{\mathbb{P}}}\left(\overline{N_p}^{\,\tau_{\mathbb{P}}}\right) = e(p).
\end{align*}
This is the expected translation: stronger forcing conditions become smaller regular open sets.
[/guided]
[/step]
[step:Use separativity to reflect order]
We prove the converse order implication. Suppose $e(p) \subset e(q)$. If $p \nleq q$, separativity gives a condition $r \leq p$ such that $r$ is incompatible with $q$. Since $r \leq p$, we have $N_r \subset N_p \subset e(p) \subset e(q)$.
Because $r$ is incompatible with $q$, the basic open set $N_r$ is disjoint from $N_q$. Moreover every condition in $N_r$ remains incompatible with $q$, so $N_r$ is disjoint from $\overline{N_q}^{\,\tau_{\mathbb{P}}}$: if $s \in N_r \cap \overline{N_q}^{\,\tau_{\mathbb{P}}}$, then the basic neighbourhood $N_s$ of $s$ intersects $N_q$, so there is $t \leq s,q$; since $s \leq r$, this gives $t \leq r,q$, contradicting incompatibility of $r$ and $q$.
Thus $N_r \cap \overline{N_q}^{\,\tau_{\mathbb{P}}} = \varnothing$, and hence $N_r \cap e(q) = \varnothing$, contradicting $N_r \subset e(q)$. Therefore $p \leq q$.
Consequently
\begin{align*}
p \leq q \quad\Longleftrightarrow\quad e(p) \subset e(q).
\end{align*}
In particular, $e$ is injective.
[/step]
[step:Show that compatibility is exactly non-zero Boolean meet]
Let $p,q \in \mathbb{P}$. If $p$ and $q$ are compatible, choose $r \in \mathbb{P}$ such that $r \leq p$ and $r \leq q$. Then
\begin{align*}
e(r) \subset e(p) \cap e(q),
\end{align*}
and $e(r) \neq \varnothing$, so $e(p) \cap e(q) \neq \varnothing$.
Conversely, suppose $e(p) \cap e(q) \neq \varnothing$. Since $e(p) \cap e(q)$ is open and non-empty, there is $r \in \mathbb{P}$ such that
\begin{align*}
N_r \subset e(p) \cap e(q).
\end{align*}
The set $N_r$ cannot be disjoint from $N_p$, because if it were, then $N_r$ would be an open neighbourhood disjoint from $N_p$, contradicting $N_r \subset e(p) \subset \overline{N_p}^{\,\tau_{\mathbb{P}}}$. Hence there exists $s \in N_r \cap N_p$, so $s \leq r,p$. Similarly, $N_s \subset N_r \subset e(q)$ cannot be disjoint from $N_q$, so there exists $t \in N_s \cap N_q$. Then $t \leq s \leq p$ and $t \leq q$, proving that $p$ and $q$ are compatible.
Thus
\begin{align*}
p \perp q \quad\Longleftrightarrow\quad e(p) \cap e(q) = \varnothing.
\end{align*}
[/step]
[step:Prove density of the image]
Let $U \in \operatorname{RO}(\mathbb{P}) \setminus \{\varnothing\}$. Since $U$ is a non-empty open set in $\tau_{\mathbb{P}}$, there exists $p \in \mathbb{P}$ such that
\begin{align*}
N_p \subset U.
\end{align*}
Because $U$ is regular open,
\begin{align*}
U = \operatorname{int}_{\tau_{\mathbb{P}}}\left(\overline{U}^{\,\tau_{\mathbb{P}}}\right).
\end{align*}
From $N_p \subset U$ we obtain
\begin{align*}
\overline{N_p}^{\,\tau_{\mathbb{P}}} \subset \overline{U}^{\,\tau_{\mathbb{P}}},
\end{align*}
and therefore
\begin{align*}
e(p) = \operatorname{int}_{\tau_{\mathbb{P}}}\left(\overline{N_p}^{\,\tau_{\mathbb{P}}}\right) \subset \operatorname{int}_{\tau_{\mathbb{P}}}\left(\overline{U}^{\,\tau_{\mathbb{P}}}\right) = U.
\end{align*}
Thus every non-zero element of $\operatorname{RO}(\mathbb{P})$ has a non-zero element of $e[\mathbb{P}]$ below it. Hence $e[\mathbb{P}]$ is dense in $\operatorname{RO}(\mathbb{P}) \setminus \{\varnothing\}$.
[/step]
[step:Transfer generic filters across the dense embedding]
Let $V$ be a ground model. Let $\mathbb{B} := \operatorname{RO}(\mathbb{P})$, and force with $\mathbb{B}^+ := \mathbb{B} \setminus \{\varnothing\}$ ordered by inclusion. Throughout this step, a filter on a forcing order is upward closed toward weaker conditions and directed downward toward common stronger conditions; for $\mathbb{B}^+$ this means upward closed under inclusion and directed by finding a non-zero regular open subset contained in both given elements.
If $G \subset \mathbb{P}$ is $V$-generic, define
\begin{align*}
H_G := \{b \in \mathbb{B}^+ : \text{there exists } p \in G \text{ such that } e(p) \subset b\}.
\end{align*}
Because $e$ preserves order and incompatibility, $H_G$ is a filter on $\mathbb{B}^+$. To see genericity, let $D \subset \mathbb{B}^+$ be dense and belong to $V$. Define
\begin{align*}
D_{\mathbb{P}} := \{p \in \mathbb{P} : \text{there exists } b \in D \text{ such that } e(p) \subset b\}.
\end{align*}
We verify that $D_{\mathbb{P}}$ is dense in $\mathbb{P}$. Given $p_0 \in \mathbb{P}$, density of $D$ in $\mathbb{B}^+$ gives $d \in D$ such that $d \subset e(p_0)$. Density of $e[\mathbb{P}]$ in $\mathbb{B}^+$ gives $p \in \mathbb{P}$ such that $e(p) \subset d$. Then $e(p) \subset e(p_0)$, so order reflection gives $p \leq p_0$, and $p \in D_{\mathbb{P}}$. Hence $D_{\mathbb{P}}$ is dense in $\mathbb{P}$. Since $G$ is $V$-generic, choose $p \in G \cap D_{\mathbb{P}}$. Then there is $b \in D$ with $e(p) \subset b$, so $b \in H_G \cap D$. Hence $H_G$ is $V$-generic for $\mathbb{B}^+$.
Conversely, if $H \subset \mathbb{B}^+$ is $V$-generic, define
\begin{align*}
G_H := \{p \in \mathbb{P} : e(p) \in H\}.
\end{align*}
First record a refinement fact. For every $b\in H$, there is $p\in\mathbb{P}$ such that
\begin{align*}
e(p)\in H
\end{align*}
and
\begin{align*}
e(p)\subset b.
\end{align*}
Indeed, define
\begin{align*}
D_b := \{e(p) : p \in \mathbb{P} \text{ and } e(p) \subset b\} \cup \{c \in \mathbb{B}^+ : c \cap b = \varnothing\}.
\end{align*}
The set $D_b$ is dense in $\mathbb{B}^+$. Given $c \in \mathbb{B}^+$, if $c \cap b = \varnothing$, then $c \in D_b$. If $c \cap b \neq \varnothing$, then $c \cap b$ is a non-zero condition below $c$, and density of $e[\mathbb{P}]$ gives $p \in \mathbb{P}$ with $e(p) \subset c \cap b$, so $e(p) \in D_b$ lies below $c$. Since $H$ is generic, choose an element of $H\cap D_b$. It cannot be disjoint from $b$, because $b\in H$ and a filter contains no two incompatible conditions. Therefore it has the form $e(p)$ with $e(p)\in H$ and $e(p)\subset b$.
We verify that $G_H$ is a filter on $\mathbb{P}$. If $p \in G_H$ and $p \leq q$, then $e(p) \subset e(q)$, so upward closure of $H$ gives $e(q) \in H$ and hence $q \in G_H$. If $p,q \in G_H$, then $e(p),e(q) \in H$. Directedness of $H$ gives $b \in H$ such that $b \subset e(p) \cap e(q)$. By the refinement fact applied to this $b$, choose $r\in\mathbb{P}$ with $e(r)\in H$ and $e(r)\subset b$. Then $e(r)\subset e(p)$ and $e(r)\subset e(q)$, so order reflection gives $r \leq p$ and $r \leq q$. Since $e(r)\in H$, we have $r \in G_H$. Thus $G_H$ is a filter on $\mathbb{P}$.
If $D \subset \mathbb{P}$ is dense and belongs to $V$, define
\begin{align*}
E_D := \{b \in \mathbb{B}^+ : \text{there exists } p \in D \text{ such that } b \subset e(p)\}.
\end{align*}
The set $E_D$ is dense in $\mathbb{B}^+$. Indeed, given any $c \in \mathbb{B}^+$, density of $e[\mathbb{P}]$ gives $q \in \mathbb{P}$ with $e(q) \subset c$, and density of $D$ gives $p \in D$ with $p \leq q$. Then
\begin{align*}
e(p) \subset e(q) \subset c,
\end{align*}
so $e(p) \in E_D$ and lies below $c$. Since $H$ meets $E_D$, choose $b \in H \cap E_D$ and $p \in D$ such that $b \subset e(p)$. Upward closure of $H$ gives $e(p) \in H$, so $p \in G_H \cap D$. Hence $G_H$ is $V$-generic for $\mathbb{P}$.
The two constructions determine one another at the level of generated extensions. If $G$ is $\mathbb{P}$-generic, then
\begin{align*}
G_{H_G} = G,
\end{align*}
because $p \in G_{H_G}$ means $e(p) \in H_G$, so for some $q \in G$ we have $e(q) \subset e(p)$, and order reflection gives $q \leq p$; since $G$ is upward closed in the forcing order, $p \in G$. The reverse inclusion is immediate from the definition of $H_G$.
Now let $H \subset \mathbb{B}^+$ be $V$-generic. The refinement fact shows that every $b \in H$ has some $e(p)\in H$ with $e(p)\subset b$. Such $p$ lies in $G_H$, and therefore $b$ is refined by an element of the image of $G_H$. Conversely, if $b \in H_{G_H}$, then for some $p \in G_H$ we have $e(p) \subset b$; since $e(p) \in H$ and filters are upward closed toward weaker Boolean conditions, $b \in H$. Hence $H$ and $H_{G_H}$ generate the same filter base and therefore the same extension.
Thus $\mathbb{P}$-generic filters and $\mathbb{B}^+$-generic filters determine one another in $V$.
[/step]
[step:Identify the generic extensions by translating names]
We now compare interpretations of names. Let $\mathsf{Name}(\mathbb{P})$ denote the class of $\mathbb{P}$-names and let $\mathsf{Name}(\mathbb{B}^+)$ denote the class of $\mathbb{B}^+$-names. Define the recursive translation map $T_e: \mathsf{Name}(\mathbb{P}) \to \mathsf{Name}(\mathbb{B}^+)$ by
\begin{align*}
T_e(\dot{x}) := \{(T_e(\dot{y}), e(p)) : (\dot{y},p) \in \dot{x}\}.
\end{align*}
The recursion is legitimate because names are defined by well-founded rank recursion. If $G \subset \mathbb{P}$ is $V$-generic and $H_G$ is the associated $\mathbb{B}^+$-generic filter, then induction on the rank of $\dot{x}$ gives
\begin{align*}
\dot{x}^G = T_e(\dot{x})^{H_G}.
\end{align*}
Here the superscripts $G$ and $H_G$ denote generic evaluation, while $T_e$ denotes translation of names. For each pair $(\dot{y},p) \in \dot{x}$, the condition $p \in G$ is equivalent to $e(p) \in H_G$, and the induction hypothesis gives $\dot{y}^G = T_e(\dot{y})^{H_G}$.
Conversely, define a recursive translation map $S: \mathsf{Name}(\mathbb{B}^+) \to \mathsf{Name}(\mathbb{P})$ as follows. For a $\mathbb{B}^+$-name $\dot{z}$, let
\begin{align*}
S(\dot{z}) := \{(S(\dot{w}),p) : \text{there exists } b \in \mathbb{B}^+ \text{ such that } (\dot{w},b) \in \dot{z} \text{ and } e(p) \subset b\}.
\end{align*}
This is a set because it is formed by rank recursion from the set of pairs in $\dot{z}$ and the set $\mathbb{P}$. Let $H \subset \mathbb{B}^+$ be $V$-generic and let $G_H$ be the associated $\mathbb{P}$-generic filter. We prove by induction on the rank of $\dot{z}$ that
\begin{align*}
\dot{z}^{H} = S(\dot{z})^{G_H}.
\end{align*}
If $(\dot{w},b) \in \dot{z}$ and $b \in H$, apply the dense-set argument from the previous step to this particular $b$. There is $p \in \mathbb{P}$ such that $e(p) \in H$ and $e(p) \subset b$. Hence $p \in G_H$, the pair $(S(\dot{w}),p)$ belongs to $S(\dot{z})$, and the induction hypothesis gives $\dot{w}^{H} = S(\dot{w})^{G_H}$. Conversely, if $(S(\dot{w}),p) \in S(\dot{z})$ and $p \in G_H$, then by definition there is $b \in \mathbb{B}^+$ with $(\dot{w},b) \in \dot{z}$ and $e(p) \subset b$; since $e(p) \in H$ and filters are upward closed toward weaker Boolean conditions, $b \in H$, and again the induction hypothesis gives the same interpreted member. Thus the recursive translation preserves all name evaluations under associated generic filters.
Therefore
\begin{align*}
V[G] = V[H_G]
\end{align*}
for every $\mathbb{P}$-generic $G$, and
\begin{align*}
V[H] = V[G_H]
\end{align*}
for every $\mathbb{B}^+$-generic $H$. Hence forcing with $\mathbb{P}$ and forcing with $\operatorname{RO}(\mathbb{P}) \setminus \{\varnothing\}$ give exactly the same generic extensions.
[/step]
[step:Pass from a preorder to its separative quotient]
Let $(\mathbb{P}, \leq)$ be an arbitrary forcing preorder, with $r \leq p$ meaning that $r$ is stronger than $p$. Define the separative preorder $\leq_s$ by declaring
\begin{align*}
p \leq_s q \quad\Longleftrightarrow\quad \text{every } r \in \mathbb{P} \text{ with } r \leq p \text{ is compatible with } q.
\end{align*}
Define an [equivalence relation](/page/Equivalence%20Relation) $\equiv_s$ on $\mathbb{P}$ by
\begin{align*}
p \equiv_s q \quad\Longleftrightarrow\quad p \leq_s q \text{ and } q \leq_s p.
\end{align*}
Let
\begin{align*}
\mathbb{P}_{\mathrm{sep}} := \mathbb{P}/{\equiv_s}
\end{align*}
be the quotient ordered by
\begin{align*}
[p]_{\equiv_s} \leq [q]_{\equiv_s} \quad\Longleftrightarrow\quad p \leq_s q.
\end{align*}
The order is well-defined because replacing $p$ or $q$ by an $\equiv_s$-equivalent representative preserves the two relations $\leq_s$ and $\geq_s$ needed in the displayed definition. It is separative: if $[p]_{\equiv_s} \nleq [q]_{\equiv_s}$, then $p \nleq_s q$, so there is $r \leq p$ incompatible with $q$ in the original preorder. Then $[r]_{\equiv_s} \leq [p]_{\equiv_s}$. If some $[s]_{\equiv_s}$ strengthened both $[r]_{\equiv_s}$ and $[q]_{\equiv_s}$, choose representatives with $s \leq_s r$ and $s \leq_s q$. Since $s \leq_s r$, the condition $s$ is compatible with $r$, so choose $u \leq s,r$. Since $s \leq_s q$, the strengthening $u \leq s$ is compatible with $q$, giving $v \leq u,q$. Then $v \leq r,q$, contradicting incompatibility of $r$ and $q$. Hence $[r]_{\equiv_s}$ is incompatible with $[q]_{\equiv_s}$.
Define the quotient map $\pi: \mathbb{P} \to \mathbb{P}_{\mathrm{sep}}$ by $\pi(p) := [p]_{\equiv_s}$. The map $\pi$ is order-preserving because $p \leq q$ implies $p \leq_s q$, and it is surjective by definition of the quotient.
[guided]
The separative quotient removes exactly the information that forcing cannot detect. The relation $p \leq_s q$ means that no extension of $p$ can rule out $q$: every stronger condition below $p$ is still compatible with $q$. Mutual separative reducibility is therefore the right equivalence relation for identifying conditions.
We must check that the quotient is separative. Suppose $[p]_{\equiv_s} \nleq [q]_{\equiv_s}$. By definition this means $p \nleq_s q$, so there is $r \leq p$ incompatible with $q$. The class $[r]_{\equiv_s}$ strengthens $[p]_{\equiv_s}$. We show that it is incompatible with $[q]_{\equiv_s}$. If not, some class $[s]_{\equiv_s}$ strengthens both classes; equivalently, after choosing the representative $s$, we have $s \leq_s r$ and $s \leq_s q$. Since $s \leq_s r$, the condition $s$ itself is compatible with $r$, so choose $u \leq s,r$. Since $s \leq_s q$ and $u \leq s$, the condition $u$ is compatible with $q$, so choose $v \leq u,q$. Then $v \leq r,q$, contradicting the choice of $r$. Thus the quotient is separative.
We now compare generic filters. If $G \subset \mathbb{P}$ is $V$-generic, define
\begin{align*}
K_G := \{[q]_{\equiv_s} \in \mathbb{P}_{\mathrm{sep}} : \text{there exists } p \in G \text{ such that } [p]_{\equiv_s} \leq [q]_{\equiv_s}\}.
\end{align*}
This is a filter because $G$ is upward closed and directed, and the quotient order is defined by $\leq_s$. If $E \subset \mathbb{P}_{\mathrm{sep}}$ is dense open and belongs to $V$, then
\begin{align*}
\pi^{-1}(E) := \{p \in \mathbb{P} : [p]_{\equiv_s} \in E\}
\end{align*}
is dense open in $\mathbb{P}$. Density follows because below any $p \in \mathbb{P}$, density of $E$ gives a class $[q]_{\equiv_s} \in E$ with $[q]_{\equiv_s} \leq [p]_{\equiv_s}$; by the definition of $q \leq_s p$, some condition below $q$ is compatible with $p$, and a common strengthening $r \leq p,q$ satisfies $[r]_{\equiv_s} \leq [q]_{\equiv_s}$, so openness of $E$ gives $[r]_{\equiv_s} \in E$. Since $G$ meets $\pi^{-1}(E)$, the filter $K_G$ meets $E$.
Conversely, if $K \subset \mathbb{P}_{\mathrm{sep}}$ is $V$-generic, define
\begin{align*}
G_K := \{p \in \mathbb{P} : [p]_{\equiv_s} \in K\}.
\end{align*}
This is a filter. If $p \in G_K$ and $p \leq q$, then $p \leq_s q$, so $[p]_{\equiv_s} \leq [q]_{\equiv_s}$ and upward closure of $K$ gives $q \in G_K$. If $p,q \in G_K$, directedness of $K$ gives a class $[r]_{\equiv_s} \in K$ with $[r]_{\equiv_s} \leq [p]_{\equiv_s}$ and $[r]_{\equiv_s} \leq [q]_{\equiv_s}$. Since $r \leq_s p$, choose $a \leq r,p$; since $a \leq r$ and $r \leq_s q$, choose $b \leq a,q$. Then $b \leq p,q$, and $[b]_{\equiv_s} \leq [r]_{\equiv_s}$, so $[b]_{\equiv_s} \in K$ and $b \in G_K$.
To prove genericity of $G_K$, let $D \subset \mathbb{P}$ be dense open and belong to $V$. Define
\begin{align*}
E_D := \{[p]_{\equiv_s} \in \mathbb{P}_{\mathrm{sep}} : \text{there exists } d \in D \text{ such that } [p]_{\equiv_s} \leq [d]_{\equiv_s}\}.
\end{align*}
This definition builds openness into the quotient dense set. It is dense because, below any class $[q]_{\equiv_s}$, choose $d \in D$ with $d \leq q$; then $[d]_{\equiv_s} \leq [q]_{\equiv_s}$ and $[d]_{\equiv_s} \in E_D$. Since $K$ meets $E_D$, choose $[p]_{\equiv_s} \in K \cap E_D$ and $d \in D$ with $[p]_{\equiv_s} \leq [d]_{\equiv_s}$. Upward closure of $K$ gives $[d]_{\equiv_s} \in K$, hence $d \in G_K \cap D$. Thus $G_K$ is $V$-generic for $\mathbb{P}$.
Finally, the name translations are the direct quotient translations. A $\mathbb{P}$-name is translated by replacing each condition $p$ by $\pi(p)=[p]_{\equiv_s}$, and a quotient name is translated by replacing each class $[p]_{\equiv_s}$ by all representatives $q \in \mathbb{P}$ with $[q]_{\equiv_s} \leq [p]_{\equiv_s}$. The filter identities above give the membership equivalences needed for induction on name rank, so associated generics satisfy $V[G]=V[K_G]$ and $V[H]=V[G_H]$. This completes the forcing-equivalence part of the quotient argument.
[/guided]
We now compare generic filters directly. If $G \subset \mathbb{P}$ is $V$-generic, define the induced quotient filter
\begin{align*}
K_G := \{[q]_{\equiv_s} \in \mathbb{P}_{\mathrm{sep}} : \text{there exists } p \in G \text{ such that } [p]_{\equiv_s} \leq [q]_{\equiv_s}\}.
\end{align*}
As before, $K_G$ is a filter. If $E\subset\mathbb{P}_{\mathrm{sep}}$ is dense open and belongs to $V$, then
\begin{align*}
\pi^{-1}(E)=\{p\in\mathbb{P}:[p]_{\equiv_s}\in E\}
\end{align*}
is dense open in $\mathbb{P}$. Given $p\in\mathbb{P}$, choose $[q]_{\equiv_s}\in E$ with $[q]_{\equiv_s}\leq[p]_{\equiv_s}$. Since $q\leq_s p$, the conditions $q$ and $p$ are compatible, so choose $r\leq q,p$. Then $[r]_{\equiv_s}\leq[q]_{\equiv_s}$, and openness of $E$ gives $[r]_{\equiv_s}\in E$. Thus $r\leq p$ and $r\in\pi^{-1}(E)$. Since $G$ meets $\pi^{-1}(E)$, the filter $K_G$ meets $E$, so $K_G$ is $V$-generic for the quotient.
Conversely, let $K \subset \mathbb{P}_{\mathrm{sep}}$ be $V$-generic. Define
\begin{align*}
G_K := \{p \in \mathbb{P} : [p]_{\equiv_s} \in K\}.
\end{align*}
This is a filter. If $p \in G_K$ and $p \leq q$, then $p \leq_s q$, so $[p]_{\equiv_s} \leq [q]_{\equiv_s}$ and upward closure of $K$ gives $q \in G_K$. If $p,q \in G_K$, directedness of $K$ gives a class $[r]_{\equiv_s} \in K$ with $[r]_{\equiv_s} \leq [p]_{\equiv_s}$ and $[r]_{\equiv_s} \leq [q]_{\equiv_s}$. Since $r \leq_s p$, choose $a \leq r,p$; since $a \leq r$ and $r \leq_s q$, choose $b \leq a,q$. Then $b \leq p,q$, and $[b]_{\equiv_s} \leq [r]_{\equiv_s}$, so $[b]_{\equiv_s} \in K$ and $b \in G_K$.
To prove genericity of $G_K$, let $D \subset \mathbb{P}$ be dense open and belong to $V$. Define
\begin{align*}
E_D := \{[p]_{\equiv_s} \in \mathbb{P}_{\mathrm{sep}} : \text{there exists } d \in D \text{ such that } [p]_{\equiv_s} \leq [d]_{\equiv_s}\}.
\end{align*}
The set $E_D$ is dense open in $\mathbb{P}_{\mathrm{sep}}$. For density, below any class $[q]_{\equiv_s}$ choose $d \in D$ with $d \leq q$; then $[d]_{\equiv_s} \leq [q]_{\equiv_s}$ and $[d]_{\equiv_s}\in E_D$. For openness, if $[r]_{\equiv_s}\leq[p]_{\equiv_s}$ and $[p]_{\equiv_s}\in E_D$ via $[p]_{\equiv_s}\leq[d]_{\equiv_s}$ with $d\in D$, then $[r]_{\equiv_s}\leq[d]_{\equiv_s}$, so $[r]_{\equiv_s}\in E_D$. Since $K$ meets $E_D$, choose $[p]_{\equiv_s}\in K\cap E_D$ and $d\in D$ with $[p]_{\equiv_s}\leq[d]_{\equiv_s}$. Upward closure of $K$ gives $[d]_{\equiv_s}\in K$, hence $d\in G_K\cap D$. Therefore $G_K$ is $V$-generic for $\mathbb{P}$.
At the level of names, define $T_\pi$ by replacing each condition $p$ in a $\mathbb{P}$-name by $\pi(p)$:
\begin{align*}
T_\pi(\dot{x})=\{(T_\pi(\dot{y}),[p]_{\equiv_s}):(\dot{y},p)\in\dot{x}\}.
\end{align*}
For quotient names define $S_\pi$ by refining each quotient condition to original representatives below it:
\begin{align*}
S_\pi(\dot{z})=\{(S_\pi(\dot{w}),p):\text{there is }[q]_{\equiv_s}\text{ with }(\dot{w},[q]_{\equiv_s})\in\dot{z}\text{ and }[p]_{\equiv_s}\leq[q]_{\equiv_s}\}.
\end{align*}
The filter correspondences proved above are exactly the membership equivalences needed for induction on name rank. Hence
\begin{align*}
V[G] = V[K_G]
\end{align*}
and
\begin{align*}
V[K] = V[G_K].
\end{align*}
Therefore forcing with $\mathbb{P}$ and forcing with $\mathbb{P}_{\mathrm{sep}}$ give the same generic extensions.
Applying the earlier separative case to $\mathbb{P}_{\mathrm{sep}}$ gives a dense embedding
\begin{align*}
\mathbb{P}_{\mathrm{sep}} \hookrightarrow \operatorname{RO}(\mathbb{P}_{\mathrm{sep}}) \setminus \{\varnothing\},
\end{align*}
and hence forcing with the original preorder $\mathbb{P}$ is equivalent to forcing with this Boolean completion. This proves the stated conclusion for arbitrary forcing preorders.
[/step]
Prerequisites (0/2 completed)
Prerequisites Graph
Interactive dependency map showing how this theorem builds on foundational concepts
Loading dependency graph...
Theorem
Definition
Current
Requires
Definitions & Concepts
Explore Further
Equivalence Relation
Definition
Open Set
Definition
Omega Is an Isometric Involution
Combinatorics
Downward Löwenheim-Skolem Theorem for Countable Elementary Submodels of $H_\theta$
Logic
Colorful Caratheodory Theorem
Combinatorics
Gentzen Consistency Theorem for First-Order LK
Logic
Characterization of PA Degrees by Paths through Nonempty $\Pi^0_1$ Classes
Logic
Chang Large Spectrum Lemma
Combinatorics
Closure Under Union and Concatenation
Discrete Mathematics
Topological Tverberg Theorem for Prime Powers
Combinatorics
Discrete Mathematics
Area
Set Theory
Subarea