Generic extension

If $G$ is a generic filter over a countable transitive model $M$, the generic extension $M[G]$ consists of the interpretations by $G$ of all forcing names in $M$.

The forcing theorem identifies truth in a generic extension with the forcing relation: a formula is true in $M[G]$ exactly when some condition in $G$ forces it.