{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T23:26:52Z","timestamp":1787009212403,"version":"3.56.0"},"reference-count":33,"publisher":"Oxford University Press (OUP)","issue":"3","license":[{"start":{"date-parts":[[2021,4,1]],"date-time":"2021-04-01T00:00:00Z","timestamp":1617235200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,4,16]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Labelled proof theory has been famously successful for modal logics by mimicking their relational semantics within deductive systems. Simpson in particular designed a framework to study a variety of intuitionistic modal logics integrating a binary relation symbol in the syntax. In this paper, we present a labelled sequent system for intuitionistic modal logics such that there is not only one but two relation symbols appearing in sequents: one for the accessibility relation associated with the Kripke semantics for normal modal logics and one for the pre-order relation associated with the Kripke semantics for intuitionistic logic. This puts our system in close correspondence with the standard birelational Kripke semantics for intuitionistic modal logics. As a consequence, it can be extended with arbitrary intuitionistic Scott\u2013Lemmon axioms. We show soundness and completeness, together with an internal cut elimination proof, encompassing a wider array of intuitionistic modal logics than any existing labelled system.<\/jats:p>","DOI":"10.1093\/logcom\/exab020","type":"journal-article","created":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T12:27:12Z","timestamp":1619612832000},"page":"998-1022","source":"Crossref","is-referenced-by-count":12,"title":["A fully labelled proof system for intuitionistic modal logics"],"prefix":"10.1093","volume":"31","author":[{"given":"Sonia","family":"Marin","sequence":"first","affiliation":[{"name":"Department of Computer Science, University College London, Gower Street, WC1E 6BT London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marianela","family":"Morales","sequence":"additional","affiliation":[{"name":"Laboratoire d\u2019Informatique de l\u2019\u00c9cole Polytechnique, 1 rue Honor\u00e9 d'Estienne d'Orves 91120 Palaiseau, France and Inria Saclay"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lutz","family":"Stra\u00dfburger","sequence":"additional","affiliation":[{"name":"Laboratoire d\u2019Informatique de l\u2019\u00c9cole Polytechnique, 1 rue Honor\u00e9 d'Estienne d'Orves 91120 Palaiseau, France and Inria Saclay"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"286","published-online":{"date-parts":[[2021,5,6]]},"reference":[{"key":"2021080214375169700_ref1","first-page":"1","article-title":"On nested sequents for constructive modal logic","volume":"11","author":"Arisaka","year":"2015","journal-title":"Logical Methods in Computer Science"},{"key":"2021080214375169700_ref2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1093\/oso\/9780198538622.003.0001","article-title":"The method of hypersequents in the proof theory of propositional non-classical logics","volume-title":"Logic: From Foundations to Applications: European Logic Colloquium","author":"Avron","year":"1996"},{"key":"2021080214375169700_ref3","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/BF02429840","article-title":"Models for normal intuitionistic modal logics","volume":"43","author":"Bo\u017ei\u0107","year":"1984","journal-title":"Studia Logica"},{"key":"2021080214375169700_ref4","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1023\/A:1005291931660","article-title":"On an intuitionistic modal logic","volume":"65","author":"Bierman","year":"2000","journal-title":"Studia Logica"},{"key":"2021080214375169700_ref5","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":"2021080214375169700_ref6","first-page":"1","article-title":"Intuitionistic non-normal modal logics: A general framework","author":"Dalmonte","year":"2020","journal-title":"Journal of Philosophical Logic"},{"key":"2021080214375169700_ref7","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/s00153-011-0254-7","article-title":"Proof analysis in intermediate logics","volume":"51","author":"Dyckhoff","year":"2012","journal-title":"Archive for Mathematical Logic"},{"key":"2021080214375169700_ref8","doi-asserted-by":"crossref","first-page":"166","DOI":"10.2307\/2273953","article-title":"Intuitionistic tense and modal logic","volume":"51","author":"Ewald","year":"1986","journal-title":"The Journal of Symbolic Logic"},{"key":"2021080214375169700_ref9","first-page":"113","article-title":"Intuitionistic modal logic with quantifiers","volume":"7","author":"Fitch","year":"1948","journal-title":"Portugali\u00e6Mathematica"},{"key":"2021080214375169700_ref10","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":"2021080214375169700_ref11","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538332.001.0001","volume-title":"Labelled Deductive Systems","author":"Gabbay","year":"1996"},{"key":"2021080214375169700_ref12","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1109\/LICS.2012.42","article-title":"Countermodels from sequent calculi in multi-modal logics","volume-title":"2012 27th Annual IEEE Symposium on Logic in Computer Science","author":"Garg","year":"2012"},{"key":"2021080214375169700_ref13","article-title":"Studies in Proof Theory","volume-title":"Proof Theory and Logical Complexity, Volume I","author":"Girard","year":"1987"},{"key":"2021080214375169700_ref14","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":"2021080214375169700_ref15","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-319-24312-2_10","article-title":"Linear nested sequents, 2-sequents and hypersequents","volume-title":"TABLEAUX: Automated Reasoning with Analytic Tableaux and Related Methods","author":"Lellmann","year":"2015"},{"key":"2021080214375169700_ref16","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/0168-0072(92)90029-Y","article-title":"2-Sequent calculus: A proof theory of modalities","volume":"58","author":"Masini","year":"1992","journal-title":"Annals of Pure and Applied Logic"},{"key":"2021080214375169700_ref17","article-title":"From axioms to synthetic inference rules via focusing","author":"Marin","year":"2020"},{"key":"2021080214375169700_ref18","first-page":"301","article-title":"Proof theory of epistemic logic of programs","volume":"23","author":"Maffezioli","year":"2014","journal-title":"Logic and Logical Philosophy"},{"key":"2021080214375169700_ref19","doi-asserted-by":"crossref","first-page":"2677","DOI":"10.1007\/s11229-012-0061-7","article-title":"The Church\u2013Fitch knowability paradox in the light of structural proof theory","volume":"190","author":"Maffezioli","year":"2013","journal-title":"Synthese"},{"key":"2021080214375169700_ref20","doi-asserted-by":"crossref","first-page":"1465","DOI":"10.1016\/j.ic.2011.10.003","article-title":"Cut-free Gentzen calculus for multimodal CK","volume":"209","author":"Mendler","year":"2011","journal-title":"Information and Computation"},{"key":"2021080214375169700_ref21","first-page":"387","article-title":"Label-free modular systems for classical and intuitionistic modal logics","volume-title":"Advances in Modal Logic","author":"Marin","year":"2014"},{"key":"2021080214375169700_ref22","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/978-3-319-66902-1_5","article-title":"Proof theory for indexed nested sequents","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods: 26th International Conference, TABLEAUX 2017","author":"Marin","year":"2017"},{"key":"2021080214375169700_ref23","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/s10992-005-2267-3","article-title":"Proof analysis in modal logic","volume":"34","author":"Negri","year":"2005","journal-title":"Journal of Philosophical Logic"},{"key":"2021080214375169700_ref24","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"Negri","year":"2001"},{"key":"2021080214375169700_ref25","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","author":"Poggiolesi","year":"2009"},{"key":"2021080214375169700_ref26","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":"2021080214375169700_ref27","first-page":"179","article-title":"Axiomatizations for some intuitionistic modal logics","volume-title":"Rendiconti del Seminario Matematico dell Universit\u00e0 Politecnica di Torino","author":"Fischer-Servi","year":"1984"},{"key":"2021080214375169700_ref28","article-title":"PhD Thesis","volume-title":"The Proof Theory and Semantics of Intuitionistic Modal Logic","author":"Simpson","year":"1994"},{"key":"2021080214375169700_ref29","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/s00153-018-0636-1","article-title":"Maehara-style modal nested calculi","volume":"58","author":"Stra\u00dfburger","year":"2019","journal-title":"Archive for Mathematical Logic"},{"key":"2021080214375169700_ref30","first-page":"209","article-title":"Cut elimination in nested sequents for intuitionistic modal logics","volume-title":"FoSSaCS\u201913","author":"Stra\u00dfburger","year":"2013"},{"key":"2021080214375169700_ref31","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"Troelstra","year":"2000"},{"key":"2021080214375169700_ref32","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3208-5","volume-title":"Labelled Non-Classical Logic","author":"Vigan\u00f2","year":"2000"},{"key":"2021080214375169700_ref33","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/0168-0072(90)90059-B","article-title":"Constructive modal logics I","volume":"50","author":"Wijesekera","year":"1990","journal-title":"Annals of Pure and Applied Logic"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/31\/3\/998\/39535289\/exab020.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/31\/3\/998\/39535289\/exab020.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,29]],"date-time":"2024-08-29T13:59:09Z","timestamp":1724939949000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/31\/3\/998\/6263488"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4]]},"references-count":33,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2021,5,6]]},"published-print":{"date-parts":[[2021,4,16]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exab020","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2021,4]]},"published":{"date-parts":[[2021,4]]}}}