{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,20]],"date-time":"2025-09-20T01:34:20Z","timestamp":1758332060103,"version":"3.44.0"},"reference-count":68,"publisher":"Oxford University Press (OUP)","issue":"7","license":[{"start":{"date-parts":[[2024,8,6]],"date-time":"2024-08-06T00:00:00Z","timestamp":1722902400000},"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,9,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>We design and study various topological semantics for the diamond-free intuitionistic modal logic $\\textsf{iS4}$, an intuitionistic analogue of $\\textsf{S4}$. Ultimately we prove that ordinary topological spaces can be used as semantics, using the specialization order to interpret intuitionistic implication and the interior for the modality. Some of our soundness and completeness results are mechanised in Coq.<\/jats:p>","DOI":"10.1093\/logcom\/exae030","type":"journal-article","created":{"date-parts":[[2024,8,6]],"date-time":"2024-08-06T23:33:56Z","timestamp":1722987236000},"source":"Crossref","is-referenced-by-count":0,"title":["Intuitionistic S4 as a logic of topological spaces"],"prefix":"10.1093","volume":"35","author":[{"given":"Jim","family":"de Groot","sequence":"first","affiliation":[{"name":"The Australian National University , Canberra, Ngunnawal & Ngambri Country, 2600, Australia"}]},{"given":"Ian","family":"Shillito","sequence":"additional","affiliation":[{"name":"The Australian National University , Canberra, Ngunnawal & Ngambri Country, 2600, Australia"}]}],"member":"286","published-online":{"date-parts":[[2024,8,6]]},"reference":[{"year":"2024","author":"Balbiani","article-title":"Constructive S4 modal logics with the finite birelational frame property","key":"2025091917100627900_ref1"},{"key":"2025091917100627900_ref2","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1093\/logcom\/2.1.31","article-title":"A constructive presentation for the modal connective of necessity","volume":"2","author":"Benevides","year":"1992","journal-title":"Journal of Logic and Computation"},{"year":"2006","author":"Bezhanishvili","article-title":"Intuitionistic logic","key":"2025091917100627900_ref3"},{"key":"2025091917100627900_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"},{"volume-title":"Intuitionistic Necessity Revisited","year":"1996","author":"Bierman","key":"2025091917100627900_ref5"},{"key":"2025091917100627900_ref6","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1017\/S0960129519000197","article-title":"Modal dependent type theory and dependent right adjoints","volume":"30","author":"Birkedal","year":"2020","journal-title":"Mathematical Structures in Computer Science"},{"key":"2025091917100627900_ref7","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"Blackburn","year":"2001"},{"volume-title":"Varieties of Interior Algebras","year":"1976","author":"Blok","key":"2025091917100627900_ref8"},{"key":"2025091917100627900_ref9","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0049-237X(08)71680-X","article-title":"Some modal calculi based on IC","volume-title":"Formal Systems and Recursive Functions","author":"Bull","year":"1965"},{"key":"2025091917100627900_ref10","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198537793.001.0001","volume-title":"Modal Logic","author":"Chagrov","year":"1997"},{"key":"2025091917100627900_ref11","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511621192","volume-title":"Modal Logic: An Introduction","author":"Chellas","year":"1980"},{"key":"2025091917100627900_ref12","first-page":"258","article-title":"Fitch-style modal lambda calculi","volume-title":"Proc. FoSSaCS 2018","author":"Clouston","year":"2018"},{"key":"2025091917100627900_ref13","article-title":"The guarded lambda-calculus: programming and reasoning with guarded recursion for coinductive types","volume":"12","author":"Clouston","year":"2017","journal-title":"Logical Methods in Computer Science"},{"key":"2025091917100627900_ref14","first-page":"171","article-title":"Modal logic S4 as a paraconsistent logic with a topological semantics","volume-title":"Logic and Computation: Essays in Honour of Amilcar Sernadas","author":"Coniglio","year":"2017"},{"key":"2025091917100627900_ref15","doi-asserted-by":"crossref","first-page":"833","DOI":"10.1007\/s10992-019-09539-3","article-title":"Intuitionistic non-normal modal logics: a general framework","volume":"49","author":"Dalmonte","year":"2020","journal-title":"Journal of Philosophical Logic"},{"key":"2025091917100627900_ref16","first-page":"283","article-title":"On intuitionistic diamonds (and lack thereof)","volume-title":"Proc. TABLEAUX 2023","author":"Das","year":"2023"},{"key":"2025091917100627900_ref17","first-page":"258","article-title":"A modal analysis of staged computation","volume-title":"Proc SIGPLAN 1996","author":"Davies","year":"1996"},{"key":"2025091917100627900_ref18","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1145\/382780.382785","article-title":"A modal analysis of staged computation","volume":"48","author":"Davies","year":"2001","journal-title":"Journal of the ACM"},{"key":"2025091917100627900_ref19","first-page":"162","article-title":"Topological semantics and bisimulations for intuitionistic modal logics and their classical companion logics","volume-title":"Proc. LFCS 2007","author":"Davoren","year":"2007"},{"key":"2025091917100627900_ref20","article-title":"Topological semantics for intuitionistic modal logics, and spatial discretisation by A\/D maps","volume-title":"Workshop on Intuitionistic Modal Logic and Applications (IMLA), Copenhagen, Denmark (2002)","author":"Davoren","year":"2002"},{"key":"2025091917100627900_ref21","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF00370809","article-title":"Models for stronger normal intuitionistic modal logics","volume":"44","author":"Do\u0161en","year":"1985","journal-title":"Studia Logica"},{"key":"2025091917100627900_ref22","first-page":"257","article-title":"On varieties of Grzegorczyk algebras","volume-title":"Studies in Non-Classical Logics and Set Theory","author":"Esakia","year":"1979"},{"key":"2025091917100627900_ref23","first-page":"128","article-title":"Diagonal constructions, L\u00f6b\u2019s formula and Cantor\u2019s scattered space","volume":"132","author":"Esakia","year":"1981","journal-title":"Studies in Logic and Semantics"},{"key":"2025091917100627900_ref24","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-030-12096-2","volume-title":"Heyting Algebras. Trends in Logic","author":"Esakia","year":"2019"},{"key":"2025091917100627900_ref25","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1093\/logcom\/exs053","article-title":"Terminating sequent calculi for proving and refuting formulas in S4","volume":"25","author":"Fiorentini","year":"2012","journal-title":"Journal of Logic and Computation"},{"key":"2025091917100627900_ref26","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/978-94-009-8937-5_5","article-title":"Semantics for a class of intuitionistic modal calculi","volume-title":"Italian Studies in the Philosophy of Science","author":"Fischer Servi","year":"1980"},{"key":"2025091917100627900_ref27","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1305\/ndjfl\/1093636766","article-title":"Modality and possibility in some intuitionistic modal logics","volume":"27","author":"Font","year":"1986","journal-title":"Notre Dame Journal of Formal Logic"},{"volume-title":"Abstract Algebraic Logic: An Introductory Textbook","year":"2016","author":"Font","key":"2025091917100627900_ref28"},{"volume-title":"Modal Definability in Topology","year":"2001","author":"Gabelaia","key":"2025091917100627900_ref29"},{"key":"2025091917100627900_ref30","first-page":"1","article-title":"Intuitionistic S4 is decidable","volume":"2023","author":"Girlando","year":"2023","journal-title":"Proc. LICS"},{"key":"2025091917100627900_ref31","first-page":"34","article-title":"Eine interpretation des intuitionistischen aussagenkalk\u00fclus","volume":"4","author":"G\u00f6del","year":"1933","journal-title":"Ergebnisse eines Mathematischen Kolloquiums"},{"volume-title":"Mathematics of Modality","year":"1993","author":"Goldblatt","key":"2025091917100627900_ref32"},{"key":"2025091917100627900_ref33","first-page":"269","article-title":"Bi-intuitionistic logics: a new instance of an old problem","volume-title":"Proc. AIML 2020","author":"Gor\u00e9","year":"2020"},{"volume-title":"Fischer Servi\u2019s Intuitionistic Modal Logic and Its Extensions","year":"1999","author":"Grefe","key":"2025091917100627900_ref34"},{"key":"2025091917100627900_ref35","doi-asserted-by":"crossref","first-page":"223","DOI":"10.4064\/fm-60-3-223-231","article-title":"Some relational systems and the associated topological spaces","volume":"60","author":"Grzegorczyk","year":"1967","journal-title":"Fundamenta Mathematicae"},{"key":"2025091917100627900_ref36","doi-asserted-by":"crossref","first-page":"849","DOI":"10.1007\/s11229-011-9905-9","article-title":"Does the deduction theorem fail for modal logic","volume":"187","author":"Hakli","year":"2012","journal-title":"Synthese"},{"volume-title":"Monotonic Modal Logics","year":"2003","author":"Hansen","key":"2025091917100627900_ref37"},{"key":"2025091917100627900_ref38","first-page":"655","article-title":"Temporal logic","volume-title":"Handbook of Modal Logic, Volume 3 (Studies in Logic and Practical Reasoning)","author":"Hodkinson","year":"2007"},{"key":"2025091917100627900_ref39","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-94-017-2798-3_1","article-title":"A contraction-free sequent calculus for S4","volume-title":"Proof Theory of Modal Logic","author":"Hudelmaier","year":"1996"},{"key":"2025091917100627900_ref40","doi-asserted-by":"crossref","first-page":"891","DOI":"10.2307\/2372123","article-title":"Boolean algebras with operators. Part I","volume":"73","author":"J\u00f3nsson","year":"1951","journal-title":"American Journal of Mathematics"},{"volume-title":"Tools and Techniques in Modal Logic","year":"1999","author":"Kracht","key":"2025091917100627900_ref41"},{"key":"2025091917100627900_ref42","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1002\/malq.19630090502","article-title":"Semantic analysis of modal logic I, normal propositional calculi","volume":"9","author":"Kripke","year":"1963","journal-title":"Zeitschrift f\u00fcr Mathemathische Logik und Grundlagen der Mathematik"},{"volume-title":"Symbolic Logic","year":"1932","author":"Lewis","key":"2025091917100627900_ref43"},{"key":"2025091917100627900_ref44","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1093\/logcom\/3.5.533","article-title":"2-sequent calculus: intuitionism and natural deduction","volume":"3","author":"Masini","year":"1993","journal-title":"Journal of Logic and Computation"},{"key":"2025091917100627900_ref45","doi-asserted-by":"crossref","first-page":"141","DOI":"10.2307\/1969080","article-title":"The algebra of topology","volume":"45","author":"McKinsey","year":"1944","journal-title":"Annals of Mathematics"},{"key":"2025091917100627900_ref46","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2268135","article-title":"Some theorems about the sentential calculi of Lewis and Heyting","volume":"13","author":"McKinsey","year":"1948","journal-title":"The Journal of Symbolic Logic"},{"key":"2025091917100627900_ref47","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1111\/j.1755-2567.1970.tb00434.x","article-title":"Universal grammar","volume":"36","author":"Montague","year":"1970","journal-title":"Theoria"},{"year":"2020","author":"M\u00fcger","article-title":"Topology for the Working Mathematician","key":"2025091917100627900_ref48"},{"volume-title":"Constructive Mathematical Logic From the Point of View of Classical Logic","year":"1977","author":"Novikov","key":"2025091917100627900_ref49"},{"key":"2025091917100627900_ref50","first-page":"113","article-title":"Gentzen method in modal calculi","volume":"9","author":"Ohnishi","year":"1957","journal-title":"Osaka Mathematical Journal"},{"key":"2025091917100627900_ref51","doi-asserted-by":"crossref","first-page":"687","DOI":"10.2977\/prims\/1195189604","article-title":"On some intuitionistic modal logics","volume":"13","author":"Ono","year":"1977","journal-title":"Publications of the Research Institute for Mathematical Sciences"},{"key":"2025091917100627900_ref52","first-page":"263","article-title":"The calculus of compatibility of propositions","volume":"35","author":"Orlov","year":"1928","journal-title":"Mathematics of the USSR"},{"key":"2025091917100627900_ref53","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-67149-9","volume-title":"Neighborhood Semantics for Modal Logic","author":"Pacuit","year":"2017"},{"key":"2025091917100627900_ref54","first-page":"399","article-title":"A framework for intuitionistic modal logics: extended abstract","volume-title":"Proc. TARK 1986","author":"Plotkin","year":"1986"},{"volume-title":"Natural Deduction\u2014A Proof Theoretical Study","year":"1965","author":"Prawitz","key":"2025091917100627900_ref55"},{"volume-title":"The Mathematics of Metamathematics. Monografie Matematyczne, Tom 41","year":"1963","author":"Rasiowa","key":"2025091917100627900_ref56"},{"key":"2025091917100627900_ref57","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/978-94-010-3272-8_7","article-title":"Advice on modal logic","volume-title":"Philosophical Problems in Logic","author":"Scott","year":"1970"},{"volume-title":"New Foundations for the Proof Theory of Bi-Intuitionistic and Provability Logics Mechanized in Coq","year":"2023","author":"Shillito","key":"2025091917100627900_ref58"},{"key":"2025091917100627900_ref59","first-page":"218","article-title":"A mechanised and constructive reverse analysis of soundness and completeness of bi-intuitionistic logic","volume-title":"Proc. CPP 2024","author":"Shillito","year":"2024"},{"volume-title":"The Proof Theory and Semantics of Intuitionistic Modal Logic","year":"1994","author":"Simpson","key":"2025091917100627900_ref60"},{"key":"2025091917100627900_ref61","doi-asserted-by":"crossref","first-page":"1","DOI":"10.21136\/CPMF.1938.124080","article-title":"Topological representations of distributive lattices and Brouwerian logics","volume":"067","author":"Stone","year":"1938","journal-title":"\u010casopis pro P\u011bstov\u00e1n\u00ed Matematiky a Fysiky"},{"key":"2025091917100627900_ref62","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1090\/dimacs\/031\/05","article-title":"Why is modal logic so robustly decidable","volume":"31","author":"Vardi","year":"1996","journal-title":"Descriptive Complexity and Finite Models"},{"key":"2025091917100627900_ref63","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/978-94-010-0387-2_2","article-title":"Sequent systems for modal logics","volume-title":"Handbook of Philosophical Logic: Volume 8","author":"Wansing","year":"2002"},{"key":"2025091917100627900_ref64","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"},{"volume-title":"General Topology","year":"2004","author":"Willard","key":"2025091917100627900_ref65"},{"key":"2025091917100627900_ref66","doi-asserted-by":"crossref","first-page":"187","DOI":"10.18778\/0138-0680.48.3.03","article-title":"Topological and multi-topological frames in the context of intuitionistic modal jogic","volume":"48","author":"Witczak","year":"2019","journal-title":"Bulletin of the Section of Logic"},{"key":"2025091917100627900_ref67","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-6942-2","volume-title":"Theory of Logical Calculi: Basic Theory of Consequence Operations","author":"W\u00f3jcicki","year":"1988"},{"key":"2025091917100627900_ref68","first-page":"168","article-title":"Intuitionistic modal logics as fragments of classical bimodal logics","volume-title":"Logic at Work, Essays in Honour of Helena Rasiowa","author":"Wolter","year":"1998"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/7\/exae030\/58740808\/exae030.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/7\/exae030\/58740808\/exae030.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T21:10:20Z","timestamp":1758316220000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/doi\/10.1093\/logcom\/exae030\/7713389"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,6]]},"references-count":68,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2025,9,11]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exae030","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2025,10]]},"published":{"date-parts":[[2024,8,6]]},"article-number":"exae030"}}