What is the reasoning behind the negation definition in Intuitionistic Logic Forcing and Set Theory Forcing?

Question

In Kunen page 96 - of 10th impression 2006:

(p $\Vdash^* \neg A) \iff $ $\forall q \leq p \; \neg \; (q \Vdash^* A)$

Similarly in https://www.logicmatters.net/resources/pdfs/LogicStudyGuide.pdf on page 97 it states :

(k $\Vdash$ ¬A) $\iff$ for any k′ such that k ≤ k′, $\neg \;$ (k′ $\Vdash$ A)

In Cohen "Set Theory and the Continuum Hypothesis" Cohen states on page 117:

(P forces $\neg $ A) $\iff$ $\forall Q \supseteq P \; \neg \; (Q$ forces A)

All these definitions are the same (taking account of the definitions of $\leq$ and $\geq$), so taking the Intuitionistic definition - my question is

"What is the purpose and reasoning behind the choice of the definition of the right to left implication :

$(k \Vdash ¬A) \Longleftarrow \forall k′ \geq k \; \neg \; (k′ \Vdash A) \tag{1}$

or equivalently its contrapositive (using classical logic in the Metatheory defining the forcing relation) :

$ \neg \; (k \Vdash ¬A) \Longrightarrow \exists k′ \geq k \; (k′ \Vdash A) \tag{1a}$

I ask because it appears that :

(i) The right to left definition in equation (1) doesn't seem Intuitionistic and looks to be a 'back door' to the ($ A \lor \neg A$) formula, since it is a "failure to find a ($k' \geq k \; k' \Vdash A$)" implies that "$(k \Vdash ¬A)$". However why can't there exist a k' $\geq$ k that has $(k' \Vdash ¬A)$, and both $(k \Vdash ¬A)$ and $(k \Vdash A)$ be not be derivable, e.g. if there isn't enough information in k to force $\neg$ A or force A?

(ii) Cohen shows that equation (1a) leads to forcing becoming negation complete i.e. :

