Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question
    
Looks okay to me. –  Henning Makholm Oct 17 '11 at 0:47

1 Answer 1

up vote 1 down vote accepted

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.

share|improve this answer
    
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"? –  Matej Oct 17 '11 at 11:13
    
Yeah, thanks for catching that. –  danportin Oct 17 '11 at 22:40

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.