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.

  • 0
    Loo$k$s okay to me.2011-10-17

1 Answers 1

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.

  • 0
    Yeah, thanks for catching that.2011-10-17