A refinement of interpolation for natural deduction

Ralph Matthes, LMU Munich


Abstract for the Dagstuhl Seminar on Proof Theory in Computer Science,
October 7-12, 2001


Interpolation is THE tool for reducing provable monotonicity to
syntactic positivity. With the ultimate goal of finding a predicative
simulation of the behavior of monotone inductive types by that of
positive inductive types, one cannot restrict the attention to
inhabitation (= provability via the Curry-Howard-isomorphism). One
also has to be aware of proof terms. This addition of coherence
information already appears in Cubric (Archive for Mathematical Logic,
1994). We reprove the result for a variant LambdaJ of lambda-calculus
which allows to define the interpolants by a single recursion on the
build-up of normal terms of LambdaJ: It has a generalized application
r^{rho->sigma}(s^rho,z^sigma.t^tau):tau which may be seen as the
closure of the left implication rule of Gentzen under substitution. 
Normalization of LambdaJ requires permutative conversions. The
interpolation result a la Cubric even requires some extended
permutations with unknown reduction properties. Nevertheless, one gets
the result on lambda-calculus as a corollary.

Towards the intended application, the positivization of monotone type
dependencies is presented.
Some remarks on uniform interpolation and its consequences for
positivization indicate future work.