Unramified forcing preserving the law of double negation

Shoenfield's unramified version of Cohen's forcing is defined in two stages: one which does not preserve double negation and the other which modifies the former so as to preserve double negation. Here we express the unramified forcing, which preserves double negation, in a single stage. Surprisingly enough, the corresponding definition of forcing for equality acquires a rather simple form. In 2] forcing ∥- is expressed in terms of strong forcing \( \Vdash * \) viap∥-Q iffp \( \Vdash * \) ¬ ¬Q for every formulaQ ofZF set theory and every elementp of a partially ordered set (P, ≦). In its turn,p \( \Vdash * \) Q is defined by the following five clauses: (1) $$p \Vdash * a \in biff(\exists c)(\exists q \geqq p)((c,q) \in b \wedge p \Vdash * a = c)$$ (2) $$\begin{gathered} p \Vdash * a \ne biff(\exists c)(\exists q \geqq p)(((c,q) \in a \wedge p \Vdash * c \notin b) \hfill \\ ((c,q) \in b \wedge p \Vdash * c \notin a)) \hfill \\ \end{gathered} $$ (3) $$p \Vdash * \neg Qiff(\forall q)(q \leqq p \to \neg (q \Vdash * Q))$$ (4) $$p \Vdash * (Q \vee S)iff(p \Vdash * Q) \vee (p \Vdash * S)$$ (5) $$p \Vdash * (\exists x)Q(x)iff(\exists b)(p \Vdash * Q(b))$$ .