David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Journal of Symbolic Logic 72 (3):738 - 754 (2007)
Consider a general class of structural inference rules such as exchange, weakening, contraction and their generalizations. Among them, some are harmless but others do harm to cut elimination. Hence it is natural to ask under which condition cut elimination is preserved when a set of structural rules is added to a structure-free logic. The aim of this work is to give such a condition by using algebraic semantics. We consider full Lambek calculus (FL), i.e., intuitionistic logic without any structural rules, as our basic framework. Residuated lattices are the algebraic structures corresponding to FL. In this setting, we introduce a criterion, called the propagation property, that can be stated both in syntactic and algebraic terminologies. We then show that, for any set R of structural rules, the cut elimination theorem holds for FL enriched with R if and only if R satisfies the propagation property. As an application, we show that any set R of structural rules can be "completed" into another set R*, so that the cut elimination theorem holds for FL enriched with R*, while the provability remains the same
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
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
No references found.
Citations of this work BETA
Agata Ciabattoni, Nikolaos Galatos & Kazushige Terui (2012). Algebraic Proof Theory for Substructural Logics: Cut-Elimination and Completions. Annals of Pure and Applied Logic 163 (3):266-290.
Nikolaos Galatos & Hiroakira Ono (2010). Cut Elimination and Strong Separation for Substructural Logics: An Algebraic Approach. Annals of Pure and Applied Logic 161 (9):1097-1133.
Similar books and articles
Agata Ciabattoni & Kazushige Terui (2006). Towards a Semantic Characterization of Cut-Elimination. Studia Logica 82 (1):95 - 119.
Francesco Belardinelli, Peter Jipsen & Hiroakira Ono (2004). Algebraic Aspects of Cut Elimination. Studia Logica 77 (2):209 - 240.
Anna Zamansky & Arnon Avron (2006). Cut-Elimination and Quantification in Canonical Systems. Studia Logica 82 (1):157 - 176.
Richard Moot & Quintijn Puite (2002). Proof Nets for the Multimodal Lambek Calculus. Studia Logica 71 (3):415-442.
Arnon Avron & Anna Zamansky, A Triple Correspondence in Canonical Calculi: Strong Cut-Elimination, Coherence, and Non-Deterministic Semantics.
Grigori Mints (2006). Cut Elimination for S4c: A Case Study. Studia Logica 82 (1):121 - 132.
Àngel J. Gil & Jordi Rebagliato (2000). Protoalgebraic Gentzen Systems and the Cut Rule. Studia Logica 65 (1):53-89.
Kai Brünnler (2006). Cut Elimination Inside a Deep Inference System for Classical Predicate Logic. Studia Logica 82 (1):51 - 71.
Gilles Dowek & Benjamin Werner (2003). Proof Normalization Modulo. Journal of Symbolic Logic 68 (4):1289-1316.
J. W. Degen (1999). Complete Infinitary Type Logics. Studia Logica 63 (1):85-119.
Gilles Dowek & Olivier Hermant (2012). A Simple Proof That Super-Consistency Implies Cut Elimination. Notre Dame Journal of Formal Logic 53 (4):439-456.
Ryo Kashima & Norihiro Kamide (1999). Substructural Implicational Logics Including the Relevant Logic E. Studia Logica 63 (2):181-212.
Added to index2010-08-24
Total downloads4 ( #383,052 of 1,700,378 )
Recent downloads (6 months)3 ( #206,271 of 1,700,378 )
How can I increase my downloads?