Grigori Mints Interpolation theorems for intuitionistic predicate logic Craig's interpolation theorem (which holds for intuitionistic logic) implies that the derivability of X,X'->Y' implies existence of an interpolant I in the common language of X and X'->Y' such that both X->I and I,X'->Y' are derivable. For classical logic this extends to X,X'->Y,Y', but for intuitionistic logic there are counterexamples. There is a version true for intuitionistic propositional (but not for predicate) logic, and a more complicated version for the predicate case.