Cheap and Secure Web Hosting Provider : See Now

[Answers] Kripke Models - evaluating the meaning of $\Box\Box p$

, , No Comments
Problem Detail: 

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?

Asked By : Ethan

Answered By : David Richerby

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

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/63199

3.2K people like this

 Download Related Notes/Documents

0 comments:

Post a Comment

Let us know your responses and feedback