I was doing an exercise out of Jech's "Set Theory," and noticed something somewhat interesting. This is exercise 14.7 in Jech.
Let $D=\{q:q\Vdash\varphi\}$ be dense below $p$. If there exists some $r\leq p$ such that $r\Vdash\lnot\varphi$ then, by Theorem 14.7 (iia), for all $s\leq r, s\Vdash\lnot\varphi$, contradicting the density of $D$. So no $r\leq p$ forces $\lnot\varphi$ and, by the same theorem, $p\Vdash\lnot\lnot\varphi.$ Thus, $p\Vdash\varphi$.
Don't worry if this proof is not entirely correct, that's not what I'm asking about. It was thrown together very quickly. Here's the interesting note. Excluded middle was used here. And it appears that for many of these arguments (but not for all!) that excluded middle is used. My question is about the interplay between constructive mathematics and forcing. It is very obvious to me that arguments like this cannot be used in constructive mathematics, but is there a scenario in which they can? Several exercises did not use excluded middle, so I wonder where exactly the line is.
How much modern set theory involving forcing can be done without assuming excluded middle?