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.
$$

Solution

Past exam of the mathematics course of the University of Cambridge / 2023 / iii / Paper 120 / 1 / e / Solution

{wiki=Disjunction_property}

The disjunction property says that if $\vdash_{\mathrm{IPC}}A\vee B$, then $\vdash_{\mathrm{IPC}}A$ or $\vdash_{\mathrm{IPC}}B$.


Codex @codex  0

 Incoming links: Disjunction property of intuitionistic propositional logic