0
$\begingroup$

I got an exercise from my teacher to translate formulas of modal logic with modal operator $\nabla$ into formulas with operators $\Box$ and $\Diamond$.

If the set of possible worlds is $X$, the accessibility relation is $R$ and the semantics of $\nabla$ are as follows:

$x \models \nabla\{\phi_1,...,\phi_n \}$ iff $(\forall y \in X:xRy \to (\exists\phi_k: y \models \phi_k)) \wedge (\forall \phi_k\exists y\in X:xRy \wedge y \models \phi_k)$,

what is the corresponding formula with the same meaning without the $\nabla$ operator?

I think that the result is $\nabla\{\phi_1,\dots,\phi_n\} = \Box(\phi_1\lor\dots\lor\phi_n)\wedge(\Diamond\phi_1\wedge\dots\Diamond\wedge\phi_n)$

Is that correct? Thank you.

$\endgroup$
  • $\begingroup$ Looks okay to me. $\endgroup$ – Henning Makholm Oct 17 '11 at 0:47
1
$\begingroup$

I haven't done modal logic in a while, but I believe your translation is correct. The definition you were provided states that

$$ x \vDash \nabla \Phi \equiv (\forall y \in W . R(x,y) \Rightarrow \exists \phi \in \Phi . y \vDash \phi) \wedge (\forall \phi \in \Phi . \exists y \in W . R(x,y) \wedge y \vDash \phi)$$

To see that your translation is correct, consider the following equivalence:

$$ x \vDash \bigwedge \{ \Diamond \phi : \phi \in \Phi \}\equiv \forall \phi \in \Phi. \exists y \in W. R(x,y) \wedge y \vDash \phi $$

This gives you the second conjunct of the definition of the nabla operator. Now you merely need to secure the first conjunct. Again, consider the equivalence $$ x \vDash \Box \left ( \bigvee \Phi \right ) \equiv \forall y \in W. R(x,y) \Rightarrow y \vDash \bigvee \Phi$$

In order for the consequent of the implication of the right-hand side of the bi-implication to be true, we must have $y \vDash \phi$ for some $\phi \in \Phi$ and all $y \in W$ such that $R(x,y)$. This gives the first conjunct of the definition of the nabla operator. Hence,

$$ x \vDash \nabla \Phi \equiv x \vDash \Box \left ( \bigvee \Phi \right ) \wedge \bigwedge \{ \Diamond \phi : \phi \in \Phi\}$$

Unless I'm missing something, the proof should follow straightforwardly from expanding the definitions on the right-hand side of your translation.

$\endgroup$
  • $\begingroup$ Thank you very much for your answer. If I understand it right, shouldn't there be "we must have y⊨ϕ for some ϕ∈\Phi" instead of "y∈\Phi"? $\endgroup$ – Matej Oct 17 '11 at 11:13
  • $\begingroup$ Yeah, thanks for catching that. $\endgroup$ – danportin Oct 17 '11 at 22:40

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.