1
$\begingroup$

I have trouble understanding why $$\Diamond P \to \square\Diamond P$$ is valid in Euclidean frames.

I found a proof online which is detailed as follows:

Proof. Suppose $F$ is a Euclidean frame, and $M$ a model based on $F.$ Suppose $\models_w \Diamond A$. Then there is a $v$ such that $w\mathrel{R}v$ and $\models_v A.$ Now, for any $u$ with $w\mathrel{R}u$, we have $u\mathrel{R}v$ since $R$ is Euclidean. So $\models_u \Diamond$A. Since $u$ is arbitrary, $\models_w \Box\Diamond A,$ and therefore $\models_w \Diamond A \to \Box\Diamond A.$

My question is what if the arbitrary $u$ is chosen as world $v.$ My understanding of necessarily true is that from every world from the current world should satisfy the condition. However, at world $v,$ there is no path to another world where $p$ is true since $p$ is only true at $v$ itself. Doesn't that imply that $\Diamond A$ is false at $v$ and hence $\Box\Diamond A$ is false as well? If that's the case, why is the axiom valid?

Thank you in advance for any explanation!

$\endgroup$
  • $\begingroup$ It's not just any arbitrary $u$, it's an arbitrary $u$ with $wRu$. It's OK if $R$ also happens to be reflexive as well as euclidean. $\endgroup$ – Ryan A Jan 9 '18 at 4:00
  • $\begingroup$ In expressions like $$ \models_w \diamond A \rightarrow \diamond A, $$ you shouldn't keep alternating in and out of MathJax. The whole thing should be between a single pair of dollar signs or double dollar signs. See my edits to the question. $\qquad$ $\endgroup$ – Michael Hardy Jan 9 '18 at 18:45
1
$\begingroup$

Maybe it is worth addressing precisely the question asked: what if the arbitrary $u$ is chosen as world $v$.

One thing to note here is this: Euclideanness implies that the endpoint of any path has a loop. That is, $wRv$ implies $vRv$ (indeed $wRu$ and $wRv$ together imply $uRv$; now take $u=v$).

Thus although there might be no path from $v$ to another world, there is a path from $v$ to itself, $v$ being an endpoint of a path (the one starting in $w$). Thus also $v$ possesses a path to a point where $p$ is true - namely a path to itself.

$\endgroup$
0
$\begingroup$

$u$ is an arbitrary world such that $w R u$, not just any old arbitrary world. If $v$ happens to be one of these worlds, then we know that $w R v$ must hold.

Suppose that $\models_w \Diamond P$. Then we get a world $v$ with $w R v$ and $\models_v P$. We then consider an arbitrary world that can be reached from $w$ (as required by the semantics of $\Box$) and call this $u$. This means that $w R u$, and since the frame was assumed to be Euclidean, $w R u$ and $w R v$ implies that $u R v$, from which we conclude that $\models_u \Diamond P$. Since the $u$ represents any world that can be reached from $w$, we have thus shown that $\models_w \Box \Diamond P$.

$\endgroup$
0
$\begingroup$

My question is what if the arbitrary $u$ is chosen as world $v.$ My understanding of necessarily true is that from every world from the current world should satisfy the condition. However, at world $v,$ there is no path to another world where $p$ is true since $p$ is only true at $v$ itself.

Why do you say that? $v$ need not be the only accessible world which witnesses the truth of $\vDash_w\Diamond A$.

In any case, in an Euclidean frame, by definition, any world $v$ accessible from $w$ is also accessible from any world $u$ that is itself accessible from $w$ . $(wRv~\& ~wRu)\implies uRv$. This inlcudes includes $v$ itself. $(wRv~\& ~wRv)\implies vRv$ . Since $v$ is the witness to $\vDash_w\Diamond A$, it is accessible from $w$, so therefore $vRv$ and hence $\vDash_v \Diamond A$ is okay.

But more, $\vDash_u\Diamond A$ is true for all arbitrary worlds, $u$, accessible from $w$ when $\vDash_w\Diamond A$, since they can each access some world $v$ where $\vDash_v A$ when $\vDash_w \Diamond A$ and the frame is Euclidean.

Hence $\vDash_w\Box\Diamond A$ if $\vDash_w \Diamond A$, and so therefore $\Diamond A\to \Box\Diamond A$ is a theorem in an Euclidean frame

$\endgroup$

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.