Is there a forcing argument of this fact? Can anybody point me to the place?
The reason I'm asking is because I was reading Heyting-Valued Models for Intuitionistic Set Theory by R.J. Grayson, yet the proof of the theorem is largely the following quotation:
$\text{For }x\subseteq 1,\text{ set }\bar{x}=\{y \in 1: y \notin x \}\text{ and let }\Omega=\{x\subseteq 1\;:\;x=\bar{\bar{x}}\}$
$\text{ so }\Omega\text{ is a }\underline{\text{complete Boolean algebra}}\text{ in IZF.}$
$\text{We denote this} \quad cBa \quad \text{by}\\P(1)/\neg\neg$
$\text{since it is the quotient of }P(1) \text{ under the }\neg\neg\text{-operator}$.
So is the above simply a re-hash of the godelian "$\varphi$ is a theorem of $ZF$ if and only if $\neg\neg\varphi$ is a theorem in $IZF$" or is it something slightly more sophisticated? I am in particular looking for a forcing argument of this claim...
I was imagining something like the following: Let $V$ be the universe of $IZF$, we construct a heyting valued model as follows. Let $\Omega_H := H$ where H is an arbitrary complete Heyting algebra. Define $V^{H}\in V$, i.e., $V^{H}=\bigcup V_{\alpha}^H$, in the normal way. We have $V^H \models IZF$. Let $\mathbb{P}=H$ be our forcing poset(Is this allowed?). Just as in the quote, for $x \subseteq 1$, set $\bar{x}=\{y \in 1: y \notin x \}$ and let $B=\{x \subseteq 1 : x = \bar{\bar{x}}\}$. Can we write $V^H/ \Omega_B=V^H[ \Omega_B]=V^B$, where $V^B$ is a Boolean valued model with $\Omega_B:=B$, or does this not make sense?
Edit: Also, I have read that forcing's relation to double negation is somehow related to "strong" versus "weak" forcing -- but I have a hard time finding definitions of these terms...