TERMS FOR NATURAL DEDUCTION, SEQUENT CALCULUS AND CUT ELIMINATION IN CLASSICAL LOGIC
Silvia Ghilezan · 2007
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 cal- culus. Their relations and normalisation properties are investigated. As a consequence a short proof of Cut elimination theorem is obtained.