[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.[/step]

[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: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. 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]

[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]