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 lambda-calculus, we use here lambda-mu-calculus as the basic term calculus. We consider two extensionally equivalent type assignment systems for lambda-mu-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.

Full text