{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T01:02:13Z","timestamp":1779757333761,"version":"3.53.1"},"reference-count":23,"publisher":"Oxford University Press (OUP)","issue":"3","license":[{"start":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T00:00:00Z","timestamp":1778630400000},"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":[[2026,5,26]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>In this paper we present a tableau proof system for basic hybrid logic extended with quantification over basic modal propositions, and prove its completeness with respect to general models. This paper is largely devoted to the technical details of the proof, but we also discuss the link with the philosophical work of Arthur Prior, which led us to this system in the first place.<\/jats:p>","DOI":"10.1093\/jigpal\/jzag022","type":"journal-article","created":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T11:15:10Z","timestamp":1776510910000},"source":"Crossref","is-referenced-by-count":0,"title":["A complete tableau system for basic hybrid logic with propositional quantification"],"prefix":"10.1093","volume":"34","author":[{"given":"Julie","family":"Lundbak Kofod","sequence":"first","affiliation":[{"name":"Department of Communication and Arts , Roskilde University, 4000 Roskilde, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Patrick","family":"Blackburn","sequence":"additional","affiliation":[{"name":"Department of Communication and Arts , Roskilde University, 4000 Roskilde, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Torben","family":"Bra\u00fcner","sequence":"additional","affiliation":[{"name":"Department of People and Technology , Roskilde University, 4000 Roskilde, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"286","published-online":{"date-parts":[[2026,5,13]]},"reference":[{"key":"2026052520023863500_ref1","volume-title":"Methods of Cut-Elimination, volume 34 of Trends in Logic Series","author":"Baaz","year":"2011"},{"key":"2026052520023863500_ref2","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1093\/logcom\/10.1.137","article-title":"Internalizing labelled deduction","volume":"10","author":"Blackburn","year":"2000","journal-title":"J Log Comput"},{"key":"2026052520023863500_ref3","first-page":"401","article-title":"Remarks on hybrid modal logic with propositional quantfiers","volume-title":"The Metaphysics of Time: Themes from Prior, volume 4 of Logic and Philosophy of Time","author":"Blackburn","year":"2020"},{"key":"2026052520023863500_ref4","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/978-3-031-39784-4_8","article-title":"An axiom system for basic hybrid logic with propositional quantifiers","volume-title":"International Workshop on Logic, Language, Information, and Computation","author":"Blackburn","year":"2023"},{"key":"2026052520023863500_ref5","article-title":"This time as grandfather","volume-title":"Proceedings of AWPL 2024, Studia Logica Library","author":"Blackburn","year":"2024"},{"key":"2026052520023863500_ref6","doi-asserted-by":"publisher","first-page":"e7","DOI":"10.1017\/S0960129525000076","article-title":"Prior\u2019s ideal language","volume":"35","author":"Blackburn","year":"2025","journal-title":"Math Struct Comput Sci"},{"key":"2026052520023863500_ref7","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"Blackburn","year":"2001"},{"key":"2026052520023863500_ref8","article-title":"Hybrid logic and its proof-theory","volume-title":"Applied Logic Series","author":"Bra\u00fcner","year":"2011"},{"key":"2026052520023863500_ref9","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1111\/j.1755-2567.1970.tb00432.x","article-title":"Propositional quantifiers in modal logic","volume":"36","author":"Fine","year":"1970","journal-title":"Theoria"},{"key":"2026052520023863500_ref10","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1111\/j.1755-2567.1974.tb00076.x","article-title":"An incomplete logic containing $S4$","volume":"40","author":"Fine","year":"1974","journal-title":"Theoria"},{"key":"2026052520023863500_ref11","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logic","author":"Fitting","year":"1983"},{"key":"2026052520023863500_ref12","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538332.001.0001","volume-title":"Labelled Deductive Systems","author":"Gabbay","year":"1996"},{"key":"2026052520023863500_ref13","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266967","article-title":"Completeness in the theory of types","volume":"15","author":"Henkin","year":"1950","journal-title":"J Symb Log"},{"key":"2026052520023863500_ref14","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1305\/ndjfl\/1040067314","article-title":"The expressive power of second-order propositional modal logic","volume":"37","author":"Kaminski","year":"1996","journal-title":"Notre Dame J Form Log"},{"key":"2026052520023863500_ref15","volume-title":"Provability in Logic","author":"Kanger","year":"1957"},{"key":"2026052520023863500_ref16","doi-asserted-by":"publisher","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":"2026052520023863500_ref17","volume-title":"Papers on Time and Tense","author":"Prior","year":"1968"},{"key":"2026052520023863500_ref18","volume-title":"Worlds, Times, and Selves","author":"Prior","year":"1977"},{"key":"2026052520023863500_ref19","volume-title":"Papers on Time and Tense","author":"Prior","year":"2003"},{"key":"2026052520023863500_ref20","article-title":"The proof theory and semantics of intuitionistic modal logic","author":"Simpson","year":"1994"},{"key":"2026052520023863500_ref21","doi-asserted-by":"publisher","first-page":"150","DOI":"10.2307\/2272558","article-title":"Semantic analysis of tense logics","volume":"37","author":"Thomason","year":"1972","journal-title":"J Symb Log"},{"key":"2026052520023863500_ref22","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-4558-5","volume-title":"Logic and Structure","author":"Van Dalen","year":"2013"},{"key":"2026052520023863500_ref23","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1023\/A:1005217827758","article-title":"The idea of a proof-theoretic semantics and the meaning of the logical operations","volume":"64","author":"Wansing","year":"2000","journal-title":"Stud Log"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/34\/3\/jzag022\/68282208\/jzag022.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/34\/3\/jzag022\/68282208\/jzag022.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T00:02:44Z","timestamp":1779753764000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/doi\/10.1093\/jigpal\/jzag022\/8677803"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,5,13]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2026,5,26]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzag022","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"value":"1367-0751","type":"print"},{"value":"1368-9894","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2026,6]]},"published":{"date-parts":[[2026,5,13]]},"article-number":"jzag022"}}