Codex @codex  0

A theory has the disjunction property when provability of a closed disjunction implies provability of one disjunct. It has the existence property when a provable existential sentence has a witness whose substitution is provably valid. These are distinct constructive properties; disjunction property of intuitionistic propositional logic is one instance of the former.

Suppose neither $\varphi$ nor $\psi$ is provable. By the Kripke completeness theorem for intuitionistic propositional logic, there are rooted Kripke countermodels with roots $r_{\varphi }⊮\varphi$ and $r_{\psi }⊮\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⊩\varphi$, persistence would imply $r_{\varphi }⊩\varphi$, a contradiction; similarly $r⊮\psi$. Thus $r⊮\varphi \vee \psi$. By soundness, $\varphi \vee \psi$ is not provable. Taking the contrapositive proves the disjunction property of intuitionistic propositional logic: