{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T21:38:24Z","timestamp":1768253904608,"version":"3.49.0"},"reference-count":27,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2022,8,12]],"date-time":"2022-08-12T00:00:00Z","timestamp":1660262400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["The Review of Symbolic Logic"],"published-print":{"date-parts":[[2024,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this article we show that bi-intuitionistic predicate logic lacks the Craig Interpolation Property. We proceed by adapting the counterexample given by Mints, Olkhovikov and Urquhart for intuitionistic predicate logic with constant domains [13]. More precisely, we show that there is a valid implication <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S1755020322000296_inline1.png\"\/><jats:tex-math>\n$\\phi \\rightarrow \\psi $\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> with no interpolant. Importantly, this result does not contradict the unfortunately named \u2018Craig interpolation\u2019 theorem established by Rauszer in [24] since that article is about the property more correctly named \u2018deductive interpolation\u2019 (see Galatos, Jipsen, Kowalski and Ono\u2019s use of this term in [5]) for global consequence. Given that the deduction theorem fails for bi-intuitionistic logic with global consequence, the two formulations of the property are not equivalent.<\/jats:p>","DOI":"10.1017\/s1755020322000296","type":"journal-article","created":{"date-parts":[[2022,8,12]],"date-time":"2022-08-12T07:33:27Z","timestamp":1660289607000},"page":"611-633","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["CRAIG INTERPOLATION THEOREM FAILS IN BI-INTUITIONISTIC PREDICATE LOGIC"],"prefix":"10.1017","volume":"17","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7773-5038","authenticated-orcid":false,"given":"GRIGORY K.","family":"OLKHOVIKOV","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5597-6794","authenticated-orcid":false,"given":"GUILLERMO","family":"BADIA","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2022,8,12]]},"reference":[{"key":"S1755020322000296_r14","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exab058"},{"key":"S1755020322000296_r5","volume-title":"Residuated Lattices: An Algebraic Glimpse at Substructural Logics","author":"Galatos","year":"2007"},{"key":"S1755020322000296_r25","unstructured":"[24] Restall, G. (1997). Extending intuitionistic logic with subtraction. Available from: http:\/\/consequently.org\/writing\/."},{"key":"S1755020322000296_r6","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn067"},{"key":"S1755020322000296_r3","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00124-3"},{"key":"S1755020322000296_r15","doi-asserted-by":"publisher","DOI":"10.1017\/S1755020312000342"},{"key":"S1755020322000296_r8","doi-asserted-by":"publisher","DOI":"10.1007\/BF01991851"},{"key":"S1755020322000296_r22","doi-asserted-by":"publisher","DOI":"10.1007\/BF02121115"},{"key":"S1755020322000296_r28","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2017.12.001"},{"key":"S1755020322000296_r9","doi-asserted-by":"publisher","DOI":"10.1017\/S175502031600040X"},{"key":"S1755020322000296_r11","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/7.4.501"},{"key":"S1755020322000296_r12","first-page":"117","article-title":"On intuitionistic sentential connectives I","volume":"XIX","author":"L\u00f3pez-Escobar","year":"1985","journal-title":"Revista Colombiana de Matem\u00e1ticas"},{"key":"S1755020322000296_r13","doi-asserted-by":"publisher","DOI":"10.2178\/jsl.7803120"},{"key":"S1755020322000296_r2","doi-asserted-by":"publisher","DOI":"10.26686\/ajl.v14i1.4027"},{"key":"S1755020322000296_r4","volume-title":"Logic, Language, Information, and Computation. WoLLIC 2019","author":"de Groot","year":"2019"},{"key":"S1755020322000296_r7","first-page":"269","article-title":"Bi-intuitionistic logics: A new instance of an old problem","volume":"13","author":"Gor\u00e9","year":"2020","journal-title":"Advances in Modal Logic"},{"key":"S1755020322000296_r16","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/ext014"},{"key":"S1755020322000296_r20","doi-asserted-by":"publisher","DOI":"10.4064\/fm-83-3-219-249"},{"key":"S1755020322000296_r1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-016-9664-1"},{"key":"S1755020322000296_r21","doi-asserted-by":"publisher","DOI":"10.1007\/BF02120864"},{"key":"S1755020322000296_r18","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exx044"},{"key":"S1755020322000296_r24","volume-title":"An Algebraic and Kripke-Style Approach to a Certain Extension of Intuitionistic Logic","author":"Rauszer","year":"1980"},{"key":"S1755020322000296_r26","unstructured":"[25] Shillito, I. (n.d.). First-order bi-intuitionistic logics: From shaky to formally verified foundations, preprint."},{"key":"S1755020322000296_r27","doi-asserted-by":"publisher","DOI":"10.1080\/11663081.2018.1448636"},{"key":"S1755020322000296_r19","first-page":"881","article-title":"Representation theorem for semi-Boolean algebras. I, II.","volume":"19","author":"Rauszer","year":"1971","journal-title":"Bulletin L\u2019Acad\u00e9mie Polonaise des Science, S\u00e9rie des Sciences Math\u00e9matiques, Astronomiques et Physiques"},{"key":"S1755020322000296_r23","doi-asserted-by":"publisher","DOI":"10.1007\/BF02121116"},{"key":"S1755020322000296_r17","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2017.03.002"}],"container-title":["The Review of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1755020322000296","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T13:20:21Z","timestamp":1716816021000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1755020322000296\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,12]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["S1755020322000296"],"URL":"https:\/\/doi.org\/10.1017\/s1755020322000296","relation":{},"ISSN":["1755-0203","1755-0211"],"issn-type":[{"value":"1755-0203","type":"print"},{"value":"1755-0211","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,12]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press on behalf of The Association for Symbolic Logic","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}