Cut Elimination in a Class of Sequent Calculi for Pure Type Systems

AbstractThis paper present a new sequent calculus for Pure Type Systems (PTS). The calculus proposed is equiconsistent to the standard formulation (natural deduction like). The corresponding cut-free fragment makes it possible to introduce a notion of Cut Elimination. This property can be applied to develop proof-search strategies with dependent types.We prove that Cut Elimination holds in two important families of normalizing systems, including, in particular, three systems in the Barendregt's λ-cube: λ →, λ2, and λ ω . In addition, a cut elimination result is obtained for the minimal implicational second-order sequent calculus