# Kripke Models - evaluating the meaning of $\Box\Box p$

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

• 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? Sep 6, 2016 at 20:32
• @David Richerby - the semantics of $\Box$ is usually "Always", not "Next", which your answer appears to be taking to account. Sep 6, 2016 at 21:20
• @Shaull Kripke models ≠ temporal logic Sep 6, 2016 at 21:32
• @Shaull The semantics of $\Box$ in modal logics is (as far as I'm aware), always exactly as I've stated it. Sep 6, 2016 at 21:46
• @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). Sep 6, 2016 at 21:49