In Kunen's Set Theory: An Introduction to Independence Proofs, Ch. VII, section 3, page 195, in definition 3.3 about forcing equality, it reads:
$p \Vdash^* t_1 = t_2 \text { iff } \\ \space \space (\alpha) \ \text {forall } \langle \pi_1,s_1 \rangle \in t_1,\\ \space\\ \space \space \{q \leq p : q \leq s_1 \to \exists \langle \pi_2,s_2 \rangle \in t_2 \,(q \leq s_2 \land q \Vdash^* \pi_1=\pi_2)\} \\ \space \\ \text {is dense below } p, \text { and } \\ \space \space (\beta) \ \text{forall } \langle \pi_2,s_2 \rangle \in t_2,\\ \space \\ \space \space \{q \leq p : q \leq s_2 \to \exists \langle \pi_1,s_1 \rangle \in t_1 \, (q \leq s_1 \land q \Vdash^* \pi_1=\pi_2)\} \\ \space \\\text { is dense below } p$.
My question is that this definition includes conditions $q \leq p \land q \not \leq s_1$ , and $q \leq p \land q \not \leq s_2$ in the definition of the first and second sets respectively?
What's the reason for including those conditions? Why not just using sets:
$\{q \leq p : q \leq s_1 \land \exists \langle \pi_2,s_2 \rangle \in t_2 \, (q \leq s_2 \land q \Vdash^* \pi_1=\pi_2)\} \\ \{q \leq p : q \leq s_2 \land \exists \langle \pi_1,s_1 \rangle \in t_1 \, (q \leq s_1 \land q \Vdash^* \pi_1=\pi_2)\}$
in the above definition?
Best Answer
Here is an outline answer for those fairly new to Forcing (with P-names having a dot over them):
Taking as the example :
$p \Vdash^* \dot t_1 = \dot t_2 \text { iff } \\ \space \space (\alpha) \ \text {forall } \langle \dot \pi_1,s_1 \rangle \in \dot t_1,\\ \space\\ \space \space \{q \leq p : q \leq s_1 \to \exists \langle \dot \pi_2,s_2 \rangle \in \dot t_2 \,(q \leq s_2 \land q \Vdash^* \dot \pi_1=\dot \pi_2)\} \\ \space \\ \text {is dense below } p$
Lets assume for simplicity, in $\Bbb P$, below the element p there are just two disjoint branches, one containing $s_1$ and one not containing $s_1$. One key point to note is that $q \nleq s_1$ has two possible solutions in a partial order : [$q > s_1$] OR [$ q \ngtr s_1$ AND $ q \nleq s_1$]. So $q \nleq s_1$ could include all $q < p$ in the branch not containing $s_1$.
The intended interpretation of $p \Vdash^*$ is that all G which contain p will satisfy $(\alpha)$ in the model M[G] containing G. However within the base model M not even one G is known. So $(\alpha)$ must work with all G containing p and all possible $\Bbb P$ in M. (We will for ease restrict $\Bbb P$ to the example mentioned above)
There are two cases :
Case 1 : $\langle \dot \pi_1,s_1 \rangle$ is not activated
Some (or all) of these G do not contain $s_1$, so may have elements in the path below p not containing $s_1$, or above $s_1$ but less than p. In this case it doesn't matter since $\langle \dot \pi_1,s_1 \rangle$ will not be activated when determining the expressions true in M[G] and will take no part in determining equality of $\dot t_1$[G] and $\dot t_2$[G] in M[G]. So these particular $q \nleq s_1$ are valid inputs to $(\alpha)$.
Case 2 : $\langle \dot \pi_1,s_1 \rangle$ is activated
Some (or all) of these G do contain $s_1$ and in this case $(\alpha)$ applies with the cases $q \leq s_1 $.
Always achieving dense below p when required
Since $(\alpha)$ has to work with both those G not containing $s_1$, and with those G containing $s_1$, then both cases $q \nleq s_1$ and $q\leq s_1$ need to be included in the dense set definition. If only the $q\leq s_1$ cases were included then the set in $(\alpha)$ may not be dense below p, since there would be no elements from the path below p not containing $s_1$ (in the $\Bbb P$ assumed in this answer).