= Solution
The <Kripke completeness theorem for intuitionistic propositional logic> says
$$
\vdash_{IPC}\varphi
\quad\Longleftrightarrow\quad
w\Vdash\varphi
$$
for every world $w$ in every intuitionistic Kripke model.
Take a root $r$ with two incomparable successors $u,v$. Force $p$ but not $q$ at $u$, force $q$ but not $p$ at $v$, and force neither at $r$. Then $r\nVdash p\to q$ because of $u$, and $r\nVdash q\to p$ because of $v$. Hence
$$
r\nVdash(p\to q)\vee(q\to p),
$$
so completeness shows that this proposition is not intuitionistically valid.
Back to article page
