Authors: Ghilezan, Silvia 
Title: Terms for Natural Deduction, Sequent Calculus and Cut Elimination in Classical Logic.
Journal: Reflections on Type Theory, Lambda Calculus and the Mind, Essays dedicated to Henk Barendregt
Issue Date: 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 calculus. Their relations and normalisation properties are investigated. As a consequence a short proof of Cut elimination theorem is obtained.
Keywords: classical logic | natural deduction | sequent calculus | normalisation | cut elimination
Publisher: Radboud University, The Netherlands

Show full item record

Page view(s)

checked on May 9, 2024

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.