= Solution
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.
Back to article page
