Annals of Pure and Applied Logic 149 (1-3):81-99 (2007)

Sufficient conditions for first-order-based sequent calculi to admit cut elimination by a Schütte–Tait style cut elimination proof are established. The worst case complexity of the cut elimination is analysed. The obtained upper bound is parameterized by a quantity related to the calculus. The conditions are general enough to be satisfied by a wide class of sequent calculi encompassing, among others, some sequent calculi presentations for the first order and the propositional versions of classical and intuitionistic logic, classical and intuitionistic modal logic S4, and classical and intuitionistic linear logic and some of its fragments. Moreover the conditions are such that there is an algorithm for checking if they are satisfied by a sequent calculus.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/j.apal.2007.08.001
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 70,163
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

The Mathematics of Sentence Structure.Joachim Lambek - 1958 - Journal of Symbolic Logic 65 (3):154-170.
Display Logic.Nuel D. Belnap - 1982 - Journal of Philosophical Logic 11 (4):375-417.
Contraction-Free Sequent Calculi for Intuitionistic Logic.Roy Dyckhoff - 1992 - Journal of Symbolic Logic 57 (3):795-807.
Indexed Systems of Sequents and Cut-Elimination.Grigori Mints - 1997 - Journal of Philosophical Logic 26 (6):671-696.

View all 13 references / Add more references

Citations of this work BETA

Cut-Elimination for Quantified Conditional Logic.Christoph Benzmüller - 2017 - Journal of Philosophical Logic 46 (3):333-353.
On Graph-Theoretic Fibring of Logics.A. Sernadas, C. Sernadas, J. Rasga & M. Coniglio - 2009 - Journal of Logic and Computation 19 (6):1321-1357.
Interpolation Via Translations.João Rasga, Walter Carnielli & Cristina Sernadas - 2009 - Mathematical Logic Quarterly 55 (5):515-534.

Add more citations

Similar books and articles

Are Necessary and Sufficient Conditions Converse Relations?Gilberto Gomes - 2009 - Australasian Journal of Philosophy 87 (3):375 – 387.
The Role of Quantifier Alternations in Cut Elimination.Philipp Gerhardy - 2005 - Notre Dame Journal of Formal Logic 46 (2):165-171.
What is a Complex System?James Ladyman, James Lambert & Karoline Wiesner - 2013 - European Journal for Philosophy of Science 3 (1):33-67.
James, Intentionality and Analysis.Henry Jackman - forthcoming - In Oxford Handbook of William James. New York: Oxford University Press.
Subjunctive Conditionals.R. A. Fumerton - 1976 - Philosophy of Science 43 (4):523-538.
Necessary and Sufficient Conditions.Andrew Brennan - 2008 - Stanford Encyclopedia of Philosophy.
The Logical Paradox of Causation.Yuval Steinitz - 2001 - Journal of Philosophical Research 26:223-227.
Reduction, Elimination, and Firewalking.Colin Cheyne - 1993 - Philosophy of Science 60 (2):349-357.
On the Strength and Scope of DLS.Willem Conradie - 2006 - Journal of Applied Non-Classical Logics 16 (3-4):279-296.


Added to PP index

Total views
25 ( #455,699 of 2,506,520 )

Recent downloads (6 months)
1 ( #416,791 of 2,506,520 )

How can I increase my downloads?


My notes