Hostname: page-component-78c5997874-fbnjt Total loading time: 0 Render date: 2024-11-20T01:17:33.643Z Has data issue: false hasContentIssue false
  • English
  • Français

AN ANALYSIS OF THE RULES OF GENTZEN’S NJ AND LJ

Published online by Cambridge University Press:  08 June 2018

MIRJANA BORISAVLJEVIĆ
MIRJANA BORISAVLJEVIĆ*
Affiliation:
Faculty of Transport and Traffic Engineering, University of Belgrade
*
*FACULTY OF TRANSPORT AND TRAFFIC ENGINEERING, UNIVERSITY OF BELGRADE VOJVODE STEPE 305, 11000 BELGRADE, SERBIA E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

The connection between the rules and derivations of Gentzen’s calculi NJ and LJ will be explained by several steps (i.e., systems), and an analysis of the well-known problems of the connection between reduction steps of normalization and cut elimination, from Zucker (1974) and Urban (2014), will be given.

Keywords

03B2003F05sequent systemsnatural deduction systems
Type
Research Article
Information
The Review of Symbolic Logic , Volume 11 , Issue 2 , June 2018 , pp. 347 - 370
Copyright
Copyright © Association for Symbolic Logic 2018 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

BIBLIOGRAPHY

Borisavljević, M. (1997). Sequents, Natural Deduction and Multicategories (in Serbian). Ph.D. Thesis, University of Belgrade.Google Scholar
Borisavljević, M. (2004). Extended natural-deduction images of conversions from the system of sequents. Journal of Logic and Computation, 14(6), 769–799.CrossRefGoogle Scholar
Borisavljević, M. (2006). A connection between cut elimination and normalization. Archive for Mathematical Logic, 45(2), 113–148.CrossRefGoogle Scholar
Dyckhoff, R. (2015). Cut elimination, substitution and normalisation. In Wansing, H., editor. Dag Prawitz on Proofs and Meaning. Cham, Switzerland: Springer, pp. 163–187.Google Scholar
Gentzen, G. (1935). Untersuchungen über das logische Schließen. Mathematische Zeitschrift. In Szabo, M., editor. The Collected Papers of Gerhard Gentzen. Amsterdam: North-Holland, pp. 176–210, 405–431.Google Scholar
Kreisel, G. (1971a). A survey of proof theory II. In Fenstad, J., editor. Proceedings of the Second Scandinavian Logic Symposium. Amsterdam: North-Holland, pp. 109–170.CrossRefGoogle Scholar
Kreisel, G. (1971b). Review of: Szabo, M. E. (ed.), The collected papers of Gerhard Gentzen (North-Holland, 1969). The Journal of Philosophy, 68(8), 238–265.CrossRefGoogle Scholar
Minc, G. E. (1996). Normal forms for sequent derivations. In Odifreddi, P., editor. Kreiseliana: About and Around Georg Kreisel. Wellesley, MA: A.K. Peters, pp. 469–492.Google Scholar
Negri, S. & von Plato, J. (2001). Structural Proof Theory. Cambridge: Cambridge University Press.CrossRefGoogle Scholar
von Plato, J. (2001). Natural deduction with general elimination rules. Archive for Mathematical Logic, 40/1, 541–567.CrossRefGoogle Scholar
von Plato, J. (2003). Translations from natural deduction to sequent calculus. Mathematical Logic Quarterly, 49, 435–443.CrossRefGoogle Scholar
von Plato, J. (2008). Gentzen’s proof of normalization for natural deduction. The Bulletin of Symbolic Logic, 14/2, 240–257.CrossRefGoogle Scholar
von Plato, J. (2011). A sequent calculus isomorphic to Gentzen’s natural deduction. Review of Symbolic Logic, 4/1, 43–53.CrossRefGoogle Scholar
Pottinger, G. (1977). Normalization as a homomorphic image of cut elimination. Annals of Pure and Applied Logic, 12, 323–357.Google Scholar
Prawitz, D. (1965). Natural Deduction. Almquist and Wiksell: Stockholm.Google Scholar
Prawitz, D. (1971). Ideas and results in proof theory. In Fenstad, J. E., editor. Proceedings of the Second Scandinavian Logic Symposium. Amsterdam: North-Holland, pp. 235–307.CrossRefGoogle Scholar
Schrdeder-Heister, P. (1984). A natural extension of natural deduction. The Journal of Symbolic Logic, 49/4, 1284–1300.CrossRefGoogle Scholar
Troelstra, A. S. & Schwichtenberg, H. (2000). Basic Proof Theory (second edition). Cambridge: Cambridge University Press.CrossRefGoogle Scholar
Urban, C. (2014). Revisiting Zuckers work on the correspondence between cut-elimination and normalisation. In Pereira, L. C., Edward, E. H., and de Paiva, V., editors. Advances in Natural Deduction, A Celebration of Dag Prawitzs Work. Dordrecht: Springer, pp. 31–50.CrossRefGoogle Scholar
Zucker, J. (1974). The correspondence between cut-elimination and normalization. Annals of Pure and Applied Logic, 7, 1–112.Google Scholar