A simply-typed lambda-calculus is presented whose normal forms exactly
represent the cut-free derivations of the contraction-free sequent
calculus, invented independently by Vorobev, Hudelmaier,
Lincoln/Shankar and Dyckhoff. Its crucial property is termination of
proof search without need for loop-detection.
The proposed lambda-calculus LambdaJT follows the paradigm of
generalized eliminations put forward by von Plato and consequently
also has permutative conversions. It will be shown that strong
normalization of the beta-reductions and permutative conversions
nevertheless can be established elegantly - even yielding an embedding
of the system with beta-reductions only into Girard's polymorphic
lambda-calculus. The full system, however, also has specific rules for
the elimination of contractions. A normalization algorithm can be
given by extending the method of proving admissibility of contraction
in the recent JSL paper by Dyckhoff and Negri. The termination of this
algorithm is still an open question due to the rule of
contraction-elimination for nested implications.
For the intended applications, LambdaJT has to be extended by rules of
immediate simplification which can only reasonably be expressed in the
term calculus as opposed to the original sequent calculus. This gives
rise to a smaller set of normal forms with good behaviour with respect
to interpolation: We show in a case study that for any proof of
monotonicity of lambda P.(((P->Q)->P)->P)->P (with P, Q different
propositional variables) in our calculus, we arrive at the
positivization lambda P.(P->Q)->P, while there are at least three ways
of blowing up this interpolant by suitable monotonicity proofs in
usual lambda-calculus, even yielding formulas of arbitrary level.
The hope will be expressed that this observation will carry over to a
new proof of Pitts' result (JSL 1992) on uniform interpolation.