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?


1 Answer 1


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”).

  • $\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
    Commented Sep 6, 2016 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
    Commented Sep 6, 2016 at 21:20
  • 3
    $\begingroup$ @Shaull Kripke models ≠ temporal logic $\endgroup$ Commented Sep 6, 2016 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$ Commented Sep 6, 2016 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$ Commented Sep 6, 2016 at 21:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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