Translation valid formulas neighbourhood semantics to kripke semantics

40 Views Asked by At

I have been tasked with an exercise which I cannot figure out and thus I require some assistance. The question is as follows:

Let $\mathsf{EM}$ be the set of formulas valid on all neighbourhood frames $\mathcal{F} = (W,N)$ in the unimodal language. That is the language generated by the grammar: $$\varphi ::= \bot\mid p\mid \neg\varphi\mid\varphi\vee\varphi\mid [\ \rangle\varphi$$ Here we have that $$\mathcal{M}, w\Vdash [\ \rangle\varphi \text{ iff forall }U\in N(w) \text{ there exists }v\in U \text{ such that }\mathcal{M}, v\Vdash \varphi$$ Let $\mathsf{K}\oplus\mathsf{K}$ be the set of all formulas valid on all bi-modal frames i.e. a frame $(X, R_1, R_2)$ where $R_1, R_2$ are binary relations. Define a translation $tr$ from the unimodal language (with $\langle\ ]$ and $[\ \rangle$) to the bi-modal language (with $\lozenge_1, \square_1, \lozenge_2, \square_2$) such that $$\varphi\in\mathsf{EM}\text{ iff }tr(\varphi)\in\mathsf{K}\oplus\mathsf{K}$$

Here $\langle\ ]\varphi \leftrightarrow \neg [\ \rangle\neg\varphi$. I got the hint that I should view a neighbourhood frame as a bi-modal frame and vice versa but that's already a step I cannot make. Given such a neighbourhood function $N:W\to\wp(\wp(W))$ we get a relation $R_N\subseteq W\times\wp(W)$ defined as $wR_N U$ iff $U\in N(w)$ but I cannot proceed further. Thus my question is if someone can give me a push in the right direction in finding a translation of $\langle\ ]\varphi$ (or $[\ \rangle\varphi)$. I thank you in advance.