{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T12:04:37Z","timestamp":1753877077129,"version":"3.41.2"},"reference-count":35,"publisher":"Oxford University Press (OUP)","issue":"3","license":[{"start":{"date-parts":[[2025,5,9]],"date-time":"2025-05-09T00:00:00Z","timestamp":1746748800000},"content-version":"vor","delay-in-days":29,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,4,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>Proof theorists have long been struggling to provide simple accounts of various modal logics. Drawing on the recent literature on metainferences, I develop in the present paper a novel approach to this challenge: regular sequent systems augmented with natural deduction-like rules for assuming and discharging sequents. Based on this approach, I introduce an elegant calculus for the modal logic $S4$. Various discharging conditions on assumptions are shown to yield the weaker logics $K,D$, and $T$. The rules in these calculi have attractive proof-theoretic properties: they are explicit, symmetrical, and non-circular, and they enjoy the subformula property.<\/jats:p>","DOI":"10.1093\/jigpal\/jzaf013","type":"journal-article","created":{"date-parts":[[2025,5,9]],"date-time":"2025-05-09T00:16:31Z","timestamp":1746749791000},"source":"Crossref","is-referenced-by-count":0,"title":["Simple sequent systems for the modal logics <i>K,D,T,<\/i> and <i>S<\/i>4"],"prefix":"10.1093","volume":"33","author":[{"given":"Rea","family":"Golan","sequence":"first","affiliation":[{"name":"Ben Gurion University of the Negev , Beer-Sheva, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2025,5,8]]},"reference":[{"key":"2025052605514412900_ref1","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 nonclassical logics","volume-title":"Logic: From Foundations to Applications","author":"Avron","year":"1996"},{"key":"2025052605514412900_ref2","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1023\/A:1005291931660","article-title":"On an intuitionistic modal logic","volume":"65","author":"Biermann","year":"2000","journal-title":"Stud Log"},{"key":"2025052605514412900_ref3","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1007\/978-3-030-25365-3_18","article-title":"ST, LP and tolerant metainferences","volume-title":"Graham Priest on Dialetheism and Paraconsistency","author":"Dicher","year":"2019"},{"key":"2025052605514412900_ref4","doi-asserted-by":"publisher","first-page":"149","DOI":"10.2307\/2273797","article-title":"Sequent-systems for modal logic","volume":"50","author":"Do\u0117n","year":"1985","journal-title":"J Symb Log"},{"key":"2025052605514412900_ref5","first-page":"362","article-title":"Logical constants as punctuation marks","volume":"30","author":"Do\u0117n","year":"1989","journal-title":"Notre Dame J Formal Log"},{"volume-title":"The Logical Basis of Metaphysics","year":"1991","author":"Dummett","key":"2025052605514412900_ref6"},{"key":"2025052605514412900_ref7","first-page":"152","article-title":"Tree proofs in modal logic","volume":"31","author":"Fitch","year":"1966","journal-title":"J Symb Log"},{"key":"2025052605514412900_ref8","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139342117","volume-title":"Modal logic for Philosophers","author":"Garson","year":"2013"},{"key":"2025052605514412900_ref9","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1093\/analys\/anab032","article-title":"There is no tenable notion of global metainferential validity","volume":"81","author":"Golan","year":"2021","journal-title":"Analysis"},{"key":"2025052605514412900_ref10","doi-asserted-by":"publisher","first-page":"1296","DOI":"10.1017\/S1755020322000090","article-title":"A simple sequent system for minimally inconsistent LP","volume":"16","author":"Golan","year":"2023","journal-title":"Rev Symb Log"},{"key":"2025052605514412900_ref11","doi-asserted-by":"crossref","first-page":"182","DOI":"10.26686\/ajl.v19i5.7540","article-title":"Minimally nonstandard K3 and FDE","volume":"19","author":"Golan","year":"2022","journal-title":"Australasian J Log"},{"key":"2025052605514412900_ref12","doi-asserted-by":"crossref","first-page":"4759","DOI":"10.1007\/s11229-018-1687-x","article-title":"Faithfulness for naive validity","volume":"196","author":"Hlobil","year":"2019","journal-title":"Synthese"},{"key":"2025052605514412900_ref13","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/BF00257380","article-title":"Valuational semantics of rule derivability","volume":"25","author":"Humberstone","year":"1996","journal-title":"J Philos Log"},{"key":"2025052605514412900_ref14","doi-asserted-by":"crossref","DOI":"10.1007\/978-90-481-8785-0","volume-title":"Natural Deduction, Hybrid Systems and Modal Logics (Vol. 30)","author":"Indrzejczak","year":"2010"},{"key":"2025052605514412900_ref15","article-title":"Sequents and trees","volume-title":"Studies in Universal Logic","author":"Indrzejczak","year":"2021"},{"key":"2025052605514412900_ref16","first-page":"37","volume-title":"Advances in Modal Logic 2020","author":"K\u00fcrbis","year":"2020"},{"key":"2025052605514412900_ref17","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"Negri","year":"2001"},{"key":"2025052605514412900_ref18","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":"J Philos Log"},{"key":"2025052605514412900_ref19","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1111\/j.1747-9991.2011.00418.x","article-title":"Proof theory for modal logic","volume":"6","author":"Negri","year":"2011","journal-title":"Philos Compass"},{"key":"2025052605514412900_ref20","first-page":"113","article-title":"Gentzen method in modal calculi","volume":"9","author":"Ohnishi","year":"1957","journal-title":"Osaka Math J"},{"key":"2025052605514412900_ref21","doi-asserted-by":"publisher","first-page":"1605","DOI":"10.1007\/s10670-020-00264-x","article-title":"A Hypersequent solution to the Inferentialist problem of modality","volume":"87","author":"Parisi","year":"2022","journal-title":"Erkenntnis"},{"key":"2025052605514412900_ref22","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/382780.382785","article-title":"A modal analysis of staged computation","volume":"48","author":"Davies","year":"2001","journal-title":"J ACM"},{"key":"2025052605514412900_ref23","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, Trends in Philosophy Series, Vol. 28","author":"Poggiolesi","year":"2009"},{"volume-title":"Gentzen Calculi for Modal Propositional Logic (Vol. 32)","year":"2010","author":"Poggiolesi","key":"2025052605514412900_ref24"},{"key":"2025052605514412900_ref25","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1007\/s10992-010-9133-7","article-title":"General-elimination harmony and the meaning of the logical constants","volume":"39","author":"Read","year":"2010","journal-title":"J Philos Log"},{"key":"2025052605514412900_ref26","first-page":"151","article-title":"Proofnets for ${S}\\_5$: Sequents and circuits for modal logic","volume":"28","author":"Restall","year":"2007","journal-title":"Log Colloq"},{"key":"2025052605514412900_ref27","doi-asserted-by":"publisher","first-page":"1611","DOI":"10.1016\/j.apal.2011.12.012","article-title":"A cut-free sequent system for two-dimensional modal logic-and why it matters","volume":"163","author":"Restall","year":"2012","journal-title":"Ann Pure Appl Log"},{"key":"2025052605514412900_ref28","doi-asserted-by":"crossref","first-page":"109","DOI":"10.18778\/0138-0680.2023.6","article-title":"Structural rules in natural deduction with alternatives","volume":"52","author":"Restall","year":"2023","journal-title":"Bull Sect Log"},{"author":"Restall","article-title":"Speech acts and the quest for a natural account of classical proof","key":"2025052605514412900_ref29"},{"key":"2025052605514412900_ref30","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/BF00293433","article-title":"The modal logic of provability: the sequential approach","volume":"11","author":"Sambin","year":"1982","journal-title":"J Philos Log"},{"key":"2025052605514412900_ref31","doi-asserted-by":"crossref","first-page":"1185","DOI":"10.1007\/s11225-014-9562-3","article-title":"The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony","volume":"102","author":"Schroeder-Heister","year":"2014","journal-title":"Stud Log"},{"key":"2025052605514412900_ref32","first-page":"455","article-title":"The sequent calculus for modal logic $D$","volume":"12","author":"Valentini","year":"1993","journal-title":"Bolletino dell\u2019Unione Matematica Italiana"},{"key":"2025052605514412900_ref33","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1093\/logcom\/4.2.125","article-title":"Sequent calculi for normal modal propositional logic","volume":"4","author":"Wansing","year":"1994","journal-title":"J Log Comput"},{"key":"2025052605514412900_ref34","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1023\/A:1005217827758","article-title":"On the idea of a proof-theoretic semantics and the meaning of the logical operations","volume":"64","author":"Wansing","year":"2000","journal-title":"Stud Log"},{"key":"2025052605514412900_ref35","article-title":"Displaying modal logic","volume-title":"Trends in Logic Series, Vol. 3","author":"Wansing","year":"2013"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/33\/3\/jzaf013\/63129339\/jzaf013.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/33\/3\/jzaf013\/63129339\/jzaf013.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,26]],"date-time":"2025-05-26T09:51:53Z","timestamp":1748253113000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/doi\/10.1093\/jigpal\/jzaf013\/8127216"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,10]]},"references-count":35,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,4,10]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzaf013","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"type":"print","value":"1367-0751"},{"type":"electronic","value":"1368-9894"}],"subject":[],"published-other":{"date-parts":[[2025,6]]},"published":{"date-parts":[[2025,4,10]]},"article-number":"jzaf013"}}