3
$\begingroup$

I am asked to prove that every Euclidean models satisfies $\diamond \diamond \diamond \varphi \to \diamond \diamond \varphi$. How can this be done? I don't see how it could even be true.

$\endgroup$

migrated from cstheory.stackexchange.com Oct 1 at 6:26

This question came from our site for theoretical computer scientists and researchers in related fields.

4
$\begingroup$

Suppose $w$ is a world in an Euclidean frame, and $w\mathbin R v$, then by the Euclidean property $w$ reaches both of the "two" worlds $v$ and $v$ (indeed, the same world), and thus $v\mathbin R v$. So in a Euclidean frame, any world that is reachable from some other world, reaches itself (or every world with an incoming arrow has a reflexive arrow).

Now, suppose $w\vDash\Diamond\Diamond\Diamond\phi$, then we know that $w\mathbin R v$ for some world $v$ such that $v\vDash \Diamond\Diamond\phi$. This, in turn, means that $v\mathrel R u$ for some world $u$ such that $u\vDash \Diamond\phi$. By the above argument we see that $v\mathbin R v$, since $v$ is reachable from the world $w$. Thus we have $v\mathrel R v$ and $v\mathrel R u$, which implies that $u\mathrel R v$ by the Euclidean property. Furthermore, we have $u\mathrel R u$ as well, since $u$ is reachable from $v$.

The final step is to see that because $u\vDash \Diamond \phi$, there is some $z$ such that $u\mathrel R z$ and $z\vDash\phi$. By the same reasoning as before, we can find out that not only $u\mathrel R z$, but also $v\mathrel R z$. This gives us that $w\mathrel R v\mathrel R z$, and thus $w\vDash \Diamond\Diamond\phi$.


As a sidenote, the way to see Euclidean frames, is as a bunch of "clusters" of worlds, where a cluster is a group of worlds that are completely connected with each other (i.e. each world in the cluster can reach every other world in the cluster), with (optionally) some "outside" worlds that reach any number (including 0) of the worlds inside one (and only one) cluster, but are not reachable from any other world.

An example in a picture, with the "clusters" in dots connected with red arrows, and the "outside" worlds those dots with blue arrows leaving them:

enter image description here

$\endgroup$
1
$\begingroup$

It's true actually. As a hint, the Euclidean property $$xRy \quad\&\quad xRz \implies yRz$$ does not require the $x,y,z$ to be distinct. So for instance it implies $$xRy \quad\&\quad xRy \implies yRy.$$

Try to construct a counterexample model with 4 worlds $w,x,y,z$ where $\phi$ holds only in $z$ and where $wRx, xRy, yRz$.

$\endgroup$
  • $\begingroup$ I used this kind of "trick" to solve all the other question of this kind, but I don't see how this could help with this. It makes sense to me when proving $\diamond \diamond \varphi \to \diamond \diamond \diamond \varphi$, but not the other way round. $\endgroup$ – Logos Oct 1 at 6:14

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.