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

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


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.



    Upload a copy of this work     Papers currently archived: 92,953

External links

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

Through your library


Added to PP

102 (#174,841)

6 months
8 (#415,941)

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 - 1996 - New York: Cambridge University Press. Edited by Helmut Schwichtenberg.
Constructivism in Mathematics: An Introduction.A. S. Troelstra & Dirk Van Dalen - 1988 - Amsterdam: North Holland. Edited by D. van Dalen.
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 (ed.), The Curry-Howard isomorphism. Louvain-la-Neuve: Academia.

View all 14 references / Add more references