{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:20:44Z","timestamp":1758979244720},"reference-count":27,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":2384,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2007,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p><jats:p>We consider full Lambek calculus (<jats:bold>FL<\/jats:bold>), i.e., intuitionistic logic without any structural rules, as our basic framework. Residuated lattices are the algebraic structures corresponding to <jats:bold>FL<\/jats:bold>. 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 \u211b of structural rules, the cut elimination theorem holds for <jats:bold>FL<\/jats:bold> enriched with \u211b if and only if \u211b satisfies the propagation property.<\/jats:p><jats:p>As an application, we show that any set \u211b of structural rules can be \u201ccompleted\u201d into another set \u211b*, so that the cut elimination theorem holds for <jats:bold>FL<\/jats:bold> enriched with \u211b*. while the provability remains the same.<\/jats:p>","DOI":"10.2178\/jsl\/1191333839","type":"journal-article","created":{"date-parts":[[2007,12,19]],"date-time":"2007-12-19T16:25:04Z","timestamp":1198081504000},"page":"738-754","source":"Crossref","is-referenced-by-count":15,"title":["Which structural rules admit cut elimination? An algebraic criterion"],"prefix":"10.1017","volume":"72","author":[{"given":"Kazushige","family":"Terui","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200005053_ref017","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80414-1"},{"key":"S0022481200005053_ref020","first-page":"790\u2013802","volume":"64","author":"Okada","year":"1999","journal-title":"The finite model property for various fragments of intuitionistic linear logic"},{"key":"S0022481200005053_ref008","volume-title":"Substructural Logics","author":"Do\u0161en","year":"1993"},{"key":"S0022481200005053_ref009","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0022481200005053_ref007","first-page":"95\u2013119","article-title":"Towards a semantic characterization of cut-elimination","volume":"82","author":"Ciabattoni","year":"2006","journal-title":"Stadia Logica"},{"key":"S0022481200005053_ref015","first-page":"2\u201323","volume-title":"Tableaux 2002","volume":"2381","author":"Miller","year":"2002"},{"key":"S0022481200005053_ref006","first-page":"135\u2013149","volume-title":"LPAR 2006","volume":"4246","author":"Ciabattoni","year":"2006"},{"key":"S0022481200005053_ref004","volume-title":"Language in Action: Categories, Lambdas and Dynamic Logic","author":"van Benthem","year":"1991"},{"key":"S0022481200005053_ref003","first-page":"1\u201332","article-title":"Algebraic aspects of cut elimination","volume":"68","author":"Belardinelli","year":"2001","journal-title":"Stadia Logica"},{"key":"S0022481200005053_ref026","first-page":"251\u2013265","volume-title":"IJCAR 2006","volume":"4130","author":"Zamansky","year":"2006"},{"key":"S0022481200005053_ref014","first-page":"227\u2013249","article-title":"Substructural logics with mingle","volume":"11","author":"Kamide","year":"2002","journal-title":"Journal of Logic, Language and Information"},{"key":"S0022481200005053_ref005","first-page":"503\u2013517","volume-title":"CSL 2004","volume":"3210","author":"Ciabattoni","year":"2004"},{"key":"S0022481200005053_ref010","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511629150"},{"key":"S0022481200005053_ref013","first-page":"19\u201356","volume-title":"Ordered Algebraic Structures","author":"Jipsen","year":"2002"},{"key":"S0022481200005053_ref002","first-page":"529\u2013543","volume-title":"IJCAR 2001","volume":"2083","author":"Avron","year":"2001"},{"key":"S0022481200005053_ref016","doi-asserted-by":"publisher","DOI":"10.4288\/jafpos1956.2.183"},{"key":"S0022481200005053_ref018","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00058-4"},{"key":"S0022481200005053_ref011","first-page":"215\u2013272","volume-title":"Computational Logic","author":"Girard","year":"1999"},{"key":"S0022481200005053_ref019","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00024-5"},{"key":"S0022481200005053_ref022","first-page":"259\u2013291","volume-title":"Substructural Logics","author":"Ono","year":"1994"},{"key":"S0022481200005053_ref001","first-page":"1403\u20131451","volume":"56","author":"Abrusci","year":"1991","journal-title":"Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic"},{"key":"S0022481200005053_ref025","volume-title":"Lectures on Linear Logic","author":"Troelstra","year":"1992"},{"key":"S0022481200005053_ref023","first-page":"177\u2013212","article-title":"Substructural logics and residuated lattices \u2014 An introduction","volume":"20","author":"Ono","year":"2003","journal-title":"Trends in Logic"},{"key":"S0022481200005053_ref024","volume-title":"An Introduction to Substructural Logics","author":"Restall","year":"1999"},{"key":"S0022481200005053_ref027","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-006-6611-6"},{"key":"S0022481200005053_ref012","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1094061862"},{"key":"S0022481200005053_ref021","first-page":"95\u2013104","volume-title":"Mathematical Logic","author":"Ono","year":"1990"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200005053","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T21:21:11Z","timestamp":1556745671000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200005053\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,9]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,9]]}},"alternative-id":["S0022481200005053"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1191333839","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,9]]}}}