{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T20:10:15Z","timestamp":1757621415116,"version":"3.44.0"},"reference-count":45,"publisher":"Oxford University Press (OUP)","issue":"6","license":[{"start":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T00:00:00Z","timestamp":1753747200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,7,29]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>The quest of smoothly combining logics so that connectives from different logics can co-exist in peace has been a fascinating topic of research. In 2015, Dag Prawitz introduced a natural deduction system for an ecumenical first-order logic, unifying classical and intuitionistic logics within a shared language. Building upon this foundation, we introduced, in a series of works, sequent systems for ecumenical logics and modal extensions. In this work we propose a new pure sequent calculus version for Prawitz\u2019s original system, where each rule features precisely one logical operator. This is achieved by extending sequents with an additional context, called stoup, and establishing the ecumenical concept of polarities. We smoothly extend these ideas for handling modalities, presenting a new pure labelled system for ecumenical modal logics. Finally, we show how this allows for naturally retrieving the ecumenical modal nested system proposed in a previous work.<\/jats:p>","DOI":"10.1093\/logcom\/exae058","type":"journal-article","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T10:43:09Z","timestamp":1753785789000},"source":"Crossref","is-referenced-by-count":0,"title":["Separability and harmony in ecumenical systems"],"prefix":"10.1093","volume":"35","author":[{"given":"Sonia","family":"Marin","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Birmingham , Birmingham B15 2TT, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luiz","family":"Carlos Pereira","sequence":"additional","affiliation":[{"name":"Department of Philosophy , UERJ, 20550-900 Rio de Janerio,","place":["Brazil"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elaine","family":"Pimentel","sequence":"additional","affiliation":[{"name":"Department Computer Science , UCL, London WC1E 6BT, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emerson","family":"Sales","sequence":"additional","affiliation":[{"name":"Gran Sasso Science Institute , 67100 L\u2019Aquila,","place":["Italy"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2025,7,29]]},"reference":[{"key":"2025090809273525100_ref1","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/S0168-0072(00)00032-4","article-title":"Focussing and proof construction","volume":"107","author":"Andreoli","year":"2001","journal-title":"Annals of Pure and Applied Logic"},{"volume-title":"Modal Logic. Cambridge Tracts in Theoretical Computer Science","year":"2001","author":"Blackburn","key":"2025090809273525100_ref2"},{"key":"2025090809273525100_ref3","first-page":"20:1","article-title":"Some axioms for mathematics","volume-title":"6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (virtual conference), volume 195 of LIPIcs","author":"Blanqui","year":"2021"},{"key":"2025090809273525100_ref4","doi-asserted-by":"crossref","first-page":"551","DOI":"10.1007\/s00153-009-0137-3","article-title":"Deep sequent systems for modal logic","volume":"48","author":"Br\u00fcnnler","year":"2009","journal-title":"Archive for Mathematical Logic"},{"key":"2025090809273525100_ref5","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1002\/malq.19920380107","article-title":"Cut elimination for propositional dynamic logic wihout ${\\ast }$","volume":"38","author":"Bull","year":"1992","journal-title":"Zeitschrift fr mathematische Logik und Grundlagen der Mathematik"},{"key":"2025090809273525100_ref6","first-page":"118","article-title":"Combining classical and intuitionistic implications","volume-title":"Frontiers of Combining Systems, 6th International Symposium, FroCoS 2007, Liverpool, UK, September 10\u201312, 2007, Proceedings, volume 4720 of Lecture Notes in Computer Science","author":"Caleiro","year":"2007"},{"key":"2025090809273525100_ref7","first-page":"16:1","article-title":"Modular focused proof systems for intuitionistic modal logics","volume-title":"1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22\u201326, 2016, Porto, Portugal","author":"Chaudhuri","year":"2016"},{"key":"2025090809273525100_ref8","first-page":"93","article-title":"Combinig classical and intuitionistic logic, or: Intuitionistic implication as a conditional","volume-title":"Frontiers of Combining Systems, First International Workshop FroCoS 1996, Munich, Germany, March 26\u201329, 1996, Proceedings, volume 3 of Applied Logic Series","author":"del Cerro","year":"1996"},{"key":"2025090809273525100_ref9","first-page":"175","article-title":"A new connective in natural deduction, and its application to quantum computing","volume-title":"Theoretical Aspects of Computing - ICTAC 2021 - 18th International Colloquium, Virtual Event, Nur-Sultan, Kazakhstan, September 8\u201310, 2021, Proceedings, volume 12819 of Lecture Notes in Computer Science","author":"D\u00edaz-Caro","year":"2021"},{"key":"2025090809273525100_ref10","first-page":"228","article-title":"On the definition of the classical connectives and quantifiers. Why is this a Proof?","volume":"27","author":"Dowek","year":"2016","journal-title":"Festschrift for Luiz Carlos Pereira"},{"volume-title":"The Logical Basis of Metaphysics","year":"1991","author":"Dummett","key":"2025090809273525100_ref11"},{"key":"2025090809273525100_ref12","doi-asserted-by":"crossref","first-page":"1109","DOI":"10.1093\/logcom\/exm037","article-title":"Call-by-value lambda-calculus and LJQ","volume":"17","author":"Dyckhoff","year":"2007","journal-title":"Journal of Logic and Computation"},{"key":"2025090809273525100_ref13","first-page":"21","article-title":"On various negative translations","volume-title":"Proceedings Third International Workshop on Classical Logic and Computation, CL&C 2010, Brno, Czech Republic, 21\u201322 August 2010, volume 47 of EPTCS","author":"Ferreira","year":"2010"},{"key":"2025090809273525100_ref14","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1215\/00294527-2377869","article-title":"Nested sequents for intuitionistic logics","volume":"55","author":"Fitting","year":"2014","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"2025090809273525100_ref15","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1017\/S0960129500001328","article-title":"A new constructive logic: classical logic","volume":"1","author":"Girard","year":"1991","journal-title":"Mathematical Structures in Computer Science"},{"key":"2025090809273525100_ref16","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/0168-0072(93)90093-S","article-title":"On the unity of logic","volume":"59","author":"Girard","year":"1993","journal-title":"Annals of Pure Applied Logic"},{"key":"2025090809273525100_ref17","first-page":"279","article-title":"Labelled tree sequents, tree hypersequents and nested (deep) sequents","volume-title":"Advances in Modal Logic 9, papers from the ninth conference on \u201dAdvances in Modal Logic,\u201d held in Copenhagen, Denmark, 22\u201325 August 2012","author":"Gor\u00e9","year":"2012"},{"key":"2025090809273525100_ref18","first-page":"61","article-title":"A lambda-calculus structure isomorphic to gentzen-style sequent calculus structure","volume-title":"Computer Science Logic, 8th International Workshop, CSL \u201894, Kazimierz, Poland, September 25\u201330, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science","author":"Herbelin","year":"1994"},{"key":"2025090809273525100_ref19","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1007\/s11229-004-6292-5","article-title":"Introduction: Proof-theoretic semantics","volume":"148","author":"Kahle","year":"2006","journal-title":"Synthese"},{"key":"2025090809273525100_ref20","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/BF01053026","article-title":"Cut-free sequent calculi for some tense logics","volume":"53","author":"Kashima","year":"1994","journal-title":"Studia Logica"},{"key":"2025090809273525100_ref21","first-page":"203","article-title":"Combining monotone and normal modal logic in nested sequents - with countermodels","volume-title":"TABLEAUX, volume 11714 of LNCS","author":"Lellmann","year":"2019"},{"key":"2025090809273525100_ref22","doi-asserted-by":"crossref","first-page":"679","DOI":"10.1016\/j.apal.2011.01.012","article-title":"A focused approach to combining logics","volume":"162","author":"Liang","year":"2011","journal-title":"Annals of Pure Applied Logic"},{"key":"2025090809273525100_ref23","first-page":"88","article-title":"Structured sequent calculi for combining intuitionistic and classical first-order logic","volume-title":"Frontiers of Combining Systems, Third International Workshop, FroCoS 2000, Nancy, France, March 22\u201324, 2000, Proceedings, volume 1794 of Lecture Notes in Computer Science","author":"Lucio","year":"2000"},{"key":"2025090809273525100_ref25","first-page":"187","article-title":"Ecumenical modal logic","volume-title":"Dynamic Logic. New Trends and Applications - Third International Workshop, DaL\u00ed 2020, Prague, Czech Republic, October 9\u201310, 2020, Revised Selected Papers, volume 12569 of Lecture Notes in Computer Science","author":"Marin","year":"2020"},{"key":"2025090809273525100_ref26","first-page":"388","article-title":"A pure view of ecumenical modalities","volume-title":"Logic, Language, Information, and Computation - 27th International Workshop, WoLLIC 2021, Virtual Event, October 5\u20138, 2021, Proceedings, volume 13038 of Lecture Notes in Computer Science","author":"Marin","year":"2021"},{"key":"2025090809273525100_ref24","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":"2025090809273525100_ref27","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1016\/j.tcs.2012.12.008","article-title":"A formal framework for specifying sequent calculus proof systems","volume":"474","author":"Miller","year":"2013","journal-title":"Theoretical Computer Science"},{"key":"2025090809273525100_ref28","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/s10670-018-0032-6","article-title":"Classical harmony and separability","volume":"85","author":"Murzi","year":"2018","journal-title":"Erkenntnis"},{"key":"2025090809273525100_ref29","article-title":"An ecumenical view of proof-theoretic semantics","volume":"abs\/2306.03656","author":"Nascimento","year":"2023","journal-title":"CoRR"},{"key":"2025090809273525100_ref30","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"Negri","year":"2001"},{"key":"2025090809273525100_ref31","first-page":"174","article-title":"Another combination of classical and intuitionistic conditionals","volume-title":"Proceedings of the 10th International Conference on Non-Classical Logics. Theory and Applications, NCL 2022, \u0141\u00f3d\u017a, Poland, 14\u201318 March 2022, volume 358 of EPTCS","author":"Niki","year":"2022"},{"key":"2025090809273525100_ref32","article-title":"A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems","volume":"abs\/2101.03113","author":"Olarte","year":"2021","journal-title":"CoRR"},{"key":"2025090809273525100_ref34","doi-asserted-by":"crossref","first-page":"1153","DOI":"10.17990\/RPF\/2017_73_3_1153","article-title":"Normalization, soundness and completeness for the propositional fragment of Prawitz\u2019 ecumenical system","volume":"73","author":"Pereira","year":"2017","journal-title":"Revista Portuguesa de Filosofia"},{"key":"2025090809273525100_ref33","first-page":"139","volume-title":"On an Ecumenical Natural Deduction with Stoup. Part I: The Propositional Case","author":"Pereira","year":"2024"},{"key":"2025090809273525100_ref35","doi-asserted-by":"crossref","first-page":"5391","DOI":"10.1007\/s11229-019-02226-5","article-title":"An ecumenical notion of entailment","volume":"198(22-S)","author":"Pimentel","year":"2021","journal-title":"Synthese"},{"key":"2025090809273525100_ref36","doi-asserted-by":"crossref","DOI":"10.1016\/B978-0-934613-04-0.50032-6","article-title":"A framework for intuitionistic modal logic","volume-title":"1st Conference on Theoretical Aspects of Reasoning About Knowledge","author":"Plotkin","year":"1986"},{"key":"2025090809273525100_ref37","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/978-1-4020-9084-4_3","article-title":"The method of tree-hypersequents for modal propositional logic","volume-title":"Towards Mathematical Philosophy, volume 28 of Trends In Logic","author":"Poggiolesi","year":"2009"},{"key":"2025090809273525100_ref38","first-page":"15","article-title":"Classical versus intuitionistic logic. Why is this a Proof?","volume":"27","author":"Prawitz","year":"2015","journal-title":"Festschrift for Luiz Carlos Pereira"},{"key":"2025090809273525100_ref39","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1016\/S0049-237X(08)70728-6","article-title":"Completeness and correspondence in first and second order semantics for modal logic","volume-title":"Proceedings of the Third Scandinavian Logic Symposium","author":"Sahlqvist","year":"1975"},{"key":"2025090809273525100_ref40","first-page":"1142","article-title":"Uniform proof-theoretic semantics for logical constants (abstract)","volume":"56","author":"Schroeder-Heister","year":"1991","journal-title":"Journal of Symbolic Logic"},{"key":"2025090809273525100_ref41","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1007\/s11229-004-6296-1","article-title":"Validity concepts in proof-theoretic semantics","volume":"148","author":"Schroeder-Heister","year":"2006","journal-title":"Synthese"},{"volume-title":"The Proof Theory and Semantics of Intuitionistic Modal Logic","year":"1994","author":"Simpson","key":"2025090809273525100_ref42"},{"key":"2025090809273525100_ref43","first-page":"209","article-title":"Cut elimination in nested sequents for intuitionistic modal logics","volume-title":"Proceedings of FOSSACS 2013","author":"Stra\u00dfburger","year":"2013"},{"key":"2025090809273525100_ref44","first-page":"25","article-title":"Combining first-order classical and intuitionistic logic","volume-title":"Proceedings of the 10th International Conference on Non-Classical Logics. Theory and Applications, NCL 2022, \u0141\u00f3d\u017a, Poland, 14\u201318 March 2022, volume 358 of EPTCS","author":"Toyooka","year":"2022"},{"volume-title":"Basic Proof Theory","year":"1996","author":"Troelstra","key":"2025090809273525100_ref45"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/6\/exae058\/63871781\/exae058.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/6\/exae058\/63871781\/exae058.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T13:28:52Z","timestamp":1757338132000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/doi\/10.1093\/logcom\/exae058\/8216169"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,29]]},"references-count":45,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2025,7,29]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exae058","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2025,9]]},"published":{"date-parts":[[2025,7,29]]},"article-number":"exae058"}}