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)$$
Best Answer
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}$:
(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:
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:
Our second assumption is "syntactic" in a sense, and says that $\mathscr{P}$ satisfies a mild closure property:
(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:
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?
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.