Which Structural Rules Admit Cut Elimination? An Algebraic Criterion

Journal of Symbolic Logic 72 (3):738 - 754 (2007)
Abstract
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)
Options
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history Request removal from index
 
Download options
PhilPapers Archive


Upload a copy of this paper     Check publisher's policy on self-archival     Papers currently archived: 11,825
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

No references found.

Citations of this work BETA
Similar books and articles
Gilles Dowek & Benjamin Werner (2003). Proof Normalization Modulo. Journal of Symbolic Logic 68 (4):1289-1316.
Analytics

Monthly downloads

Sorry, there are not enough data points to plot this chart.

Added to index

2010-08-24

Total downloads

1 ( #454,238 of 1,100,101 )

Recent downloads (6 months)

1 ( #304,144 of 1,100,101 )

How can I increase my downloads?

My notes
Sign in to use this feature


Discussion
Start a new thread
Order:
There  are no threads in this forum
Nothing in this forum yet.