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

Silvia Ghilezan
Faculty of Engineering, University of Novi Sad, Novi Sad, Serbia

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

PDF