{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,23]],"date-time":"2024-03-23T04:10:36Z","timestamp":1711167036729},"reference-count":32,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":1472,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2010,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper presents a polarized phase semantics, with respect to which the linear fragment of second order polarized linear logic of Laurent [15] is complete. This is done by adding a topological structure to Girard's phase semantics [9], The topological structure results naturally from the categorical construction developed by Hamano\u2013Scott [12]. The polarity shifting operator \u2193 (resp. \u2191) is interpreted as an interior (resp. closure) operator in such a manner that positive (resp. negative) formulas correspond to open (resp. closed) facts. By accommodating the exponentials of linear logic, our model is extended to the polarized fragment of the second order linear logic. Strong forms of completeness theorems are given to yield cut-eliminations for the both second order systems. As an application of our semantics, the first order conservativity of linear logic is studied over its polarized fragment of Laurent [16]. Using a counter model construction, the extension of this conservativity is shown to fail into the second order, whose solution is posed as an open problem in [16]. After this negative result, a second order conservativity theorem is proved for an eta expanded fragment of the second order linear logic, which fragment retains a focalized sequent property of [3].<\/jats:p>","DOI":"10.2178\/jsl\/1264433910","type":"journal-article","created":{"date-parts":[[2010,1,25]],"date-time":"2010-01-25T15:38:59Z","timestamp":1264433939000},"page":"77-102","source":"Crossref","is-referenced-by-count":1,"title":["A phase semantics for polarized linear logic and second order conservativity"],"prefix":"10.1017","volume":"75","author":[{"given":"Masahiro","family":"Hamano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ryo","family":"Takemura","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S002248120000284X_ref031","first-page":"738","volume":"72","author":"Terui","year":"2007","journal-title":"Which structural rules admit cut elimination? \u2014 An algebraic criterion"},{"key":"S002248120000284X_ref030","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950000311X"},{"key":"S002248120000284X_ref026","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1093\/oso\/9780198537779.003.0010","volume-title":"Substructural Logics","author":"Ono","year":"1993"},{"key":"S002248120000284X_ref015","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_16"},{"key":"S002248120000284X_ref028","first-page":"861","volume":"60","author":"Sambin","year":"1995","journal-title":"Pretopologies and completeness proofs"},{"key":"S002248120000284X_ref027","volume-title":"Natural Deduction - A Proof Theoretical Study","author":"Prawitz","year":"1965"},{"key":"S002248120000284X_ref013","first-page":"262","volume-title":"Computer Science Logic 2008","volume":"5213","author":"Hamano","year":"2008"},{"key":"S002248120000284X_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2006.09.001"},{"key":"S002248120000284X_ref008","first-page":"340","volume":"69","author":"Ehrhard","year":"2004","journal-title":"A completeness theorem for symmetric product phase spaces"},{"key":"S002248120000284X_ref007","first-page":"755","volume":"62","author":"Danos","year":"1997","journal-title":"A new deconstructive logic: Linear logic"},{"key":"S002248120000284X_ref029","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/092\/1003210"},{"key":"S002248120000284X_ref002","first-page":"1403","volume":"56","author":"Abrusci","year":"1991","journal-title":"Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic"},{"key":"S002248120000284X_ref023","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511550850.004"},{"key":"S002248120000284X_ref014","first-page":"1202","volume":"62","author":"Lafont","year":"1997","journal-title":"The finite model property for various fragments of linear logic"},{"key":"S002248120000284X_ref020","volume-title":"Theoretical Computer Science","author":"Melli\u00e8s","year":"2003"},{"key":"S002248120000284X_ref010","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001328"},{"key":"S002248120000284X_ref009","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S002248120000284X_ref005","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(99)00040-8"},{"key":"S002248120000284X_ref011","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950100336X"},{"key":"S002248120000284X_ref022","volume-title":"Proceedings of the Conference on Logic in Computer Science (LICS)","author":"Melli\u00e8s","year":"2007"},{"key":"S002248120000284X_ref019","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511550850.008"},{"key":"S002248120000284X_ref021","volume-title":"Electronic Notes in Theoretical Computer Science","author":"Melli\u00e8s","year":"2005"},{"key":"S002248120000284X_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0609-2_15"},{"key":"S002248120000284X_ref006","first-page":"167","volume-title":"Computer Science Logic 2005","author":"Curien","year":"2005"},{"key":"S002248120000284X_ref024","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00058-4"},{"key":"S002248120000284X_ref003","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"S002248120000284X_ref017","unstructured":"Laurent Olivier , A proof of the focalization property of linear logic, 2005, draft."},{"key":"S002248120000284X_ref004","first-page":"321","volume-title":"Logic programming and automated reasoning","author":"Andreoli","year":"1999"},{"key":"S002248120000284X_ref032","volume-title":"Lectures on Linear Logic","volume":"29","author":"Troelstra","year":"1992"},{"key":"S002248120000284X_ref016","unstructured":"Laurent Olivier , \u00c9tude de la polarisation en logique, Ph.D. thesis, Institut de Math\u00e9matiques de Luminy, Universit\u00e9 Aix-Marseille II, 2002."},{"key":"S002248120000284X_ref025","first-page":"790","volume":"64","author":"Okada","year":"1999","journal-title":"The finite model property for various fragments of intuitionistic linear logic"},{"key":"S002248120000284X_ref018","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.05.012"}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S002248120000284X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,23]],"date-time":"2024-03-23T03:47:14Z","timestamp":1711165634000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S002248120000284X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,3]]}},"alternative-id":["S002248120000284X"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1264433910","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,3]]}}}