Suppose our language has two diamond operators $\Diamond$ and $\overline{\Diamond}$ and, over a Kripke model whose relation is $R$, we have the following semantics:
- $w\models\Diamond\varphi$ if there exists $v$ such that $(w,v)\in R$ and $v\models\varphi$.
- $w\models\overline{\Diamond}\varphi$ if there exists $v$ such that $(w,v)\notin R$ and $v\models\varphi$.
I want to know if there are works dealing with these interpretations (for instance, one could ask for a complete system).
