Terms for Natural Deduction, Sequent Calculus and Cut Elimination in Classical Logic.

Abstract

This paper revisits the results of Barendregt and Ghilezan [3] and generalizes them for classical logic. Instead ofλ-calculus, we use hereλμ-calculus as the basic term cal-culus. We consider two extensionally equivalent type assignment systems forλμ-calculus,one corresponding to classical natural deduction, and the other to classical sequent calculus. Their relations and normalisation properties are investigated. As a consequence a short proof of Cut elimination theorem is obtained.