In the intuitionistic version of the modal logic K (IK), the following is a theorem: $(\Diamond p \to \Box q) \to \Box( p \to q)$. However, given the definitions for $\Box$ and $\Diamond$, I think I have a counterexample.
$w \Vdash \Box A$ iff for all $v$ s.t. $w \le v$ and all $u$ s.t. $vRu$, $u \Vdash A$
$w \Vdash \Diamond A$ iff there is a $v$ s.t. $wRv$ and $v \Vdash A$
Take three states $w$, $v$ and $u$ such that $s \le s$ for all states, $v \le u$, and $wRv$. Further, let $w \not \Vdash p$ and $v \not \Vdash p$. Next, let $u \not \Vdash q$ and $u \Vdash p$. So, for every state $s$ where $w \le s$, if $w \Vdash \Diamond p$, then $s \Vdash \Box q$. So, $w \Vdash \Diamond p \to \Box q$. But, $v \not \Vdash p \to q$ since $v \le u$ and $u \not \Vdash p \to q$. So, $w \not \Vdash \Box (p \to q)$.
What mistake am I making here? Though $p$ is satisfied at $u$, we don’t have $wRu$, so clearly $w$ cannot satisfy $\Diamond p$. Am I misinterpreting the semantics somehow?
In retrospect, I missed a crucial part of the semantics for intuitionistic modal logic. There is a bisimulation between the accessibility relations $\le$ and $R$. That is, the following hold:
if $wRv$ and $w \le u$, then there is an $x$ such that $v \le x$ and $uRx$
and
if $wRv$ and $v \le u$, then there is an $x$ such that $w \le x$ and $xRu$.
These conditions validate the formula in question.