Hostname: page-component-cd9895bd7-mkpzs Total loading time: 0 Render date: 2024-12-23T00:15:46.302Z Has data issue: false hasContentIssue false
  • English
  • Français

CUT ELIMINATION AND NORMALIZATION FOR GENERALIZED SINGLE AND MULTI-CONCLUSION SEQUENT AND NATURAL DEDUCTION CALCULI

Part of: Proof theory and constructive mathematics

Published online by Cambridge University Press:  29 June 2020

RICHARD ZACH
RICHARD ZACH*
Affiliation:
DEPARTMENT OF PHILOSOPHY UNIVERSITY OF CALGARY 2500 UNIVERSITY DRIVE NW CALGARYABT2N 1N4, CANADAE-mail:[email protected]: https://richardzach.org/
Get access Rights & Permissions [Opens in a new window]

Abstract

Any set of truth-functional connectives has sequent calculus rules that can be generated systematically from the truth tables of the connectives. Such a sequent calculus gives rise to a multi-conclusion natural deduction system and to a version of Parigot’s free deduction. The elimination rules are “general,” but can be systematically simplified. Cut-elimination and normalization hold. Restriction to a single formula in the succedent yields intuitionistic versions of these systems. The rules also yield generalized lambda calculi providing proof terms for natural deduction proofs as in the Curry–Howard isomorphism. Addition of an indirect proof rule yields classical single-conclusion versions of these systems. Gentzen’s standard systems arise as special cases.

Keywords

sequent calculuscut-eliminationnatural deductionnormalizationproof termsCurry-Howard isomorphism

MSC classification

Primary: 03F03: Proof theory, general
Secondary: 03F05: Cut-elimination and normal-form theorems 03F07: Structure of proofs
Type
Research Article
Information
The Review of Symbolic Logic , Volume 14 , Issue 3 , September 2021 , pp. 645 - 686
Check for updates
Copyright
© Association for Symbolic Logic, 2020

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

Baaz, M. (1984). Die Anwendung der Methode der Sequenzialkalküle auf nichtklassische Logiken. Dissertation, Universität Wien.Google Scholar
Baaz, M., & Fermüller, C. G. (1996). Intuitionistic counterparts of finitely-valued logics. In Proceedings of the 26th International Symposium on Multiple-Valued Logic. Los Alamitos: IEEE Press, pp. 136–141.Google Scholar
Baaz, M., Fermüller, C. G., and Zach, R. (1993). Systematic construction of natural deduction systems for many-valued logics. In Proceedings of the 23rd International Symposium on Multiple-Valued Logic. Los Alamitos: IEEE Press, pp. 208–213.CrossRefGoogle Scholar
Baaz, M., Fermüller, C. G., and Zach, R. (1994). Elimination of cuts in first-order finite-valued logics. Journal of Information Processing and Cybernetics EIK, 29(6), 333–355.Google Scholar
Baaz, M., & Leitsch, A. (2000). Cut-elimination and redundancy-elimination by resolution. Journal of Symbolic Computation, 29(2), 149–176.CrossRefGoogle Scholar
Boričić, B. R. (1985). On sequence-conclusion natural deduction systems. Journal of Philosophical Logic, 14(4), 359–377.CrossRefGoogle Scholar
Cellucci, C. (1992). Existential instantiation and normalization in sequent natural deduction. Annals of Pure and Applied Logic, 58(2), 111–148.CrossRefGoogle Scholar
Gentzen, G. (1934). Untersuchungen über das logische Schließen I–II. Mathematische Zeitschrift, 39(1), 176–210, 405–431.CrossRefGoogle Scholar
Geuvers, H., & Hurkens, T. (2017). Deriving natural deduction rules from truth tables. In Ghosh, S., & Prasad, S., editors. Logic and Its Applications. Lecture Notes in Computer Science, Vol. 10119. Berlin: Springer, pp. 123–138.CrossRefGoogle Scholar
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(1), 59–87.CrossRefGoogle Scholar
Milne, P. (2015). Inversion principles and introduction rules. In Wansing, H., editor. Dag Prawitz on Proofs and Meaning. Outstanding Contributions to Logic, Vol. 7. Berlin: Springer, pp. 189–224.Google Scholar
Negri, S., & von Plato, J. (2001). Structural Proof Theory. Cambridge, MA: Cambridge University Press.CrossRefGoogle Scholar
Parigot, M. (1992a). Free deduction: An analysis of “computations” in classical logic. In Voronkov, A., editor. Logic Programming. Lecture Notes in Computer Science, Vol. 592. Berlin: Springer, pp. 361–380.CrossRefGoogle Scholar
Parigot, M. (1992b). λμ-Calculus: An algorithmic interpretation of classical natural deduction. In Logic Programming and Automated Reasoning. Lecture Notes in Computer Science, Vol. 624. Berlin, Heidelberg, Germany: Springer, pp. 190–201.CrossRefGoogle Scholar
Prawitz, D. (1965). Natural Deduction: A Proof-Theoretical Study, Stockholm Studies in Philosophy, Vol. 3. Stockholm, Sweden: Almqvist & Wiksell.Google Scholar
Sambin, G., Battilotti, G., and Faggian, C. (2000). Basic logic: Reflection, symmetry, visibility. The Journal of Symbolic Logic, 65(3), 979–1013.CrossRefGoogle Scholar
Schroeder-Heister, P. (1984). A natural extension of natural deduction. The Journal of Symbolic Logic, 49(4), 1284–1300.CrossRefGoogle Scholar
Schroeder-Heister, P. (2013). Definitional reflection and basic logic. Annals of Pure and Applied Logic, 164(4), 491–501.CrossRefGoogle Scholar
Shoesmith, D. J., & Smiley, T. J. (1978). Multiple-Conclusion Logic. Cambridge, England: Cambridge University Press.CrossRefGoogle Scholar
Stålmarck, G. (1991). Normalization theorems for full first order classical natural deduction. The Journal of Symbolic Logic, 56(1), 129–149.CrossRefGoogle Scholar
von Kutschera, F. (1962). Zum Deduktionsbegriff der klassischen Prädikatenlogik erster Stufe. In Käsbauer, M., & von Kutschera, F., editors. Logik und Logikkalkül. Freiburg, Munich, Germany: Karl Alber, pp. 211–236.Google Scholar
Zach, R. (1993). Proof Theory of Finite-Valued Logics. Diplomarbeit. Vienna, Austria: Technische Universität Wien.Google Scholar
Zach, R. (2016). Natural deduction for the Sheffer stroke and Peirce's arrow (and any other truth-functional connective). Journal of Philosophical Logic, 45(2), 183–197.CrossRefGoogle Scholar
Zach, R. (2017). General natural deduction rules and general lambda calculi. The Bulletin of Symbolic Logic, 23(3), 371.Google Scholar