$$ \forall k \; \forall A \; (\exists k' \geq k) : (k' \Vdash A) \; OR \; (k' \Vdash \neg A) $$ However I thought Intuitionistic logic wasn't negation complete (though I couldn't find anything on the web relating Intuitionistic logic and negation completeness)

(iii) Whenever $ k_0 \leq k_1 \leq k_2 ...$ and there is a $k_n \Vdash \neg A$ then :

If we assume forcing is consistent, $\forall k_i \geq k_0 \; \neg \; (k_i \Vdash A) $ will hold and therefore using equation (1) then $$(k_n \Vdash \neg A) \implies \forall k \geq k_0 \; (k \Vdash \neg A) \; $$ which doesn't look 'right' if its correct.

Similarly if there is a $k_n \Vdash A$ then :

If we assume forcing is consistent, $\forall k_i \geq k_0 \; \neg \; (k_i \Vdash \neg A) $ will hold and therefore using equation (1) then $$(k_n \Vdash A) \implies \forall k \geq k_0 \; (k \Vdash \neg \neg A) \; $$ which also doesn't look 'right' if its correct.

Indeed $k_0$ would be able to force the appropriate $\neg A$ or $\neg(\neg A)$ for all formulae A and so would it fall foul of the Godel Incompleteness theorems ?

(iv) I couldn't derive equation (1) from the assumption of negation completeness, I got instead, with no other assumptions :

$$ \exists k'' \geq k : (k'' \Vdash ¬A) \Longleftarrow \forall k′ \geq k \; \neg \; (k′ \Vdash A)$$

Answer 1

Some partial answers:

For (iv), consider the following:$$(*)\forall k [(\exists k'' \geq k : (k'' \Vdash ¬A)) \Longleftarrow \forall k′ \geq k \; \neg \; (k′ \Vdash A)]$$ This implies $$\forall k\{k' \geq k :(k' \Vdash A) \; OR \; (k' \Vdash \neg A)\}$$ is dense below $k$. So if you mean in (*) in (iv), then (iv) works.

For (i), I think Cohen wants truth in the forcing extension M[G] can be forced in the ground model M, that is, for any given A, whether M[G]\models A can be decided in M. That is exactly what the forcing theorem says. Since $M[G]\models A$ or $\neg A$ is true, without loss of generality, assume M[G]\models A, then for any condition $p$ and any generic filter $G$ containing $p$, there must be some stronger $q$ forces $A$.

For (ii), first note the book of either Kunen's or Cohen's is working under first-order logic. Secondly note the difference between the two notions of forcing. Kunen and Cohen's book are talking set-theoretic forcing in Set Theory under first-order logic. Set-theoretic forcing is merely a tool helping us extending set-theoretic model(structure)s. Validity in first-order logic has nothing to do with set-theoretic forcing ($A$ is valid if $M\models A$ for any structure $M$). But validity in intuitionistic is depend on (defined by) forcing (see page 97 in the second reference you cited.
). You may find a poof of the non-intuitionistic validity of ($A$ or $\neg A$) in page 97-98 in the second reference you cited.

I do not understand your question in (iii). What do you mean "forcing is consistent" ?

Answer 2

I would argue that you're putting the cart before the horse, here. Forcing follows a very snappy theme - "how do generic objects behave?" - and the behavior of negation in forcing is really inhereted from the basic nature of the background mathematics. When we view forcing "intrinsically" in this way, there's no surprising definition of the behavior of negation but rather a provable consequence of a very natural definition of forcing that makes no reference to syntax at all.

(This is certainly not the only way to approach the problem, but I think it's the one that makes things clearest.)

---

Consider the following topological version of forcing (and skip to the end of this answer - the section starting "At this point ..." - for the connection between this material and forcing as usually presented!): we have a topological space $\mathcal{T}=(X,\tau)$ and a collection $\mathscr{P}$ of properties of points that we care about called ... "properties." We start by asking about the "generic" behavior of points in $\mathcal{T}$:

Q1: For which properties $\varphi\in\mathscr{P}$ is the set $$S_\varphi:=\{x\in X: \varphi(x)\}$$ $\tau$-comeager?

(Why do we care about comeager behavior rather than all-of-$X$ behavior? Well, experience from a number of areas in mathematics - including algebraic geometry, incidentally - suggests that allowing a small number of "pathological" points to not impact our notion of generic behavior is usually a good idea.)

We can also ask "local" versions of Q1 above:

Q2: Suppose $U$ is $\tau$-open (and nonempty!). For which properties $\varphi\in\mathscr{P}$ is the set $$S_\varphi^U:=\{x\in U: \varphi(x)\}$$ $\tau_U$-comeager, where $\tau_U=\{W\cap U: W\in\tau\}$ is the subspace topology on $U$ coming from $\tau$?

The point is this:

We now have a forcing relation!

Specifically, for $U$ an open subset of $\mathcal{T}$ and $\varphi$ a property in $\mathscr{P}$, we write $U\Vdash \varphi$ iff the set $S_\varphi^U$ is $\tau_U$-comeager. Note that there is no negation in sight ... yet.

Now let's make two assumptions about $\mathscr{P}$.

Our first assumption is forcing-related; effectively, this says that we have a "truth=forcing" result:

Assumption 1: There is a $\tau$-comeager set $C\subseteq X$ such that for every $\varphi\in\mathscr{P}$ and every $x\in C$ there is an open $U\ni x$ such that every $y\in C\cap U$ has $\varphi(y)\leftrightarrow \varphi(x)$.

Our second assumption is "syntactic" in a sense, and says that $\mathscr{P}$ satisfies a mild closure property:

Assumption 2: $\mathscr{P}$ is closed under negation, that is, for every property $\varphi\in\mathscr{P}$ there is a $\psi\in\mathscr{P}$ such that $$S_\psi=X\setminus S_\varphi.$$ (We'll write $\neg\varphi$ for such a $\psi$.)

(Now you might wonder why I'm talking about properties at all instead of just sets of points, and that's a fair question; in my opinion, talking about properties keeps the intuition clearer, but that's subjective.)

Again, I want to stress that negation has so far only appeared on the "properties" side of things. The behavior of negation on the forcing side of things is now a provable result:

Claim: Let $C$ be as in assumption $1$, and let $\varphi\in\mathscr{P}$. Then for every nonempty $\tau$-open set $U\subseteq X$ the following are equivalent:

1. $U\Vdash\neg\varphi$.

2. There is no nonempty $\tau$-open $W\subseteq U$ such that $W\Vdash\varphi$.

Proof: Immediately from the definition we see that forcing is monotonic, in the sense that if $U$ and $V$ are nonempty $\tau$-open sets with $U\supseteq V$ then $U\Vdash\varphi\implies W\Vdash\varphi$ for every $\varphi\in\mathscr{P}$. This gives us $1\rightarrow 2$.

For $2\rightarrow 1$, note that if $2$ holds then by assumption $1$ there cannot be any $x\in U\cap C$ such that $\varphi(x)$ holds (otherwise take the $W$ as given by assumption $1$ and consider $U\cap W$). But this means that $S^U_\varphi$ is $\tau_U$-comeager, that is, $U\Vdash \varphi$. $\quad\Box$

The point is this:

The logical structure of $\Vdash$, as developed here, simply recapitulates the logical properties of $\mathscr{P}$ (e.g. closure under negation)

At this point I can give the precise connection between the topological picture above and the standard set-theoretic picture of forcing with a (nontrivial) poset $\mathbb{P}$ over a c.t.m. $M$:

• $X$ is the set of all maximal filters through $\mathbb{P}$, and $\tau$ is the topology on $X$ generated by $\{\{G\in X: p\in G\}: p\in\mathbb{P}\}$.

• $C$ is the set of all points in $X$ which are $\mathbb{P}$-generic over $M$.

Of course, neither $X$ nor $C$ is an element of $M$ (indeed, $C\cap M=\emptyset$), but who cares?

• $\mathscr{P}$ is then the set of properties of the form $$M[G]\models\varphi$$ for $\varphi$ a sentence in the first-order forcing language in the usual sense.

Note, of course, that assumption 1 (in any particular case including the set-theoretic one) requires proof. But this is exactly what the forcing theorem does, at least for $\mathcal{T}$ and $\mathscr{P}$ of the above form.

Answer 3

Like many foundational aspects of forcing, this makes more sense (to me) if we think first about Boolean-valued models. In that context, formulas $A$ have truth values $\Vert A\Vert$ in a completeBoolean algebra $\mathcal B$, and the propositional connectives for formulas correspond to the Boolean operations in $\mathcal B$. In particular, propositional negation $\neg$ corresponds to Boolean complement: $\Vert\neg A\Vert=-\Vert A\Vert$.

The transition from Boolean-valued models to forcing consists of working not with the complete Boolean algebra $\mathcal B$ but with a dense subset $P$ of its non-zero part $\mathcal B-\{0\}$. ("Dense" means that each non-zero element of $\mathcal B$ is $\geq$ some element of $P$.) Instead of talking about elements $b\in\mathcal B$, one talks about $\{p\in P:p\leq b\}$. In particular, one says that $p$ forces $A$ and one writes $p\Vdash A$ iff $p\leq\Vert A\Vert$.

So to describe "forcing $\neg A$" in terms of "forcing $A$", we must figure out how to express (for elements $p\in P$) that $p\leq-b$ in terms of $p\leq b$.

It is an easy exercise in Boolean algebra to show that, for any elements of any Boolean algebra, we have $p\leq-b$ iff $0$ is the only element $c$ that simultaneously satisfies $c\leq p$ and $c\leq b$.

Finally, using the fact that $P$ is dense in $\mathcal B-\{0\}$, we find that the $c$ in this criterion can be understood as ranging only over $P$ (and then $0$ is no longer an exception, since $0\notin P$) without any change in the meaning. So we get $p\leq-b$ iff no element $q\in P$ simultaneously satisfies $q\leq p$ and $q\leq b$. In particular, taking $\Vert A\Vert$ as $b$, we get that $p\Vdash\neg A$ iff no $q\leq p$ in $P$ satisfies $q\Vdash A$.