 Finite model property of intuitionistic propositional logic

Every intuitionistically underivable proposition has a finite rooted Kripke countermodel. Filtration and witness pruning bound the model in terms of the number of subformulas.