Cut-free proofs in Herbelin’s sequent calculus are in 1-1 correspondence with normal natural deduction proofs. For this reason Herbelin’s sequent calculus has been considered a privileged middle-point between L-systems and natural deduction. However, this bijection does not extend to proofs containing cuts and Herbelin observed that his cut- elimination procedure is not isomorphic to β-reduction. In this paper we equip Herbelin’s system with rewrite rules which, at the same time: (1) complete in a sense the cut elimination procedure firstly proposed by Herbelin; and (2) perform the intuitionistic “fragment” of the tq-protocol - a cut-elimination procedure for classical logic defined by Danos, Joinet and Schellinx. Moreover we identify the subcalculus of our system which is isomorphic to natural deduction, the isomorphism being with respect not only to proofs but also to normalisation. Our results show, for the implicational fragment of intuitionistic logic, how to embed natural deduction in the much wider world of sequent calculus and what a particular cut-elimination procedure normalisation is.
CITATION STYLE
Espìrito Santo, J. (2000). Revisiting the correspondence between cut elimination and normalisation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1853, pp. 600–611). Springer Verlag. https://doi.org/10.1007/3-540-45022-x_51
Mendeley helps you to discover research relevant for your work.