{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T00:05:20Z","timestamp":1759017920966,"version":"3.44.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032060846","type":"print"},{"value":"9783032060853","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The proof theory and semantics of intuitionistic modal logics have been studied by Simpson in terms of Prawitz-style labelled natural deduction systems and Kripke models. An alternative to model-theoretic semantics is provided by proof-theoretic semantics, which is a logical realization of inferentialism, in which the meaning of constructs is understood through their use. The key idea in proof-theoretic semantics is that of a base of atomic rules, all of which refer only to propositional atoms and involve no logical connectives. A specific form of proof-theoretic semantics, known as base-extension semantics (B-eS), is concerned with the validity of formulae and provides a direct counterpart to Kripke models that is grounded in the provability of atomic formulae in a base. We establish, systematically, B-eS for Simpson\u2019s intuitionistic modal logics and, also systematically, obtain soundness and completeness theorems with respect to Simpson\u2019s natural deduction systems.<\/jats:p>","DOI":"10.1007\/978-3-032-06085-3_17","type":"book-chapter","created":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:25Z","timestamp":1758969925000},"page":"318-334","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Base-Extension Semantics for\u00a0Intuitionistic Modal Logics (Extended Abstract)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-9478-6009","authenticated-orcid":false,"given":"Yll","family":"Buzoku","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6504-5838","authenticated-orcid":false,"given":"David J.","family":"Pym","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"17_CR1","unstructured":"Brandom, R.B.: Making it Explicit. Harvard University Press (1994)"},{"key":"17_CR2","doi-asserted-by":"publisher","unstructured":"Brandom, R.B.: Articulating Reasons: An Introduction to Inferentialism. Harvard University Press (2000). https:\/\/doi.org\/10.2307\/j.ctvjghvz0","DOI":"10.2307\/j.ctvjghvz0"},{"key":"17_CR3","unstructured":"Buzoku, Y.: A proof-theoretic semantics for intuitionistic linear logic (2025). https:\/\/arxiv.org\/abs\/2402.01982"},{"key":"17_CR4","unstructured":"Buzoku, Y., Pym, D.J.: Base-extension semantics for intuitionistic modal logics (2025). https:\/\/arxiv.org\/abs\/2507.06834"},{"issue":"18\u20133","key":"17_CR5","doi-asserted-by":"publisher","first-page":"13","DOI":"10.4000\/philosophiascientiae.965","volume":"3","author":"W Campos Sanz","year":"2014","unstructured":"Campos Sanz, W., Piecha, T.: A critical remark on the BHK interpretation of implication. Philos. Sci. 3(18\u20133), 13\u201322 (2014). https:\/\/doi.org\/10.4000\/philosophiascientiae.965","journal-title":"Philos. Sci."},{"key":"17_CR6","unstructured":"Dummett, M.: The Logical Basis of Metaphysics. The William James Lectures Delivered at Harvard University. Harvard University Press (1991). https:\/\/books.google.co.uk\/books?id=lvsVFxK3BPcC"},{"key":"17_CR7","doi-asserted-by":"publisher","unstructured":"Eckhardt, T., Pym, D.: Base-extension semantics for modal logic. Log. J. IGPL 3(2) (2024). https:\/\/doi.org\/10.1093\/jigpal\/jzae004","DOI":"10.1093\/jigpal\/jzae004"},{"key":"17_CR8","doi-asserted-by":"publisher","unstructured":"Eckhardt, T., Pym, D.: Base-extension semantics for S5 modal logic. Log. J. IGPL (2025). https:\/\/doi.org\/10.1093\/jigpal\/jzae131","DOI":"10.1093\/jigpal\/jzae131"},{"key":"17_CR9","doi-asserted-by":"publisher","unstructured":"Gheorghiu, A., Pym, D.: Semantical analysis of the logic of bunched implications. Stud. Log. 111 (01 2023). https:\/\/doi.org\/10.1007\/s11225-022-10028-z","DOI":"10.1007\/s11225-022-10028-z"},{"key":"17_CR10","doi-asserted-by":"publisher","unstructured":"Gheorghiu, A., Pym, D.: From proof-theoretic validity to base-extension semantics for intuitionistic propositional logic. Stud. Log. (2025). https:\/\/doi.org\/10.1007\/s11225-024-10163-9","DOI":"10.1007\/s11225-024-10163-9"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-031-43513-3_20","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"AV Gheorghiu","year":"2023","unstructured":"Gheorghiu, A.V., Gu, T., Pym, D.J.: Proof-theoretic semantics for intuitionistic multiplicative linear logic. In: Ramanayake, R., Urban, J. (eds.) TABLEAUX 2023. LNCS, vol. 14278, pp. 367\u2013385. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43513-3_20"},{"key":"17_CR12","doi-asserted-by":"publisher","unstructured":"Gheorghiu, A.V., Gu, T., Pym, D.J.: Inferentialist resource semantics. Electron. Notes Theor. Inform. Comput. Sci. 4, 9 (2024). https:\/\/doi.org\/10.46298\/entics.14727, https:\/\/entics.episciences.org\/14727","DOI":"10.46298\/entics.14727"},{"key":"17_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-024-10158-6","author":"AV Gheorghiu","year":"2024","unstructured":"Gheorghiu, A.V., Gu, T., Pym, D.J.: Proof-theoretic semantics for intuitionistic multiplicative linear logic. Stud. Log. (2024). https:\/\/doi.org\/10.1007\/s11225-024-10158-6","journal-title":"Stud. Log."},{"key":"17_CR14","unstructured":"Gu, T., Gheorghiu, A.V., Pym, D.J.: Proof-theoretic semantics for the logic of bunched implications (2023). https:\/\/arxiv.org\/abs\/2311.16719"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Hlobil, U., Brandom, R.: Reasons for Logic, Logic for Reasons: Pragmatics, Semantics, and Conceptual Roles. Routledge (2024)","DOI":"10.4324\/9781003330141"},{"key":"17_CR16","unstructured":"Lambek, J., Scott, P.: Introduction to Higher-Order Categorical Logic. Cambridge University Press (1986)"},{"key":"17_CR17","series-title":"Trends in Logic","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-319-22686-6_15","volume-title":"Advances in Proof-Theoretic Semantics","author":"T Piecha","year":"2016","unstructured":"Piecha, T.: Completeness in proof-theoretic semantics. In: Piecha, T., Schroeder-Heister, P. (eds.) Advances in Proof-Theoretic Semantics. TL, vol. 43, pp. 231\u2013251. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-22686-6_15"},{"issue":"3","key":"17_CR18","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/s10992-014-9322-x","volume":"44","author":"T Piecha","year":"2015","unstructured":"Piecha, T., Campos Sanz, W., Schroeder-Heister, P.: Failure of completeness in proof-theoretic semantics. J. Philos. Log. 44(3), 321\u2013335 (2015)","journal-title":"J. Philos. Log."},{"key":"17_CR19","unstructured":"Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Dover Books on Mathematics, Dover Publications (2006). https:\/\/books.google.co.uk\/books?id=sJj3DQAAQBAJ"},{"key":"17_CR20","doi-asserted-by":"publisher","unstructured":"Prawitz, D.: Ideas and results in proof theory. In: Fenstad, J. (ed.) Studies in Logic and the Foundations of Mathematics, vol.\u00a063, pp. 235\u2013307. Elsevier (1971). https:\/\/doi.org\/10.1016\/S0049-237X(08)70849-8","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"17_CR21","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s11225-024-10101-9","volume":"113","author":"D Pym","year":"2025","unstructured":"Pym, D., Ritter, E., Robinson, E.: Categorical proof-theoretic semantics. Stud. Log. 113, 125\u2013162 (2025)","journal-title":"Stud. Log."},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Sandqvist, T.: Base-extension semantics for intuitionistic sentential logic. Log. J. IGPL 23, 719\u2013731 (2015). https:\/\/api.semanticscholar.org\/CorpusID:7310523","DOI":"10.1093\/jigpal\/jzv021"},{"key":"17_CR23","first-page":"1142","volume":"56","author":"P Schroeder-Heister","year":"1991","unstructured":"Schroeder-Heister, P.: Uniform proof-theoretic semantics for logical constants. J. Symb. Log. 56, 1142 (1991)","journal-title":"J. Symb. Log."},{"key":"17_CR24","unstructured":"Schroeder-Heister, P.: Proof-theoretic versus model-theoretic consequence. In: Pelis, M. (ed.) The Logica Yearbook 2007. Filosofia (2008)"},{"key":"17_CR25","unstructured":"Simpson, A.K.: The proof theory and semantics of intuitionistic modal logic. Ph.D. thesis, University of Edinburgh (1994)"},{"key":"17_CR26","volume-title":"Philosophical Investigations","author":"L Wittgenstein","year":"1953","unstructured":"Wittgenstein, L.: Philosophical Investigations. Wiley-Blackwell, New York (1953)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-06085-3_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:27Z","timestamp":1758969927000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06085-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032060846","9783032060853"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06085-3_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,25]]},"assertion":[{"value":"25 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/tableaux\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}