{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T02:49:50Z","timestamp":1771642190294,"version":"3.50.1"},"reference-count":25,"publisher":"Oxford University Press (OUP)","issue":"3","license":[{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":1,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,3,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>In this paper, a new approach to the issue of extra-logical information within analytic (i.e. obeying the sub-formula property) sequent systems is introduced. We prove that incorporating extra-logical axioms into a purely logical system can preserve analyticity, provided these axioms belong to a suitable class of formulas that can be decomposed into a set of equivalent initial sequents and are permutable over the cut rule. Our approach is applicable not only to first-order classical and intuitionistic logics, but also to substructural logics. Furthermore, we establish a limit for the augmented systems under analysis: exceeding the boundaries of their respective classes of extra-logical axioms leads to either a loss of analyticity or a loss of structural properties.<\/jats:p>","DOI":"10.1093\/logcom\/exae013","type":"journal-article","created":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T10:30:12Z","timestamp":1712313012000},"source":"Crossref","is-referenced-by-count":2,"title":["Analyticity with extra-logical information"],"prefix":"10.1093","volume":"35","author":[{"given":"Mario","family":"Piazza","sequence":"first","affiliation":[{"name":"Scuola Normale Superiore di Pisa , Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matteo","family":"Tesi","sequence":"additional","affiliation":[{"name":"Institute of Logic and Computation , TU Wien, Vienna, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2024,4,4]]},"reference":[{"key":"2025042210091749300_ref1","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","article-title":"Logic programming with focusing proofs in linear logic","volume":"2","author":"Andreoli","year":"1992","journal-title":"Journal of Logic and Computation"},{"key":"2025042210091749300_ref2","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BF00881838","article-title":"Gentzen-type systems, resolution and tableaux","volume":"10","author":"Avron","year":"1993","journal-title":"Journal of Automated Reasoning"},{"key":"2025042210091749300_ref3","doi-asserted-by":"crossref","first-page":"5433","DOI":"10.1016\/j.tcs.2011.05.053","article-title":"Corrected upper bounds for free-cut elimination","volume":"412","author":"Beckmann","year":"2011","journal-title":"Theoretical Computer Science"},{"key":"2025042210091749300_ref4","volume-title":"Introduction to Mathematical Logic","author":"Church","year":"1956"},{"key":"2025042210091749300_ref5","first-page":"229","article-title":"From axioms to analytic rules in nonclassical logics","volume-title":"23rd Annual IEEE Symposium on Logic in Computer Science","author":"Ciabattoni","year":"2008"},{"key":"2025042210091749300_ref6","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/978-3-642-04027-6_14","article-title":"Expanding the realm of systematic proof theory","volume-title":"International Workshop on Computer Science Logic","author":"Ciabattoni","year":"2009"},{"key":"2025042210091749300_ref7","doi-asserted-by":"crossref","first-page":"41","DOI":"10.2307\/2274953","article-title":"Quantales and non commutative logic","volume":"55","author":"Yetter","year":"1990","journal-title":"The Journal of Symbolic Logic"},{"key":"2025042210091749300_ref8","doi-asserted-by":"crossref","first-page":"558","DOI":"10.1016\/j.jal.2014.08.001","article-title":"A logical calculus for controlled monotonicity","volume":"12","author":"D\u2019Agostino","year":"2014","journal-title":"Journal of Applied Logic"},{"key":"2025042210091749300_ref9","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schliessen","volume":"39","author":"Gentzen","year":"1934-1935","journal-title":"Mathematische Zeitschrift"},{"key":"2025042210091749300_ref10","first-page":"19","article-title":"Neue Fassung des Widerspruchsfreiheitsbeweises f\u00fcr die reine Zahlentheorie","volume":"4","author":"Gentzen","year":"1938","journal-title":"Forschungen zur Logik und zur Grundlegung der exakter Wissenschaften"},{"key":"2025042210091749300_ref11","volume-title":"Proof-Theory and Logical Complexity","author":"Girard","year":"1986"},{"key":"2025042210091749300_ref12","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1017\/S0960129500001328","article-title":"A new constructive logic: Classic logic","volume":"1","author":"Girard","year":"1991","journal-title":"Mathematical Structures in Computer Science"},{"key":"2025042210091749300_ref13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"2025042210091749300_ref14","first-page":"1","article-title":"Untersuchungen zum Pr\u00e4dikatenkalk\u00fcl","volume":"I","author":"Ketonen","year":"1944","journal-title":"Annales Academiae Scientiarum Fennicae. Series A"},{"key":"2025042210091749300_ref15","volume-title":"Etude de la Polarisation en Logique","author":"Laurent","year":"2002"},{"key":"2025042210091749300_ref16","volume-title":"Bridges from Classical to Nonmonotonic Logic","author":"Makinson","year":"2005"},{"key":"2025042210091749300_ref17","doi-asserted-by":"crossref","first-page":"103091","DOI":"10.1016\/j.apal.2022.103091","article-title":"From axioms to synthetic inference rules via focusing","volume":"173","author":"Marin","year":"2022","journal-title":"Annals of Pure and Applied Logic"},{"key":"2025042210091749300_ref18","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"Negri","year":"2001"},{"key":"2025042210091749300_ref19","doi-asserted-by":"crossref","first-page":"418","DOI":"10.2307\/420956","article-title":"Cut elimination in the presence of axioms","volume":"4","author":"Negri","year":"1998","journal-title":"Bulletin of Symbolic Logic"},{"key":"2025042210091749300_ref20","doi-asserted-by":"crossref","first-page":"708","DOI":"10.1093\/jigpal\/jzw032","article-title":"Uniqueness of axiomatic extensions of cut-free classical propositional logic","volume":"24","author":"Piazza","year":"2016","journal-title":"Logic Journal of the IGPL"},{"key":"2025042210091749300_ref21","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1093\/logcom\/exv051","article-title":"Unifying logics via context-sensitiveness","volume":"27","author":"Piazza","year":"2017","journal-title":"Journal of Logic and Computation"},{"key":"2025042210091749300_ref22","doi-asserted-by":"crossref","first-page":"163","DOI":"10.2307\/2370324","article-title":"Introduction to a general theory of elementary propositions","volume":"43","author":"Post","year":"1921","journal-title":"American Journal of Mathematics"},{"key":"2025042210091749300_ref23","volume-title":"Classical Logic and Intuitionistic Logic: Equivalent Formulations in Natural Deduction, Goedel-Kolmogorov-Glivenko Translation","author":"Retor\u00e9","year":"2016"},{"key":"2025042210091749300_ref24","volume-title":"Proof Theory","author":"Takeuti","year":"1975"},{"key":"2025042210091749300_ref25","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"Troelstra","year":"2000"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/3\/exae013\/57164922\/exae013.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/3\/exae013\/57164922\/exae013.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,22]],"date-time":"2025-04-22T14:53:57Z","timestamp":1745333637000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/doi\/10.1093\/logcom\/exae013\/7639991"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,4]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,3,11]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exae013","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2025,4]]},"published":{"date-parts":[[2024,4,4]]},"article-number":"exae013"}}