# Forcing is intuitionistic

The main idea of why it´s necessary a generic filter $G$ to extend a countable transitive $\epsilon$-interpretation (not necessarily a model) $M$ is given by the condition (for which $G$ being a generic filter can be derived):

For each formula $\varphi(x_1, ..., x_n)$ there exists a formula $Q_{\varphi} (x, x_1, ..., x_n)$ (usually denoted by $x \Vdash \varphi (x_1, ...x_n)$), such that $$\forall m_1, ..., m_n \in M(\varphi^{ M[ G ] } (F_G (m_1), ...,F_G (m_n)) \equiv \exists p \in G; Q_{\varphi}^M (p, m_1, ..., m_n)))$$

where $F_G$ is the collapsing function from $M$ with the relation $R_G (x, y) : \exists p \in G; (p, x) \in y$.

However $Q_{\neg \neg \varphi} \not\equiv Q_{\varphi}$, so it´s intuitionistic in some sense. I think that it´s what inspired the Kripke semantics. But I don´t think it can be mere coincidence.

So the question is Is there a more philosophical reason for why forcing is intuitionistic?

• Because forcing is really the internal language of some topos, and topos logic is in general intuitionistic? It's a special case that you end up with Boolean logic because for ZFC applications you take what is called the 'double negation topology'. Other sorts of forcing are possible (e.g. Heyting-valued models in material language) – David Roberts Oct 10 '14 at 23:17
• The set-theoretic forcing relation does satisfy double-negation elimination. (However, the mostly obsolete strong forcing relation does not.) Kripke models also have a relation denoted $\Vdash$ which does not necessarily satisfy double-negation elimination. Since Kripke models precede forcing historically, I don't think it's Cohen that inspired Kripke. – François G. Dorais Oct 10 '14 at 23:41
• @user40276: Follow up question, why? – Asaf Karagila Oct 11 '14 at 10:46
• An explicit presentation of forcing in terms of intuitionistic Kripke models is given in Melvin Fitting’s “Intuitionistic logic model theory and forcing”. – Emil Jeřábek 3.0 Oct 11 '14 at 20:51
• Have you checked Kreisel (1961) "Set-theoretic problems suggested by the notion of potential infinity"? As mentioned in MO 124011, Kreisel claimed he had a form of forcing in his interpretation of intuitionism in that paper. (Cf. the historical treatment of forcing by G.H. Moore.) – Benjamin Dickman Nov 2 '15 at 4:11

For example, an intuitionistic proof of $(\exists x)\phi(x)$, by the BHK interpretation, consists of an object $c$ and a proof of $\phi(c)$. If we apply the same intuition to forcing, we would suspect that if a condition $p$ "forces" $(\exists x)\phi(x)$ to hold, there should be a term $t$ such that $p$ forces $\phi(t)$ to hold. (This intuition can be complicated, in the case of set-theoretic forcing, by the fact that the term $t$ will be a $P$-name. But for recursion-theoretic forcing, $t$ may well just be a natural number.)
For example, in recursion theoretic Cohen forcing over a model of PA to construct a generic $G \subseteq \mathbb{N}$, with the classical forcing relation $\Vdash$, we have $\langle\rangle \Vdash [5 \in G \lor 5 \not \in G]$, even though $\langle\rangle \not \Vdash 5 \in G$ and $\langle\rangle \not\Vdash 5 \not \in G$. This is because $\langle\rangle$ strongly forces $\lnot\lnot (5 \in G \lor 5 \not \in G)$. Similarly $\langle\rangle$ forces $(\exists x)[x \in G]$ without strongly forcing any particular number to be in $G$, because $\langle\rangle$ does not strongly force $G$ to be empty.
• Some modern accounts also incorporate classical logic into the definition of forcing by beginning with a limited set of connectives (e.g. including $\lnot$, $\land$, and $\forall$, but not $\exists$ and not $\lor$), and then assuming the other connectives are given by their classical definitions, which are not intuitionistically correct. – Carl Mummert Oct 11 '14 at 19:25
• I prefer to include $\lnot,\land$ and $\exists$. – Asaf Karagila Oct 11 '14 at 22:31