A cut-free sequent calculus for pure type systems verifying the structural rules of Gentzen/Kleene

Abstract

In this paper, a new notion for sequent calculus (à la Gentzen) for Pure Type Systems (PTS) is introduced. This new calculus, script K, is equivalent to the standard PTS, and it has a cut-free subsystem, script Kcf, that will be proved to hold non-trivial properties such as the structural rules of Gentzen/Kleene: thinning, contraction, and interchange. An interpretation of completeness of the script Kcf system yields the concept of Cut Elimination, (CE), and it is an essential technique in proof theory; thus we think that it will have a deep impact on PTS and in logical frameworks based on PTS. © Springer-Verlag Berlin Heidelberg 2003.