composition of forcing notions

Suppose $P$ is a forcing notion in $\mathfrak{M}$ and $\hat{Q}$ is some $P$ -name such that $\Vdash_{P}\hat{Q}$ is a forcing notion.

Then take a set of $P$ -names $Q$ such that given a $P$ name $\tilde{Q}$ of $Q$ , $\Vdash_{P}\tilde{Q}=\hat{Q}$ (that is, no matter which generic subset $G$ of $P$ we force with, the names in $Q$ correspond precisely to the elements of $\hat{Q}[G]$ ). We can define

P*Q=\{\langle p,\hat{q}\rangle\mid p\in P,\hat{q}\in Q\}

We can define a partial order on $P*Q$ such that $\langle p_{1},\hat{q}_{1}\rangle\leq\langle p_{2},\hat{q}_{2}\rangle$ iff $p_{1}\leq_{P}p_{2}$ and $p_{1}\Vdash\hat{q}_{1}\leq_{\hat{Q}}\hat{q}_{2}$ . (A note on interpretation: $q_{1}$ and $q_{2}$ are $P$ names; this requires only that $\hat{q}_{1}\leq\hat{q}_{2}$ in generic subsets contain $p_{1}$ , so in other generic subsets that fact could fail.)

Then $P*\hat{Q}$ is itself a forcing notion, and it can be shown that forcing by $P*\hat{Q}$ is equivalent to forcing first by $P$ and then by $\hat{Q}[G]$ .

Title	composition of forcing notions
Canonical name	CompositionOfForcingNotions
Date of creation	2013-03-22 12:54:20
Last modified on	2013-03-22 12:54:20
Owner	Henry (455)
Last modified by	Henry (455)
Numerical id	4
Author	Henry (455)
Entry type	Definition
Classification	msc 03E35
Classification	msc 03E40
Related topic	Forcing