Finite model property of intuitionistic propositional logic
= Finite model property of intuitionistic propositional logic
{c}
Every intuitionistically underivable proposition has a finite rooted Kripke countermodel. Filtration and witness pruning bound the model in terms of the number of subformulas.