= Solution
Suppose neither $\phi$ nor $\psi$ is provable. By the <Kripke completeness theorem for intuitionistic propositional logic>, there are rooted <Kripke countermodel>[Kripke countermodels] with roots $r_\phi\nVdash\phi$ and $r_\psi\nVdash\psi$. Take their disjoint union and place a fresh world $r$ below every world in both components, forcing no propositional variables at $r$ beyond those required by persistence.
If $r\Vdash\phi$, persistence would imply $r_\phi\Vdash\phi$, a contradiction; similarly $r\nVdash\psi$. Thus $r\nVdash\phi\vee\psi$. By soundness, $\phi\vee\psi$ is not provable. Taking the contrapositive proves the <disjunction property of intuitionistic propositional logic>:
$$
\vdash_{\mathrm{IPC}}\phi\vee\psi
\quad\Longrightarrow\quad
\vdash_{\mathrm{IPC}}\phi\ \text{or}\ \vdash_{\mathrm{IPC}}\psi.
$$
Back to article page
