Definition (Interpretation of forcing language). If $G$ is a $\mathbb{P}$-generic over $M$ and $\phi$ is in the forcing language, we say

$$M[G]\models \phi$$

if and only if

$$M[G],v\models \phi$$

where $v(\tau ):=\mathrm{val}(\tau ,G)$.