Past exam of the mathematics course of the University of Cambridge / 2013 / iii / Paper 19 / 5 / i / c / Solution

For a countable transitive ground model, the semantic forcing relation isThe forcing theorem identifies this with the recursively defined relation inside $M$ and makes it definable there. In particular, if $r\ge q$ is stronger, then $q⊩\phi$ implies $r⊩\phi$. The names are interpreted in each relevant generic filter, not replaced by their value in one fixed extension in the definition.