Why is intuitionistic modelling called forcing? In classical model theory, the relation $\vDash$ is usually pronounced as "models", e.g. I would read something like $\mathcal{M}\vDash \phi$ as "M models phi".
For intuitionistic Kripke semantics, there is the notion of $\Vdash$, which is very similar to the classical $\vDash$, but usually pronounced as "forces". 
Is this just a case of various logicians inventing various names for the same thing, or is there some nontrivial reason for this? I feel it might have something to do with set theoretic forcing.
 A: In Kriple semantics, each node has two relations, $\models$ and $\Vdash$. In the simplest case, intuitionistic propositional logic, each node is a model in the classical sense for some limited alphabet in propositional logic. 
The magic of Kripke frames is to use partially ordered collections of classical models to study intuitionistic logic (and to study modal logic as well).    The key point is that, classically, to satisfy $A \to B$ just means to satisfy $B$ or not to satisfy $A$. But to force $A \to B$ is stronger: it means that in every descendant of the node, if $A$ is true in that descendant then $B$ is also true in the descendant.   So the entire point is that $\Vdash$ is not the same as $\models$.  
The completeness theorem for intuitionistic logic and Kripke frames shows that the logic of the forcing relation $\Vdash$ aligns exactly with intuitionistic logic.  
Moreover, in modal logic, there is no clause for the $\Box$ or $\Diamond$ connectives in the definition of the classical $\models$ relation. But there are definitions for what it means to force a formula beginning with one of these connectives. 
This is closely related to forcing in set theory, as well. Some older set theory texts worked with a "strong" forcing relation, which only yielded an intuitionistic logic. These texts then used a double negation embedding of classical logic into intuitionistic logic in order to study forcing in classical logic.  More recent set theory texts often incorporate the double negation translation directly into the definition of the forcing relation, or use a more semantic definition that automatically gives classical logic. This can obscure the underlying intuitionistic nature of set theoretic forcing. 
