|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||URL:||http://www.cs.ru.nl/barendregt60/essays/ghilezan/art09_ghilezan.pdf||Abstract:||
This paper revisits the results of Barendregt and Ghilezan  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
checked on Mar 21, 2023
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.