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)$$


4 Answers 4


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.

  • $\begingroup$ Apologies, I can't work out what either Assumption 1 or 2 is doing. About Assumption 1 : Should it be "..that for each $\varphi$ there exists an x $\in$ C which gives ...." (i.e. there will always be at least one x that will be able to have $\varphi$ true in $\mathscr{P}$)? What does $\varphi(y)\leftrightarrow \varphi(x)$ mean ? Does it refer to when $\varphi$ is true and when $\varphi$ is not true ? Or is it that they take on the same truth value (which is true). How is it related to "truth=forcing" ? $\endgroup$
    – user239186
    Aug 26, 2022 at 7:29
  • $\begingroup$ @LittleCheese No, assumption 1 is correct as written: every $x$ in $C$ has the relevant property. Meanwhile, "$\varphi(y)\leftrightarrow\varphi(x)$" means that $y$ has property $\varphi$ iff $x$ does. Basically, assumption 1 is saying that all the properties we care about - on a comeager set, at least! - look "locally constant." The connection with forcing is that open sets (essentially) correspond to forcing conditions, points in $X$ are maximal filters (generic or not!), $C$ is the set of (sufficiently) generic filters, and $\mathscr{P}$ is the set of sentences in the forcing language. $\endgroup$ Aug 26, 2022 at 16:50
  • $\begingroup$ (This is spelled out at the end of my answer.) That is, assumption 1 says: for each sufficiently-generic point (= for each point $x$ in $C$), any property we care about (= any $\varphi\in\mathscr{P}$) that holds of $x$ in fact holds of all sufficiently-generic points near $x$ (= all $y\in C\cap U$ for some open $U\ni x$), and any property we care about that fails of $x$ in fact fails of all sufficiently-generic points near $x$. Similarly, "truth=forcing" says "if $G$ is sufficiently generic and $\varphi$ holds of $G$ then for some $p\in G$ $\varphi$ holds of all sufficiently generic $H\ni p$ $\endgroup$ Aug 26, 2022 at 16:54
  • $\begingroup$ I think I may have finally worked out what your Assumption 1 is doing. So is the following correct (using Kunen) - Definition of $\Vdash$ : $p \Vdash \varphi \; \text{ iff } \; \forall G \; [(G \text{ is } \mathbb{P} \text{-Generic } \land p \in G) \implies (M[G]\models\varphi[G])] \tag{1} $ The Forcing Truth Theorem is (taking $\Vdash^*$ to be the same as $\Vdash$), with G $\mathbb{P}$-Generic : $\endgroup$
    – user239186
    Aug 30, 2022 at 12:44
  • $\begingroup$ $ \forall \varphi \; \forall G \; [(M[G]\models\varphi[G]) \leftrightarrow (\exists p \in G ) \; p \Vdash \varphi)] \tag{2} $ So, inserting (1) into rhs of (2) and taking G to be $\mathbb{P}$-Generic : $ \forall \varphi \; \forall G \; [(M[G]\models\varphi[G]) \leftrightarrow ((\exists p \in G ) \; \forall G' \ni p \; (M[G']\models\varphi[G']))] \tag{3} $ $\endgroup$
    – user239186
    Aug 30, 2022 at 12:44

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$.


Question (i) & (iii) Answer :

See https://cstheory.stackexchange.com/questions/22476/why-is-intuitionistic-negation-nonconstructive

Intuitionism primarily addresses proved truths. This means proved truths continue into the future [$p \Vdash A \implies \forall q \geq p \text{ }q \Vdash A$]. But "not proved truth" goes the other way : if $\neg (p \Vdash A)$ then [$\neg (p \Vdash A) \implies \forall q \leq p \text{ } \neg (q \Vdash A)$], i.e. if it hasn't been proved to be true now, it can't have been proved before.

Also note that the design of forcing is intended to mimic the behaviour of models, via the Taski truth definition :

$$ M \models \neg A \iff \neg [M \models A]$$

and taking the contrapositive

$$ \neg (M \models \neg A) \iff [M \models A] \tag{0}$$

If we have a model M[G] that includes a set G with elements $g_i$, the Tarski truth definition, like Forcing, is based upon assessing the truth of an expression A by assessing all its sub expressions. If we use the compactness theorem, for ease, using Enderton "A Mathematical Introduction to Logic", 2nd Edition, for sentential logic, page 60, Corollary 17A :

If $\Sigma$ is any collection of well formed formulas (it could be, for example { $p_1 \in G$ , $p_2 \in G$ ... }), then the following is equivalent to the Compactness Theorem :

$$\Sigma \models \varphi \text{ } \iff \text{ } \exists \text{ finite } \Sigma_0 \subseteq \Sigma : \Sigma_0 \models \varphi \tag{i} $$

So taking equation (0) and converting it to the compactness form using (i):

$$ \neg (M[G] \models \neg A) \iff [M[G] \models A] \iff [\exists \text{ finite subset of G, } \color{blue}{P} : M[ \color{blue}{P}] \models A] \tag{ii}$$

So the intention of Equation (1a) in the Question is to mimic the form of Equation (ii):

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

Question (iv) Answer :

In fact the following :

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

IS equivalent to

$$\exists k' \geq k : (k' \Vdash ¬A) \iff \forall k'' \geq k \text{ } \neg \text{ } (k'' \Vdash A) \tag{iv}$$

but it just doesn't look like it is. The key point to realise is that the expression $k \Vdash A$ is 'really' a different way of writing its real meaning of "$ \Vdash (k) = A$" i.e. just like a function F of one variable k would be written "F(k) = A", but here with $\Vdash$ being the same as F. Since $k \Vdash$ can produce a set of expressions, then if the range is split into sets of expressions {A,B,C,...}, then $\Vdash$ can still be considered to be a function.

It is very important to recognise that $k \Vdash A$ does NOT mean anything like $k \implies A$. Indeed k itself may not even be directly used. In the most general case, k could just be used as a placeholder in "an expression that uses in some way some other elements k' $\geq$ k - or even k' $\leq$ k. So thinking of "$\Vdash(k) = A$" as a function helps to understand what that general meaning is.

To prove equation (1) $\iff$ equation (iv) :

Note firstly that -

$$[\forall k'' \geq k \text{ } \neg \text{ } (k'' \Vdash A)] \iff [\forall k'' \geq k \text{ } \neg \text{ } (\exists k''' \geq k'' (k''' \Vdash A))] \tag{2}$$

