How do I read double connectives in modal logic?

Question

My book says:

$\neg \Box p \rightarrow \Box \neg \Box p$ is not a valid formula and proves it by saying that in Figure 5.3, if we change $L(x_4)$ to $\{p, q\}$, then $\neg \Box p$ is true but $\Box \neg \Box p$ is not.

I get that $\neg \Box p$ is true: It is not the case that all worlds accessible from $x_4$ are labeled $p$.

Now why is $\Box \neg \Box p$ not true? What does $\Box \neg \Box p$ really mean? Could you please provide more examples of multiple connectives with relation to a diagram (the one provided if you want), so I can get a better understanding?

@MauroALLEGRANZA - Please reread the question: It came out wrong, the boxes were not rendered. — mdemont, Apr 25 '17 at 10:43
It is easier to format them with $... \square for "necessary" and \diamond for "possible". — Mauro ALLEGRANZA, Apr 25 '17 at 10:45
Thus, $\lnot \square p$ means that $\square p$ is false at $w$, i.e. there is a world z such that $wRz$ and $z \nvDash p$. — Mauro ALLEGRANZA, Apr 25 '17 at 10:50
$\lnot \square p$ means "it is not necessary that.." and thus the formal semantics is consistent with our intuition: if $p$ is not necessary, there is some "situation" where $p$ does not hold. — Mauro ALLEGRANZA, Apr 25 '17 at 10:53
I understand what ¬□p means and what □p means. I don't understand when there are multiple □'s. — mdemont, Apr 25 '17 at 10:53

score 2 · Answer 1 · answered May 05 '17 at 11:51

You should think of $\Box$ and $\Diamond$ as saying something about the next "step" or transition in the Kripke model. $\Box \varphi$ says that in the next step, $\varphi$ will hold, regardless of which transition we pick. $\Diamond \varphi$ says that there is a transition in which $\varphi$ will hold, i.e. we can choose our next step such that $\varphi$ will hold.

Multiple connectives will therefore tell you something about multiple steps. For example, $\Diamond \Box \Diamond \varphi$ says that there exists a transition such that we end up in a world $w$, and for any transition we take from $w$, we will end up in a world where we can take some transition to where $\varphi$ holds. Hence, we know something about what happens three steps ahead.

For your specific example, let us relabel $x_4$ with $\{p,q\}$, as you say. The formula $\Box \neg \Box p$ says that any transition we take will take us to a world in which we can not reach a world that is labelled with $p$. However, this is clearly false for $x_4$: The only transition we can take is to $x_5$, and all the worlds reachable by $x_5$ (these are $x_4$ and $x_6$) are labelled with $p$.

How do I read double connectives in modal logic?

1 Answers1