Cut-elimination and a permutation-free sequent calculus for intuitionistic logic

&
Studia Logica 60 (1):107-118 (1998)
  Copy   BIBTEX

Abstract

We describe a sequent calculus, based on work of Herbelin, of which the cut-free derivations are in 1-1 correspondence with the normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path ordering theorem of Dershowitz.

Categories

Keywords

Reprint years

DOI

10.1023/a:1005099619660

Other Versions

No versions found

Links

PhilArchive

    This entry is not archived by us. If you are the author and have permission from the publisher, we recommend that you archive it. Many publishers automatically grant permission to authors to archive pre-prints. By uploading a copy of your work, you will enable us to better index it, making it easier to find.

    Upload a copy of this work     Papers currently archived: 106,894

External links

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

Through your library

My notes

Similar books and articles

A normalizing system of natural deduction for intuitionistic linear logic.Sara Negri - 2002 - Archive for Mathematical Logic 41 (8):789-810.
A cut-free sequent calculus for the bi-intuitionistic logic 2Int.Sara Ayhan - manuscript
Translations from natural deduction to sequent calculus.Jan von Plato - 2003 - Mathematical Logic Quarterly 49 (5):435.
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev, Advances in Modal Logic. CSLI Publications. pp. 43-66.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev, Advances in Modal Logic. CSLI Publications. pp. 43-66.
Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic.Linda Postniece - unknown
Cut Elimination and Normalization for Generalized Single and Multi-Conclusion Sequent and Natural Deduction Calculi.Richard Zach - 2021 - Review of Symbolic Logic 14 (3):645-686.
An Analytic Calculus for the Intuitionistic Logic of Proofs.Brian Hill & Francesca Poggiolesi - 2019 - Notre Dame Journal of Formal Logic 60 (3):353-393.
Tautology Elimination, Cut Elimination, and S5.Andrezj Indrzejczak - 2017 - Logic and Logical Philosophy 26 (4):461-471.

Analytics

Added to PP
2009-01-28

Downloads
127 (#182,719)

6 months
12 (#301,168)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Advances in Proof-Theoretic Semantics.Peter Schroeder-Heister & Thomas Piecha (eds.) - 2015 - Cham, Switzerland: Springer Verlag.
1999 Spring Meeting of the Association for Symbolic Logic.Charles Parsons - 1999 - Bulletin of Symbolic Logic 5 (4):479-484.

Add more citations

References found in this work

Natural deduction: a proof-theoretical study.Dag Prawitz - 1965 - Mineola, N.Y.: Dover Publications.
Constructivism in Mathematics: An Introduction.A. S. Troelstra & Dirk Van Dalen - 1988 - Amsterdam: North Holland. Edited by D. van Dalen.
Basic proof theory.A. S. Troelstra - 2000 - New York: Cambridge University Press. Edited by Helmut Schwichtenberg.
The collected papers of Gerhard Gentzen.Gerhard Gentzen - 1969 - Amsterdam,: North-Holland Pub. Co.. Edited by M. E. Szabo.
The formulæ-as-types notion of construction.W. A. Howard - 1995 - In Philippe De Groote, The Curry-Howard isomorphism. Louvain-la-Neuve: Academia.

View all 12 references / Add more references