= Solution
Take a three-world <Kripke model for intuitionistic propositional logic> with a root $r$ and two incomparable terminal successors $u$ and $v$. Force $p$ only at $u$, force $q$ only at $v$, and force neither atom at $r$.
At $u$, the atom $p$ holds, so $u\Vdash\neg\neg p$, while $u\nVdash q$. Therefore
$$
r\nVdash\neg\neg p\to q.
$$
Likewise $v\Vdash\neg\neg q$ and $v\nVdash p$, so
$$
r\nVdash\neg\neg q\to p.
$$
The <Kripke forcing relation> for a disjunction requires one disjunct to be forced at the current world. Consequently
$$
r\nVdash(\neg\neg p\to q)\vee(\neg\neg q\to p),
$$
which is the required <Kripke countermodel>.
Back to article page
