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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,592

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 cut-free sequent calculus for bi-intuitionistic logic.Rajeev Gore - manuscript
Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic.Linda Postniece - unknown
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Admissibility of structural rules for contraction-free systems of intuitionistic logic.Roy Dyckhoff & Sara Negri - 2000 - Journal of Symbolic Logic 65 (4):1499-1518.
Varieties of linear calculi.Sara Negri - 2002 - Journal of Philosophical Logic 31 (6):569-590.
A Simple Proof of Completeness and Cut-elimination for Propositional G¨ odel Logic.Arnon Avron - unknown
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 (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.

Analytics

Added to PP
2009-01-28

Downloads
101 (#171,329)

6 months
7 (#419,635)

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.
Basic proof theory.A. S. Troelstra - 2000 - New York: Cambridge University Press. Edited by Helmut Schwichtenberg.
Constructivism in mathematics: an introduction.A. S. Troelstra - 1988 - New York, N.Y.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co.. Edited by D. van Dalen.
The collected papers of Gerhard Gentzen.Gerhard Gentzen - 1969 - Amsterdam,: North-Holland Pub. Co.. Edited by M. E. Szabo.

View all 14 references / Add more references