Interpolation in a fragment of intuitionistic propositional logic
Gerard R. Renardel de Lavalette · Logic Group preprint series · 1986
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.