Every intuitionistically underivable proposition has a finite rooted Kripke countermodel. Filtration and witness pruning bound the model in terms of the number of subformulas.
Articles by others on the same topic
There are currently no matching articles.