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? 
Thanks in advance.
 A: It seems to me that the "more philosophical" reason why forcing is intuitionistic is that forcing and intuitionistic logic have similar interpretations of the logical connectives and quantifiers. This is also why forcing is related to Kripke models and why Kripke models give semantics for intuitionistic logic; and it is also why intuitionistic logic is related to realizability.  From an informal perspective, these all have a viewpoint that aligns closely with the BHK interpretation of intuitionistic logic.  
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.)
This intuition about forcing leads to a forcing relation known as "strong forcing", which is what we obtain if we define forcing by directly considering the intuitionistic meaning of each of the connectives, as in the BHK interpretation. This will look very similar to the definition of the forcing relation in a Kripke model.  We can then obtain a "weaker" classical forcing relation by using a double-negation translation to embed classical logic into the intuitionistic logic of the strong forcing relation.  This classical forcing relation is weaker in that it allows a condition to force a formula (such as a disjunction or an existential formula) without providing as much evidence about why the formula will hold.  
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. 
In modern accounts of forcing, when the goal is to obtain classical models, the authors often bypass strong forcing entirely, and begin with a different definition of forcing that somehow has double-negation translation embedded into its definition. 
