There is a lemma in Kunen's book Set theory edition Studies in logic 34: lemma IV.2.30(5) $$p\Vdash\varphi \text{ iff }\neg \exists q\leq p[q \Vdash\neg\varphi].$$
This equivalence has by elementary formal logic $2$ parts:
$(p$ forces $\varphi$ or some extension forces $\neg \varphi)$ and $(p\not \Vdash\varphi$ or no extension forces $\neg\varphi).$
My question is what metamathematicaly says the $2$nd conjunct :
$(p\not \Vdash\varphi$ or no extension forces $\neg\varphi).$
Can it be described around? I simply do not understand its meaning.
Remember that "no extension of $p$ forces $\neg\varphi$" is by definition of the forcing relation equivalent to "$p$ forces $\neg\neg\varphi$." Intuitively, this should be equivalent to "$p$ forces $\varphi$," and if you believe this then the second conjunct is obvious. Also note that "$p$ forces $\varphi$" clearly implies "$p$ forces $\neg\neg\varphi$."
So the real content of the second conjunct is basically saying that we have double negation elimination in this context.