Abstract
We present a proof (of the main parts of which there is a formal version, checked with the Isabelle proof assistant) that, for a G3-style calculus covering all of intuitionistic zero-order logic, with an associated term calculus, and with a particular strongly normalising and confluent system of cut-reduction rules, every reduction step has, as its natural deduction translation, a sequence of zero or more reduction steps (detour reductions, permutation reductions or simplifications). This complements and (we believe) clarifies earlier work by (e.g.) Zucker and Pottinger on a question raised in 1971 by Kreisel.
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
Baader, F., & Nipkow, T. (1998). Term rewriting and all that. Cambridge: Cambridge University Press.
Barendregt, H. (1984). The lambda calculus. Amsterdam: Elsevier Science. revised ed.
Borisavljević, M. (2004). Extended natural-deduction images of conversions from the system of sequents. Journal of Logic & Computation, 14, 769–799.
Dyckhoff, R., & Urban, C. (2003). Strong normalization of Herbelin’s explicit substitution calculus with substitution propagation. Journal of Logic & Computation, 13, 689–706.
Dyckhoff, R., & Chapman, P. (2009). Isabelle proof script, available from its first author.
Dyckhoff, R. (2011). Cut-elimination, substitution and normalisation, Section A3. Logic and Computation, 14th Congress of Logic, Methodology and Philosophy of Science, Nancy.
Dyckhoff, R. (2013). LPO checker in Prolog, available from the author.
Gentzen, G. (1935). Untersuchungen uber das logische Schließen. Mathematische Zeitschrift, 39, 176–210 and 405–431.
Joachimski, F., & Matthes, R. (2003). Short proofs of normalization for the simply-typed lambda-calculus, permutative conversions and Gödel’s T. Archive for Mathematical Logic, 42, 59–87.
Kikuchi, K. (2006). On a local-step cut-elimination procedure for the intuitionistic sequent calculus. In Proceedings of the 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR’06), 4246 of LNCS (pp. 120–134). Springer.
Kreisel, G. (1971). A survey of proof theory II, In J. E. Fenstad (Ed.), Proceedings of the 2nd Scandinavian Logic Symposium, North-Holland (pp. 109–170).
Mayr, R., & Nipkow, T. (1998). Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192, 3–29.
Negri, S., & von Plato, J. (2001). Structural proof theory. Cambridge: Cambridge University Press.
Pottinger, G. (1977). Normalisation as a homomorphic image of cut-elimination. Annals of Mathematical Logic 12, 323–357. New York: North-Holland.
Prawitz, D. (1965). Natural deduction: A proof-theoretical study. Stockholm: Almqvist & Wiksell.
Prawitz, D. (1971). Ideas and results in proof theory. In J. E. Fenstad (Ed.), Proceedings of the 2nd Scandinavian Logic Symposium, North-Holland (pp. 235–307).
Schwichtenberg, H., & Wainer, S. (2012). Proofs and computations, Perspectives in Logic Series, Association for Symbolic Logic. Cambridge: Cambridge University Press.
Troelstra, A., & van Dalen, D. (2000). Constructivism in mathematics: An introduction, Vol II (Vol. 123)., Studies in logic and the foundations of mathematics Amsterdam: North-Holland.
Troelstra, A., & Schwichtenberg, H. (2000). Basic proof theory (2nd ed.). Cambridge: Cambridge University Press.
Urban, C. (2014). Revisiting Zucker’s work on the correspondence between cut-elimination and normalisation. In L. C. Pereira, E. H. Haeusler, & V. de Paiva (Eds.), Advances in natural deduction. A celebration of Dag Prawitz’s work (pp. 31–50). Dordrecht: Springer.
Urban, C., & Bierman, G. (2001). Strong normalisation of cut-elimination in classical logic. Fundamenta Informaticae, 45, 123–155.
Urban, C. (2008). Nominal techniques in Isabelle/HOL. Journal of Automated Reasoning, 40, 327–356.
Vestergaard, R. (1999). Revisiting Kreisel: A computational anomaly in the Troelstra-Schwichtenberg G3i system, Unpublished.
von Plato, J. (2001). Natural deduction with general elimination rules. Archive for Mathematical Logic, 40, 541–567.
von Raamsdonk, F. & Severi, P. (1995). On normalisation, Centrum voor Wiskunde en Informatica, Amsterdam, CS-R9545.
Zucker, J. (1974). The correspondence between cut-elimination and normalisation. Annals of Mathematical Logic, 7, 1–112.
Acknowledgments
Thanks are due to Jan von Plato, Peter Chapman, Jacob Howe, Stéphane Graham-Lengrand and Christian Urban for helpful comments and (to the last of these) for a copy of (Urban 2014) prior to its publication, albeit many years after its 2001 presentation in Rio. Chapman’s work (Dyckhoff and Chapman 2009) (incorporating also ideas by Urban) was invaluable in checking the correctness of all the lemmata about substitution. The work was motivated by requirements for some not yet published work (joint with James Caldwell) supported by EPSRC grant EP/F031114/1.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Dyckhoff, R. (2015). Cut Elimination, Substitution and Normalisation. In: Wansing, H. (eds) Dag Prawitz on Proofs and Meaning. Outstanding Contributions to Logic, vol 7. Springer, Cham. https://doi.org/10.1007/978-3-319-11041-7_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-11041-7_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11040-0
Online ISBN: 978-3-319-11041-7
eBook Packages: Humanities, Social Sciences and LawPhilosophy and Religion (R0)