9
$\begingroup$

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.

$\endgroup$
11
  • 6
    $\begingroup$ 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) $\endgroup$
    – David Roberts
    Oct 10, 2014 at 23:17
  • 4
    $\begingroup$ 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. $\endgroup$ Oct 10, 2014 at 23:41
  • 3
    $\begingroup$ @user40276: Follow up question, why? $\endgroup$
    – Asaf Karagila
    Oct 11, 2014 at 10:46
  • 3
    $\begingroup$ An explicit presentation of forcing in terms of intuitionistic Kripke models is given in Melvin Fitting’s “Intuitionistic logic model theory and forcing”. $\endgroup$ Oct 11, 2014 at 20:51
  • 3
    $\begingroup$ 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.) $\endgroup$ Nov 2, 2015 at 4:11

1 Answer 1

11
$\begingroup$

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.

$\endgroup$
2
  • 3
    $\begingroup$ 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. $\endgroup$ Oct 11, 2014 at 19:25
  • 1
    $\begingroup$ I prefer to include $\lnot,\land$ and $\exists$. $\endgroup$
    – Asaf Karagila
    Oct 11, 2014 at 22:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.