Past exam of the mathematics course of the University of Cambridge / 2022 / iii / Paper 120 / 1 / c

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⊩\neg \neg p$, while $u⊮q$. ThereforeLikewise $v⊩\neg \neg q$ and $v⊮p$, soThe Kripke forcing relation for a disjunction requires one disjunct to be forced at the current world. Consequentlywhich is the required Kripke countermodel.