In Kripke models the evaluation of $x \vdash \Box p$ would be that every world reachable from $x$ satisfies $p$.

But how would the truth of $\Box\Box p$ be evaluated in Kripke models?


This is an unfortunate use of the word “reachable”, in that Kripke structures are graphs but “reachable” in a Kripke structure is not the same thing as “reachable” in a graph. Let us avoid this confusion by saying that a state $y$ is a successor of state $x$ if there is a (directed) edge $(x,y)$ in the structure.

Now, the semantics of modal logic says that $\Box\varphi$ is true at state $x$ if, and only if, $\varphi$ is true at every successor of $x$. Informally, $\Box\varphi$ means, “$\varphi$ is true everywhere I can get to from here in one step.” So, to understand the meaning of $\Box\Box p$, just substitute $\Box p$ for $\varphi$:

  • $\Box p$ is true at every successor
  • $p$ is true at every successor of every successor.

In other words, $p$ is true everywhere I can get in two steps. Note that this is not, in general, the same thing as $\Box p$, which means that $p$ is true after one step. Indeed, one can show that $(\Box \varphi)\rightarrow (\Box\Box\varphi)$ is a tautology in a particular Kripke frame if, and only if, the successor relation is transitive.

Note that, without assuming transitivity, basic modal logic with only $\Box$ and $\Diamond$ has no way of expressing “$\varphi$ is true everywhere that can be reached from here, in any number of steps” (i.e., the usual graph-theoretic meaning of “reachable”).

| cite | improve this answer | |
  • $\begingroup$ Okay, so would □□□p be saying "anywhere I can get to in 3 steps" and so on? This Stanford article says that in S4, operators of the same kind can be replaced by one occurrence of that operator. But if a specific logic is not specified which interpretation of evaluating □□p is the most intuitive? $\endgroup$ – ethane Sep 6 '16 at 20:32
  • $\begingroup$ @David Richerby - the semantics of $\Box$ is usually "Always", not "Next", which your answer appears to be taking to account. $\endgroup$ – Shaull Sep 6 '16 at 21:20
  • 3
    $\begingroup$ @Shaull Kripke models ≠ temporal logic $\endgroup$ – Gilles 'SO- stop being evil' Sep 6 '16 at 21:32
  • $\begingroup$ @Shaull The semantics of $\Box$ in modal logics is (as far as I'm aware), always exactly as I've stated it. $\endgroup$ – David Richerby Sep 6 '16 at 21:46
  • 1
    $\begingroup$ @Ethan S4 is precisely basic modal logic plus the requirement that the edge relation of the Kripke frame is reflexive and transitive. And it's that transitivity that means that $(\Box\cdots\Box \varphi)\leftrightarrow(\Box\varphi)$ holds (and similarly with diamonds). $\endgroup$ – David Richerby Sep 6 '16 at 21:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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