Interpolation in a fragment of intuitionistic propositional logic

Abstract

Let NNIL (No Nestings of Implication to the Left) be the fragment of IpL (intuitionistic propositional logic) in which the antecedent of any implication is always prime. The following strong interpolation theorem is proved: if IpL }-A+B and A or B is in NNIL, then there is an interpolant I in KNIT The proof consists in constructing I from a proof of A+B in a sequent calculus system by means of a variant of a method devised by K. Schutte. This settles a question posed by A. Visser.