G. Mints
Deptartment of Philosophy
Stanford University
Stanford
Ca 94305, USA
mints@csli.stanford.edu
Craig 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 more complicated version for the predicate case.