Cut Elimination and Normalization for Generalized Single and Multi-Conclusion Sequent and Natural Deduction Calculi

Review of Symbolic Logic 14 (3):645-686 (2021)
  Copy   BIBTEX

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.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,593

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Tautology Elimination, Cut Elimination, and S5.Andrezj Indrzejczak - 2017 - Logic and Logical Philosophy 26 (4):461-471.
Existential instantiation and normalization in sequent natural deduction.Carlo Cellucci - 1992 - Annals of Pure and Applied Logic 58 (2):111-148.
Natural deduction with general elimination rules.Jan von Plato - 2001 - Archive for Mathematical Logic 40 (7):541-567.
Gentzen's proof systems: byproducts in a work of genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
Ultimate Normal Forms for Parallelized Natural Deductions.Neil Tennant - 2002 - Logic Journal of the IGPL 10 (3):299-337.
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Cut as Consequence.Curtis Franks - 2010 - History and Philosophy of Logic 31 (4):349-379.
On Inversion Principles.Enrico Moriconi & Laura Tesconi - 2008 - History and Philosophy of Logic 29 (2):103-113.

Analytics

Added to PP
2020-06-30

Downloads
22 (#606,933)

6 months
3 (#445,838)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Richard Zach
University of Calgary

Citations of this work

No citations found.

Add more citations

References found in this work

Structural Proof Theory.Sara Negri, Jan von Plato & Aarne Ranta - 2001 - New York: Cambridge University Press. Edited by Jan Von Plato.
A natural extension of natural deduction.Peter Schroeder-Heister - 1984 - Journal of Symbolic Logic 49 (4):1284-1300.
Elimination of Cuts in First-order Finite-valued Logics.Matthias Baaz, Christian G. Fermüller & Richard Zach - 1993 - Journal of Information Processing and Cybernetics EIK 29 (6):333-355.

View all 10 references / Add more references