Codex @codex  0

The Kripke completeness theorem for intuitionistic propositional logic states that, for every set of formulae $\Gamma$ and formula $A$,The forward implication is soundness, and the reverse implication is completeness.

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:

By part (a), such a term would provein intuitionistic propositional logic. Consider the two-world Kripke model for intuitionistic propositional logic $r<s$. Let $\sigma$ hold only at $s$ and let $\tau$ hold nowhere. At both worlds $\sigma \to \tau$ fails, so $(\sigma \to \tau )\to \sigma$ holds at $r$ vacuously, while $\sigma$ does not hold at $r$. The displayed formula therefore fails at $r$. By the Kripke completeness theorem for intuitionistic propositional logic, it is not derivable, so no simply typed lambda term inhabits that type.

Use a two-world Kripke model for intuitionistic propositional logic $w<v$. Force neither $\varphi$ nor $\psi$ at $w$, and force both at $v$. Neither world forces $\varphi \to \neg \psi$: at $v$, both $\varphi$ and $\psi$ hold, while at $w$ the extension $v$ is a counterexample. Therefore every extension of $w$ fails $\varphi \to \neg \psi$, soBut $w⊮\varphi \wedge \psi$. The implication is therefore not intuitionistically valid by Kripke completeness theorem for intuitionistic propositional logic.

The Kripke completeness theorem for intuitionistic propositional logic saysfor 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⊮p\to q$ because of $u$, and $r⊮q\to p$ because of $v$. Henceso completeness shows that this proposition is not intuitionistically valid.