# 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.

• The link is S.Kripke, Semantical Analysis of Intuitionistic Logic I, JSL (1965) (that not uses $\Vdash$): Section 1.3.1 (page 118) is dedicated to discuss the link of Kripke's model theory for intuitionistic logic with Cohen's notion of "forcing". Feb 13, 2018 at 10:59

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.

• I am afraid I may be switching the words "strong" and "weak" in the older style forcing relations. Feb 11, 2018 at 19:33
• There is a long essay by Paul Cohen, the inventor of forcing, titled The Development of Forcing, (I read only part of it) If he chose the word "forcing" then that explains the terminology, Especially as he won a Fields Medal for it. Feb 12, 2018 at 8:28
• In usual presentations of the intuitionistic propositional calculus with Kripke semantics I have never seen the relation $\models$ employed (usually only the forcing relation is supplied). How come? Can you cite an exposition where both are employed? Mar 21, 2018 at 11:08
• @user65526: in Kripke semantics each world is a model in the classical sense (of propositional logic or first-order logic, say). As such, each world has its own $\models$ relation. This may be written as $w \models \phi$ or some other way (e.g. the SEP writes $v(w,\phi) = T$ plato.stanford.edu/entries/logic-modal/#PosWorSem ). In any case, there is some $\models$ relation to define truth in each world. Of course, this is not the relation of the most interest - the forcing relation is the ultimate goal, because that gives the definition of modal truth in the overall Kripke frame. Mar 21, 2018 at 13:40