{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T20:13:58Z","timestamp":1758053638208,"version":"3.44.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032041661","type":"print"},{"value":"9783032041678","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"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>One of the most fascinating examples of the failure of Beth\u2019s definability theorem and, consequently, of Craig\u2019s interpolation theorem, is quantified S5. In this paper, we intend to establish the interpolation property for fragments of quantified S5 using a formulation of the semantics of quantified S5 as an analytic calculus in its own right. This is especially straightforward for S5, because necessity (possibility) in S5 means for all worlds (there exists a world), and we have simply to extend every predicate by a world position (worlds and objects are to be considered as separate entities).<\/jats:p>","DOI":"10.1007\/978-3-032-04167-8_4","type":"book-chapter","created":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:24Z","timestamp":1757887404000},"page":"63-79","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An Analytic Representation of\u00a0the\u00a0Semantics of\u00a0First-Order S5"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7815-2501","authenticated-orcid":false,"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-0468-9945","authenticated-orcid":false,"given":"Mariami","family":"Gamsakhurdia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4753-7302","authenticated-orcid":false,"given":"Anela","family":"Loli\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"issue":"2","key":"4_CR1","first-page":"146","volume":"30","author":"H Barkan","year":"1964","unstructured":"Barkan, H.: On the interpretation of modal logic. Theoria 30(2), 146\u2013153 (1964)","journal-title":"Theoria"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Blackburn, P., van Benthem, J.: Modal logic: a semantic perspective. In: Handbook of Modal Logic, vol.\u00a03, chap.\u00a01. Elsevier (2007)","DOI":"10.1016\/S1570-2464(07)80004-8"},{"key":"4_CR3","unstructured":"Bra\u00fcner, T., Ghilardi, S.: Modal logic: a semantic perspective. In: Handbook of Modal Logic, vol.\u00a03, chap.\u00a09. Elsevier (2007)"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Ciabattoni, A., Galatos, N., Terui, K.: From axioms to analytic rules in nonclassical logics. In: Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, Pittsburgh, PA, USA, 24\u201327 June 2008. pp. 229\u2013240. IEEE Computer Society (2008). https:\/\/doi.org\/10.1109\/LICS.2008.39","DOI":"10.1109\/LICS.2008.39"},{"issue":"3","key":"4_CR5","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1016\/j.apal.2011.09.003","volume":"163","author":"A Ciabattoni","year":"2009","unstructured":"Ciabattoni, A., Galatos, N., Terui, K.: Algebraic proof theory for substructural logics: cut-elimination and analyticity. Ann. Pure Appl. Logic 163(3), 266\u2013290 (2009)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"03","key":"4_CR6","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Logic 22(03), 269\u2013285 (1957)","journal-title":"J. Symb. Logic"},{"issue":"2","key":"4_CR7","doi-asserted-by":"publisher","first-page":"201","DOI":"10.2307\/2273727","volume":"44","author":"K Fine","year":"1979","unstructured":"Fine, K.: Failures of the interpolation lemma in quantified modal logic. J. Symb. Logic 44(2), 201\u2013206 (1979)","journal-title":"J. Symb. Logic"},{"key":"4_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-5292-1","volume-title":"First-Order Modal Logic, Synthese Library","author":"M Fitting","year":"1998","unstructured":"Fitting, M., Mendelsohn, R.L.: First-Order Modal Logic, Synthese Library, vol. 277. Springer, Cham (1998)"},{"issue":"1","key":"4_CR9","first-page":"95","volume":"36","author":"J Flum","year":"1990","unstructured":"Flum, J., Ziegler, M.: Interpolation theorems for fragments of first-order modal logic. Math. Log. Q. 36(1), 95\u2013104 (1990)","journal-title":"Math. Log. Q."},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Friedman, H.: The complexity of explicit definitions. Adv. Math. 20(1), 18\u201329 (1976). https:\/\/doi.org\/10.1016\/0001-8708(76)90167-5. https:\/\/www.sciencedirect.com\/science\/article\/pii\/0001870876901675","DOI":"10.1016\/0001-8708(76)90167-5"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Gabbay, D.M.: Semantical investigations in heyting\u2019s intuitionistic logic. In: Synthese Library. Springer, Cham (1981), chapter on interpolation failures","DOI":"10.1007\/978-94-017-2977-2"},{"key":"4_CR12","volume-title":"Grundlagen der mathematik","author":"D Hilbert","year":"1934","unstructured":"Hilbert, D., Bernays, P.: Grundlagen der mathematik. Springer, Cham (1934)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Hughes, G.E., Cresswell, M.J.: A New Introduction to Modal Logic. Routledge (1996)","DOI":"10.4324\/9780203290644"},{"key":"4_CR14","unstructured":"Jergitsch, C.: Interpolation by translation. Master\u2019s thesis, TU Wien, Vienna, Austria (2023). http:\/\/hdl.handle.net\/20.500.12708\/176748"},{"issue":"1\u20133","key":"4_CR15","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/S0168-0072(99)00049-4","volume":"105","author":"L Maksimova","year":"2000","unstructured":"Maksimova, L.: Intuitionistic logic and implicit definability. Ann. Pure Appl. Logic 105(1\u20133), 83\u2013102 (2000)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"6","key":"4_CR16","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/BF01670006","volume":"16","author":"LL Maksimova","year":"1977","unstructured":"Maksimova, L.L.: Craig\u2019s theorem in superintuitionistic logics and amalgamable varieties of pseudo-Boolean algebras. Algebra Logic 16(6), 427\u2013455 (1977)","journal-title":"Algebra Logic"},{"issue":"4","key":"4_CR17","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/BF00370479","volume":"38","author":"LL Maksimova","year":"1979","unstructured":"Maksimova, L.L.: Interpolation properties of superintuitionistic logics. Stud. Logica. 38(4), 419\u2013428 (1979)","journal-title":"Stud. Logica."},{"key":"4_CR18","unstructured":"Steinacker, P.: Modallogik. In: Nichtklassische Logik - eine Einf\u00fchrung, chap.\u00a03. Akademie-Verlag, Berlin (1988)"},{"key":"4_CR19","unstructured":"Sturm, H., Wolter, F.: First-order expressivity for s5-models: modal vs. two-sorted languages. J. Philos. Logic 44(2), 201\u2013206 (2000)"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Takeuti, G.: Proof theory. Studies in Logic and the Foundations of Mathematics, 2nd edn. North-Holland (1987). https:\/\/doi.org\/10.1016\/S0049-237X(08)70603-7. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0049237X08706037","DOI":"10.1016\/S0049-237X(08)70603-7"},{"issue":"11","key":"4_CR21","doi-asserted-by":"publisher","first-page":"2021","DOI":"10.1109\/JPROC.2015.2455034","volume":"103","author":"Y Vizel","year":"2015","unstructured":"Vizel, Y., Weissenbacher, G., Malik, S.: Boolean satisfiability solvers and their applications in model checking. Proc. IEEE 103(11), 2021\u20132035 (2015)","journal-title":"Proc. IEEE"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04167-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:26Z","timestamp":1757887406000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04167-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"ISBN":["9783032041661","9783032041678"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04167-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,15]]},"assertion":[{"value":"15 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","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":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/frocos\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}