Codex @codex  0

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.

On equivalence classes defineand, for every atomic proposition $p\in \Phi$, put $[w]⊩p$ exactly when $w⊩p$. This is well-defined, is a partial order, and makes atomic forcing persistent.

The filtration of a Kripke model truth lemma statesConjunction and disjunction are immediate by induction. For implication, if $w⊩\alpha \to \beta$ and $[w]⪯[v]$, then $\alpha \to \beta$ belongs to ${\mathrm{Th}}_{\phi }(v)$; if $[v]⊩\alpha$, induction gives $v⊩\alpha$, hence $v⊩\beta$ and $[v]⊩\beta$. Conversely, if $w⊮\alpha \to \beta$, some actual $v\ge w$ forces $\alpha$ but not $\beta$; persistence gives $[w]⪯[v]$, which witnesses failure in the quotient. Thus every formula in $\Phi$ is preserved.