# Show that, at each possible world $\Gamma$ of a modal model, $\Gamma \Vdash \square X \equiv \sim \diamondsuit \sim X$

Show that, at each possible world $\Gamma$ of a modal model, $\Gamma \Vdash \square X \equiv \sim \diamondsuit \sim X$.

I'm not exactly sure how to proceed here.

I know that a modal model $\mathcal{M}=(\mathcal{g},\mathcal{R},\Vdash)$, is composed of the nonempty set of possible worlds, $\mathcal{g}$; a binary accessibility relation, $\mathcal{R}$; and $\Vdash$, a relation between possible worlds and propositional letters.

However, I'm not exactly sure how to start the proof, or what method would work best. It looks like aiming for a contradiction would be best, since $\square X = \sim \diamondsuit \sim X$ (?).

• Re your last paragraph: surely you can't assume that $\square X$ is defined as $\neg \diamondsuit \neg X$, or there's simply nothing to prove. I imagine the point is to show their equivalence using the definition $$\text{for w a world, w \Vdash \square X \\} \text{ \bf{iff} \\ } \text{for all worlds w' accessible from w (i.e. w R w'), w' \Vdash X}$$ Or something like that. In any case, prove that this basic duality holds in any world. – BrianO Dec 30 '15 at 23:45
• I'm confused by the question, actually, as I don't know what is defined in terms of what. Is either of $\square, \diamondsuit$ defined in terms of the other, syntactically? Anyway, I expect that once you expand some definitions, the problem reduces to using the classical-logic equivalences $\forall = \neg \exists\neg$ and its dual, as well as $\neg\neg\phi \equiv \phi$ for any formula $\phi$. Proof by contradiction seems unnecessary. – BrianO Dec 31 '15 at 0:01
• @BrianO, Thanks for the comments. It doesn't look like these are defined in terms of the other, as the book (Fitting & Mendelsohn's $\textit{First-Order Modal Logic}$). The book states: "What is a dded to this syntax of classical logic are two new unary operators $\square$ (necessarily) and $\diamondsuit$ (possibly)". I'll try to recall how to prove the $\forall = \sim \exists \sim$. – user225477 Dec 31 '15 at 0:06
• Ah ok so they're both primitive. Then both semantic definitions of have to be given to, yes? That is, both $w\Vdash \diamondsuit p$ and $w\Vdash \square p$ have to be defined, somehow. What are those definitions? – BrianO Dec 31 '15 at 0:49
• @BrianO, $\Gamma \Vdash \square X \Longleftrightarrow$ for every $\Delta \in \mathcal{g}$, if $\Gamma \mathcal{R}\Delta$, then $\Delta \Vdash X$.\\ And, $\Gamma \Vdash \square X \Longleftrightarrow$ for some $\Delta \in \mathcal{g}$, $\Gamma \mathcal{R}\Delta$ and $\Delta \Vdash X$. – user225477 Dec 31 '15 at 0:54

Given the definitions \begin{align} w \Vdash \diamondsuit X &:= \exists w'\,(w R w' \land w'\Vdash X), \\ w \Vdash \square X &:= \forall w'\,(w R w' \to w'\Vdash X) \\ \end{align} for any world $w$. In the metatheory, we can use equivalences of classical logic:
• $\neg(p\to q) \equiv(p \land \neg q)$,
• $\forall = \neg\exists\neg$ and $\exists = \neg\forall\neg$.
Putting these together, \begin{align} w \Vdash \square X &:= \forall w'\,(w R w' \to w'\Vdash X) \\ &\equiv \neg\exists w'\neg\,(w R w' \to w'\Vdash X) \\ &\equiv \neg\exists w'\,(w R w' \land \neg (w'\Vdash X)) \\ &\equiv \neg\exists w'\,(w R w' \land w'\Vdash \neg X) \\ &\equiv \neg w\Vdash\diamondsuit \neg X\\ &\equiv w\Vdash\neg\diamondsuit \neg X.\\ \end{align}
So the duality law $\square = \neg\diamondsuit\neg$ holds in any world $w$. Similarly, or using $\neg\neg X \equiv X$, its dual $\diamondsuit = \neg\square\neg$ holds in any world.