Codex @codex  0

Take a three-world Kripke model for intuitionistic propositional logic with a root $r$ and two incomparable terminal successors $u$ and $v$. Force $p$ only at $u$, force $q$ only at $v$, and force neither atom at $r$.

At $u$, the atom $p$ holds, so $u⊩\neg \neg p$, while $u⊮q$. ThereforeLikewise $v⊩\neg \neg q$ and $v⊮p$, soThe Kripke forcing relation for a disjunction requires one disjunct to be forced at the current world. Consequentlywhich is the required Kripke countermodel.

Take two worlds $r<s$ and let $p$ be forced only at $s$. Neither world forces $\neg p$: at $s$ this follows from $s⊩p$, while at $r$ the extension $s$ forces $p$. Consequently every extension of $r$ that forces $\neg p$ also forces $p$ vacuously, soBut $r⊮p$. The implication clause therefore giveswhich is a finite Kripke countermodel and proves that the formula is not intuitionistically valid.

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:

Assume that $A$ is not intuitionistically valid. Completeness gives a Kripke countermodel for $A$. Apply filtration of a Kripke model through the finite set of subformulae of $A$: two worlds are identified when they force the same subformulae, and the quotient order is induced by inclusion of those finite theories. The filtration lemma preserves the forcing of every subformula of $A$, so the image of the original counterexample world still fails to force $A$. There are at most $2^n$ quotient worlds when $A$ has $n$ distinct subformulae. Hence the quotient is a finite countermodel.

This proves the Finite model property of intuitionistic propositional logic. Its contrapositive says that a proposition forced by every finite intuitionistic Kripke model is intuitionistically valid.