forcing relation

If $𝔐$ is a transitive model of set theory and $P$ is a partial order then we can define a forcing relation:

$$p{⊩}_P\varphi ({\tau }_1,\mathrm{\dots },{\tau }_n)$$

($p$ forces $\varphi ({\tau }_1,\mathrm{\dots },{\tau }_n)$)

for any $p\in P$, where ${\tau }_1,\mathrm{\dots },{\tau }_n$ are $P$- names.

Specifically, the relation holds if for every generic filter $G$ over $P$ which contains $p$,

$$𝔐[G]\models \varphi ({\tau }_1[G],\mathrm{\dots },{\tau }_n[G])$$

That is, $p$ forces $\varphi$ if every of $𝔐$ by a generic filter over $P$ containing $p$ makes $\varphi$ true.

If $p{⊩}_P\varphi$ holds for every $p\in P$ then we can write ${⊩}_P\varphi$ to mean that for any generic $G\subseteq P$, $𝔐[G]\models \varphi$.