{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T12:05:43Z","timestamp":1759147543899},"reference-count":29,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,5,27]],"date-time":"2014-05-27T00:00:00Z","timestamp":1401148800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Review of Symbolic Logic"],"published-print":{"date-parts":[[2014,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Uniform interpolation property of a given logic is a stronger form of Craig\u2019s interpolation property where both <jats:italic>pre-interpolant<\/jats:italic> and <jats:italic>post-interpolant<\/jats:italic> always exist uniformly for any provable implication in the logic. It is known that there exist logics, e.g., modal propositional logic <jats:bold>S4<\/jats:bold>, which have Craig\u2019s interpolation property but do not have uniform interpolation property. The situation is even worse for predicate logics, as classical predicate logic does not have uniform interpolation property as pointed out by L. Henkin.<\/jats:p><jats:p>In this paper, uniform interpolation property of basic substructural logics is studied by applying the proof-theoretic method introduced by A. Pitts (Pitts, 1992). It is shown that uniform interpolation property holds even for their predicate extensions, as long as they can be formalized by sequent calculi without contraction rules. For instance, uniform interpolation property of full Lambek predicate calculus, i.e., the substructural logic without any structural rule, and of both linear and affine predicate logics without exponentials are proved.<\/jats:p>","DOI":"10.1017\/s175502031400015x","type":"journal-article","created":{"date-parts":[[2014,5,27]],"date-time":"2014-05-27T08:27:35Z","timestamp":1401179255000},"page":"455-483","source":"Crossref","is-referenced-by-count":6,"title":["UNIFORM INTERPOLATION IN SUBSTRUCTURAL LOGICS"],"prefix":"10.1017","volume":"7","author":[{"given":"MAJID","family":"ALIZADEH","sequence":"first","affiliation":[]},{"given":"FARZANEH","family":"DERAKHSHAN","sequence":"additional","affiliation":[]},{"given":"HIROAKIRA","family":"ONO","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,5,27]]},"reference":[{"key":"S175502031400015X_ref7","doi-asserted-by":"publisher","DOI":"10.2307\/2275765"},{"key":"S175502031400015X_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/BF00671566"},{"key":"S175502031400015X_ref13","unstructured":"Hudelmaier J . (1989). Bounds for cut elimination in intuitionistic propositional logic. PhD Thesis, University of T\u00fcbingen."},{"key":"S175502031400015X_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/s11229-008-9351-5"},{"key":"S175502031400015X_ref3","first-page":"2","article-title":"Intuitionistic system without contraction","volume":"6","author":"Dard\u017eani\u00e1","year":"1977","journal-title":"Bulletin of the Section of Logic"},{"key":"S175502031400015X_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370272"},{"key":"S175502031400015X_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-012-9379-x"},{"key":"S175502031400015X_ref29","volume-title":"A Survey of Mathematical Logic","author":"Wang","year":"1963"},{"key":"S175502031400015X_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0609-2_8"},{"key":"S175502031400015X_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S175502031400015X_ref24","doi-asserted-by":"publisher","DOI":"10.2307\/2275175"},{"key":"S175502031400015X_ref11","doi-asserted-by":"publisher","DOI":"10.2307\/2271066"},{"key":"S175502031400015X_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-007-9021-5"},{"key":"S175502031400015X_ref25","unstructured":"Tamura S . (1974). On a decision procedure for free lo-algebraic systems. Technical report of Mathematics, Yamaguchi University 9."},{"key":"S175502031400015X_ref12","unstructured":"Heuerding A . (1998). Sequent calculi for proof search in some modal logics. Ph. D. thesis, University of Bern."},{"key":"S175502031400015X_ref6","first-page":"532","volume-title":"Residuated Lattices: An Algebraic Glimpse at Substructural Logics","volume":"151","author":"Galatos","year":"2007"},{"key":"S175502031400015X_ref18","doi-asserted-by":"publisher","DOI":"10.2307\/2310058"},{"key":"S175502031400015X_ref15","volume-title":"Provability in Logic","author":"Kanger","year":"1957"},{"key":"S175502031400015X_ref26","volume-title":"Lectures on Linear Logic","volume":"29","author":"Troelstra","year":"1992"},{"key":"S175502031400015X_ref19","first-page":"235","article-title":"On the interpolation theorem of Craig (Japanese)","volume":"12","author":"Maehara","year":"1960","journal-title":"Sugaku"},{"key":"S175502031400015X_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/BF01061237"},{"key":"S175502031400015X_ref22","doi-asserted-by":"publisher","DOI":"10.2969\/msjmemoirs\/00201C060"},{"key":"S175502031400015X_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370189"},{"key":"S175502031400015X_ref23","doi-asserted-by":"publisher","DOI":"10.2307\/2273798"},{"key":"S175502031400015X_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/s11229-008-9359-x"},{"key":"S175502031400015X_ref10","doi-asserted-by":"publisher","DOI":"10.1070\/IM1982v018n01ABEH001382"},{"key":"S175502031400015X_ref14","unstructured":"Idziak P. M . (1984). Lattice operations in BCK-algebras. PhD Thesis, Jagiellonian University, Krak\u00f3w, Poland."},{"key":"S175502031400015X_ref28","first-page":"139","volume-title":"Lecture Notes in Logic 6 \u201cG\u00f6del \u201996: Logical foundations of mathematics, computer science and physics \u2014 Kurt G\u00f6del\u2019s legacy\u201d","author":"Visser","year":"1996"},{"key":"S175502031400015X_ref5","doi-asserted-by":"publisher","DOI":"10.2307\/2275431"}],"container-title":["The Review of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S175502031400015X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,22]],"date-time":"2019-04-22T01:07:41Z","timestamp":1555895261000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S175502031400015X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,5,27]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,9]]}},"alternative-id":["S175502031400015X"],"URL":"https:\/\/doi.org\/10.1017\/s175502031400015x","relation":{},"ISSN":["1755-0203","1755-0211"],"issn-type":[{"value":"1755-0203","type":"print"},{"value":"1755-0211","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,5,27]]}}}