Also note that using (1) and from Question (i) answer that unproved/proved truths propagate backwards/forwards :

$$\exists k' \geq k \text{ } (k' \Vdash ¬A) \iff \forall k′' \geq k' \text{ } \neg (k'' \Vdash A) \iff \forall k'' \geq k \text{ } \neg (k'' \Vdash A) \iff (k \Vdash ¬A) \text{ } \square \text{ } \tag{3} $$

In fact we can write (iv) in the same form as (1), using (2) to rewrite the r.h.s. if we define a new function $\Vdash'$ by :

$$(k \Vdash' A) \iff \exists k' \geq k : (k' \Vdash A) \tag{4}$$

Then (iv) becomes :

$$(k \Vdash' ¬A) \iff \forall k′ \geq k \text{ } \neg \text{ } (k′ \Vdash' A) \tag{5}$$


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" ?

  • $\begingroup$ Thanks Hang Zhang. I am interested to see why (iv) : $$\exists k'' \geq k : (k'' \Vdash ¬A) \Longleftarrow \forall k′ \geq k \; \neg \; (k′ \Vdash A)$$ doesn't work - it looks to create a negation complete generic set. In Cohen's book the proof "Lemma 5 A is true in N iff for some k , k forces A" would go through using (iv). [Also presumably you meant $\models$ instead of $\Vdash$ in your answer.]. $\endgroup$
    – user239186
    Jul 14, 2022 at 17:12
  • $\begingroup$ @ Hang Zhang. Also what about the strange results in (i), (ii), (iii) as well? It seems like forcing has a very large amount of reasoning that isn't based upon the individual content of each element in the generic set., in order to make it negation complete (ie $M[G] \models A$ or $M[G] \models \neg A$). But does it have to be like that to make the generic negation complete and consistent ? (I suspect it does - but due to the properties of infinity and the need for the generic to be a new set). $\endgroup$
    – user239186
    Jul 14, 2022 at 17:19
  • $\begingroup$ @ Hang Zhang - thanks for your interest in the question (and my late reply). It seems like StackExchange does not notify me that you have edited your answer ! I'm giving your answers some thought. $\endgroup$
    – user239186
    Jul 26, 2022 at 13:07
  • $\begingroup$ @ Hang Zhang - Maybe on (i) you could consider the following : Let A be "G has infinitely many elements" and $\neg A$ to be "G has finitely many elements". Is it possible for the finite amount of information in any forcing condition to 'imply' (note I didn't say force) either of these statements? The answer is a definite NO. Indeed any finite forcing condition will not 'imply' an infinite number of formulae one way or another. So any p will not 'imply' an infinite number of B : "not true (p $\implies$ B) AND not true (p $\implies \neg$ B)". $\endgroup$
    – user239186
    Jul 26, 2022 at 13:17
  • $\begingroup$ @ Hang Zhang - Also of course any p will also definitely 'imply' an infinite number of formulae C, or negated formulae $\neg$ D , using ONLY the finite information in p : {C : p $\implies$ C} and {$\neg$ D : p $\implies \neg$ D}. Given, as you correctly say, the objective is to achieve a negation complete representation of the formulae true in M[G] in the base model M, the question is how to balance out what a condition p can and can't imply, by imposing a forced negation completeness definition in a way that doesn't create chaos and an inconsistent set of forced formulae. $\endgroup$
    – user239186
    Jul 26, 2022 at 13:45

This site is temporarily in read-only mode and not accepting new answers.