{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T22:16:33Z","timestamp":1757542593301},"reference-count":28,"publisher":"Oxford University Press (OUP)","issue":"3","license":[{"start":{"date-parts":[[2021,4,14]],"date-time":"2021-04-14T00:00:00Z","timestamp":1618358400000},"content-version":"vor","delay-in-days":13,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,4,16]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce labelled sequent calculi for quantified modal logics with definite descriptions. We prove that these calculi have the good structural properties of G3-style calculi. In particular, all rules are height-preserving invertible, weakening and contraction are height-preserving admissible and cut is syntactically admissible. Finally, we show that each calculus gives a proof-theoretic characterization of validity in the corresponding class of models.<\/jats:p>","DOI":"10.1093\/logcom\/exab018","type":"journal-article","created":{"date-parts":[[2021,3,31]],"date-time":"2021-03-31T15:14:38Z","timestamp":1617203678000},"page":"923-946","source":"Crossref","is-referenced-by-count":12,"title":["Labelled calculi for quantified modal logics with definite descriptions"],"prefix":"10.1093","volume":"31","author":[{"given":"Eugenio","family":"Orlandelli","sequence":"first","affiliation":[{"name":"Department of Philosophy and Communication Studies , University of Bologna, via Zamboni 38, Bologna, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2021,4,14]]},"reference":[{"key":"2023031406060497100_","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/s11225-006-6603-6","article-title":"Gentzen calculi for the existence predicate","volume":"82","author":"Baaz","year":"2006","journal-title":"Studia Logica"},{"key":"2023031406060497100_","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":"2023031406060497100_","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-45744-5_11","article-title":"Free-variable tableaux for constant-domain quantified modal logics with rigid and non-rigid designation","volume-title":"Automated Reasoning: Proceedings of the First International Joint Conference, IJCAR 2001","author":"Cerrito","year":"2001"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","first-page":"11:1","DOI":"10.1145\/3180075","article-title":"Hypersequents and systems of rules: embeddings and applications","volume":"19","author":"Ciabattoni","year":"2018","journal-title":"ACM Transactions on Computational Logic"},{"key":"2023031406060497100_","first-page":"120","article-title":"From display to labelled proofs for tense logics","volume-title":"Logical Foundations of Computer Science, International Symposium, LFCS 2018","author":"Ciabattoni","year":"2018"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","first-page":"1245","DOI":"10.1007\/s11225-014-9566-z","article-title":"Hypersequent and display calculi: a unified perspective","volume":"102","author":"Ciabattoni","year":"2014","journal-title":"Studia Logica"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1023\/A:1013838528631","article-title":"Ground and free-variable tableaux for variants of quantified modal logics","volume":"69","author":"Mayer","year":"2001","journal-title":"Studia Logica"},{"key":"2023031406060497100_","first-page":"21","article-title":"Sequent calculi for indexed epistemic logics","volume-title":"Proceedings of the 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016)","author":"Corsi","year":"2016"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/BF01048353","article-title":"Incompleteness and the Barcan formula","volume":"24","author":"Cresswell","year":"1995","journal-title":"Journal of Philosophical Logic"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1017\/bsl.2015.7","article-title":"Geometrisation of first-order logic","volume":"21","author":"Dyckhoff","year":"2015","journal-title":"Bulletin of Symbolic Logic"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-011-5292-1","volume-title":"First-order Modal Logic","author":"Fitting","year":"1998"},{"key":"2023031406060497100_","first-page":"25","article-title":"\u00dcber sinn und bedeutung","volume":"100","author":"Frege","year":"1892","journal-title":"Zeitschrift f\u00fcr Philosophie Und Philosophische Kritik"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139342117","volume-title":"Modal Logic for Philosophers","author":"Garson","year":"2013"},{"key":"2023031406060497100_","first-page":"387","article-title":"Cut-free modal theory of definite descriptions","volume-title":"Advances in Modal Logic","author":"Indrzejczak","year":"2018"},{"key":"2023031406060497100_","first-page":"137","article-title":"Fregean description theory in proof-theoretical setting","volume":"28","author":"Indrzejczak","year":"2019","journal-title":"Logic and Logical Philosophy"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","first-page":"137","DOI":"10.18778\/0138-0680.48.2.04","article-title":"Full cut elimination and interpolation for intuitionistic logic with existence predicate","volume":"48","author":"Maffezioli","year":"2019","journal-title":"Bulletin of the Section of Logic"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/BF01977152","article-title":"Remarks on descriptions and natural deduction","volume":"3","author":"Montague","year":"1957","journal-title":"Archiv f\u00fcr Mathematische Logik und Grundlagenforschung"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/s001530100124","article-title":"Contraction-free sequent calculi for geometric theories with an application to Barr\u2019s theorem","volume":"42","author":"Negri","year":"2003","journal-title":"Archive for Mathematical Logic"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1093\/jigpal\/jzz015","article-title":"Proof theory for quantified monotone modal logics","volume":"27","author":"Negri","year":"2019","journal-title":"Logic Journal of the IGPL"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","first-page":"418","DOI":"10.2307\/420956","article-title":"Cut elimination in the presence of axioms","volume":"4","author":"Negri","year":"1998","journal-title":"Bulletin of Symbolic Logic"},{"key":"2023031406060497100_","article-title":"Cambridge University Press","volume-title":"Proof Analysis","author":"Negri","year":"2011"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-030-01713-2_11","article-title":"Decidable term-modal logics","volume-title":"Multi-agent Systems and Agreement Technologies","author":"Orlandelli","year":"2018"},{"key":"2023031406060497100_","first-page":"64","article-title":"Labelled calculi for quantified modal logics with non-rigid and non-denoting terms","volume-title":"Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018)","author":"Orlandelli","year":"2018"},{"key":"2023031406060497100_","first-page":"1","article-title":"From axioms to structural rules, then add the quantifiers","volume-title":"Proceedings of the 2nd International Workshop on Automated Reasoning in Quantified Non-classical Logics (ARQNL 2016)","author":"Ramanayake","year":"2016"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1093\/mind\/XIV.4.479","article-title":"On denoting","volume":"14","author":"Russell","year":"1905","journal-title":"Mind"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","first-page":"31","DOI":"10.2307\/2268137","article-title":"Modality and description","volume":"13","author":"Smullyan","year":"1948","journal-title":"Journal of Symbolic Logic"},{"key":"2023031406060497100_","volume-title":"Basic Proof Theory","author":"Troelstra","year":"1996"},{"key":"2023031406060497100_","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3208-5","volume-title":"Labelled Non-classical Logic","author":"Vigan\u00f2","year":"2000"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/31\/3\/923\/49518293\/exab018.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/31\/3\/923\/49518293\/exab018.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,1]],"date-time":"2023-11-01T08:05:05Z","timestamp":1698825905000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/31\/3\/923\/6224159"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4]]},"references-count":28,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2021,4,14]]},"published-print":{"date-parts":[[2021,4,16]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exab018","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]]}}}