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.


1 Answer 1


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.

  • $\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$ Oct 17, 2011 at 11:13
  • $\begingroup$ Yeah, thanks for catching that. $\endgroup$
    – emi
    Oct 17, 2011 at 22:40

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .