Abstract
Zucker showed that in the fragment of intuitionistic logic whose formulae are build up from \(\wedge \), \(\supset \) and \(\forall \) only, every reduction sequence in natural deduction corresponds to a reduction sequence in the sequent calculus and vice versa. Unfortunately, the technical machinery in Zucker’s work is rather cumbersome and complicated. One contribution of this chapter is to greatly simplify his arguments. For example he defined a cut-elimination procedure modulo an equivalence relation; our cut-elimination procedure will be a simple term-rewriting system instead. Zucker also showed that the correspondence breaks down when the connectives \(\vee \) or \(\exists \) are included. We shall show that this negative result is not because cut-elimination fails to be strongly normalising for these connectives, as asserted by Zucker, rather it is because certain cut-elimination reductions do not correspond to any normalisation reduction.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Altenkirch, T., Dybjer, P., Hofmann, M., & Scott, P. (2001). Normalization by Evaluation for typed lambda calculus with coproducts. Proceedings of Logic in Computer Science (pp. 203–210).
Barbanera, F. & Berardi, S. (1994). A symmetric lambda calculus for “classical” program extraction. Theoretical Aspects of Computer Software, volume 789 of LNCS (pp. 495–515). Springer.
Barendregt, H., & Ghilezan, S. (2000). Theoretical pearls: Lambda terms for natural deduction, sequent calculus and cut elimination. Journal of Functional Programming, 10(1), 121–134.
Bloo, R. (1997). Preservation of termination for explicit substitution. Ph.D. thesis. Eindhoven University of Technology.
Espírito Santo, J. C. (2000). Revisiting the correspondence between cut elimination and normalisation. Proceedings of ICALP 2000, volume 1853 of LNCS (pp. 600–611). Springer.
Gallier, J. (1993). Constructive logics. Part I: A tutorial on proof systems and typed \(\lambda \)-calculi. Theoretical Computer Science, 110(2), 239–249.
Gentzen, G. (1935). Untersuchungen über das logische Schließen I and II. Mathematische Zeitschrift, 39(176–210), 405–431.
Girard, J.-Y., Lafont, Y., & Taylor, P. (1989). Proofs and types, volume 7 of cambridge tracts in theoretical computer science. Cambridge: Cambridge University Press.
Herbelin, H. (1994). A \(\lambda \)-calculus structure isomorphic to sequent calculus structure. Computer Science Logic, volume 933 of LNCS (pp. 67–75). Springer.
Kreisel, G. (1971). A survey of proof theory II. Proceedings of the 2nd Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics pp. 109–170. North-Holland.
Laird, J. (2001). A deconstruction of non-deterministic cut elimination. Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications, Volume 2044 of LNCS pp. 268–282. Springer.
Negri, S., & von Plato, J. (2001). Structural proof theory. Cambridge: Cambridge University Press.
Pottinger, G. (1977). Normalisation as homomorphic image of cut-elimination. Annals of Mathematical Logic, 12, 323–357.
Prawitz, D. (1965). Natural deduction: A proof-theoretical study. Stockholm: Almquist and Wiksell.
Troelstra, A. S., & Schwichtenberg, H. (2000). Basic proof theory. Cambridge tracts in theoretical computer science (2\(^{nd}\) ed.). Cambridge: Cambridge University Press.
Ungar, A. M. (1992). Normalisation, cut-elimination and the theory of proofs, volume 28 of CLSI Lecture Notes. Stanford: Center for the Study of Language and Information.
Urban, C. (2000). Classical logic and computation. Ph.D. Thesis. Cambridge University.
Urban, C., & Bierman, G. M. (2001). Strong normalisation of cut-elimination in classical logic. Fundamenta Informaticae, 45(1–2), 123–155.
Zucker, J. (1974). The correspondence between cut-elimination and normalisation. Annals of Mathematical Logic, 7, 1–112.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Urban, C. (2014). Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation. In: Pereira, L., Haeusler, E., de Paiva, V. (eds) Advances in Natural Deduction. Trends in Logic, vol 39. Springer, Dordrecht. https://doi.org/10.1007/978-94-007-7548-0_2
Download citation
DOI: https://doi.org/10.1007/978-94-007-7548-0_2
Published:
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-007-7547-3
Online ISBN: 978-94-007-7548-0
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)