{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:12:30Z","timestamp":1776888750133,"version":"3.51.2"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2023,1,31]],"date-time":"2023-01-31T00:00:00Z","timestamp":1675123200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,1,31]],"date-time":"2023-01-31T00:00:00Z","timestamp":1675123200000},"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":["Stud Logica"],"published-print":{"date-parts":[[2023,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We give a novel approach to proving soundness and completeness for a logic (henceforth: the object-logic) that bypasses truth-in-a-model to work directly with validity. Instead of working with specific worlds in specific models, we reason with eigenworlds (i.e., generic representatives of worlds) in an arbitrary model. This reasoning is captured by a sequent calculus for a<jats:italic>meta<\/jats:italic>-logic (in this case, first-order classical logic) expressive enough to capture the semantics of the object-logic. Essentially, one has a calculus of validity for the object-logic. The method proceeds through the perspective of reductive logic (as opposed to the more traditional paradigm of deductive logic), using the space of reductions as a medium for showing the behavioural equivalence of reduction in the sequent calculus for the object-logic and in the validity calculus. Rather than study the technique in general, we illustrate it for the logic of Bunched Implications (BI), thus IPL and MILL (without negation) are also treated. Intuitively, BI is the free combination of intuitionistic propositional logic and multiplicative intuitionistic linear logic, which renders its meta-theory is quite complex. The literature on BI contains many similar, but ultimately different, algebraic structures and satisfaction relations that either capture only fragments of the logic (albeit large ones) or have complex clauses for certain connectives (e.g., Beth\u2019s clause for disjunction instead of Kripke\u2019s). It is this complexity that motivates us to use BI as a case-study for this approach to semantics.<\/jats:p>","DOI":"10.1007\/s11225-022-10028-z","type":"journal-article","created":{"date-parts":[[2023,1,31]],"date-time":"2023-01-31T14:04:23Z","timestamp":1675173863000},"page":"525-571","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Semantical Analysis of the Logic of Bunched Implications"],"prefix":"10.1007","volume":"111","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7144-6910","authenticated-orcid":false,"given":"Alexander V.","family":"Gheorghiu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David J.","family":"Pym","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,1,31]]},"reference":[{"key":"10028_CR1","unstructured":"Beth, W.E., Semantic Constructions of Intuitionistic Logic, Mededelingen Der Koninklijke Nederlandse Akademie Vanwetenschappen, Afd. Letterkunde 19(11):357\u2013388, 1956."},{"key":"10028_CR2","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Bunched Logics Displayed, Studia Logica 100(6):1223\u20131254, 2012.","DOI":"10.1007\/s11225-012-9449-0"},{"key":"10028_CR3","unstructured":"Bundy, A., The Computer Modelling of Mathematical Reasoning, Academic Press Professional Inc., 1985."},{"key":"10028_CR4","doi-asserted-by":"crossref","unstructured":"Cao, Q., S. Cuellar, and A. W. Appel, Bringing Order to the Separation Logic Jungle, in Bor-Yuh Evan Chang, (ed.), Asian Symposium on Programming Languages and Systems \u2013 APLAS 15, vol. 10695 of Lecture Notes in Computer Science, Springer, 2017, pp. 190\u2013211.","DOI":"10.1007\/978-3-319-71237-6_10"},{"key":"10028_CR5","unstructured":"Docherty, S., Bunched Logics: A Uniform Approach, Ph.D. thesis, University College London, 2019."},{"key":"10028_CR6","doi-asserted-by":"crossref","unstructured":"Docherty, S., and D. Pym, Intuitionistic Layered Graph Logic, in N. Olivetti, and A. Tiwari, (eds.), International Joint Conference on Automated Reasoning \u2013 IJCAR 16, Springer, 2016, pp. 469\u2013486.","DOI":"10.1007\/978-3-319-40229-1_32"},{"key":"10028_CR7","doi-asserted-by":"crossref","unstructured":"Docherty, S., and D. Pym, Modular Tableaux Calculi for Separation Theories, in Ch. Baier, and U. Dal Lago, (eds.), Foundations of Software Science and Computation Structures \u2013 FOSSACS 21, Springer International Publishing, 2018, pp. 441\u2013458.","DOI":"10.1007\/978-3-319-89366-2_24"},{"key":"10028_CR8","doi-asserted-by":"crossref","unstructured":"Docherty, S., and D. J. Pym, A Stone-type Duality Theorem for Separation Logic via its Underlying Bunched Logics, Electronic Notes in Theoretical Computer Science 336:101\u2013118, 2018.","DOI":"10.1016\/j.entcs.2018.03.018"},{"key":"10028_CR9","doi-asserted-by":"crossref","unstructured":"Docherty, S., and D. J. Pym, Intuitionistic Layered Graph Logic: Semantics and Proof Theory, Logical Methods in Computer Science 14:1\u201336, 2018.","DOI":"10.24963\/ijcai.2017\/673"},{"key":"10028_CR10","unstructured":"Docherty, S., and D. J. Pym, Stone-Type Dualities for Separation Logics, Logical Methods in Computer Science 15:1\u201340, 2019."},{"key":"10028_CR11","doi-asserted-by":"crossref","unstructured":"Dummett, M. A. E., Elements of Intuitionism, vol. 39 of Oxford Logic Guides, Clarendon Press, 2000.","DOI":"10.1093\/oso\/9780198505242.001.0001"},{"key":"10028_CR12","doi-asserted-by":"crossref","unstructured":"Gabbay, D.M., Fibring Logics, vol. 38 of Oxford Logic Guides, Clarendon Press, 1998.","DOI":"10.1093\/oso\/9780198503811.001.0001"},{"key":"10028_CR13","doi-asserted-by":"crossref","unstructured":"Galmiche, D., M. Marti, and D. Mery, Relating Labelled and Label-Free Bunched Calculi in BI Logic, in S. Cerrito, and A. Popescu, (eds.), Automated Reasoning with Analytic Tableaux and Related Methods \u2013 Tableaux 28, Springer International Publishing, 2019, pp. 130\u2013146","DOI":"10.1007\/978-3-030-29026-9_8"},{"key":"10028_CR14","doi-asserted-by":"crossref","unstructured":"Galmiche, D., D. Mery, and D. Pym, The Semantics of BI and Resource Tableaux, Mathematical Structures in Computer Science 15(6):1033\u20131088, 2005.","DOI":"10.1017\/S0960129505004858"},{"key":"10028_CR15","doi-asserted-by":"crossref","unstructured":"Gheorghiu, A.V., S. Docherty, and D.J. Pym, Reductive Logic, Coalgebra, and Proof-search: A Perspective from Resource Semantics, in A. Palmigiano, and M. Sadrzadeh, (eds.), Samson Abramsky on Logic and Structure in Computer Science and Beyond, vol. 25 of Outstanding Contributions to Logic, Springer, 2023, to appear.","DOI":"10.1007\/978-3-031-24117-8_23"},{"key":"10028_CR16","doi-asserted-by":"crossref","unstructured":"Gheorghiu, A.V., and S. Marin, Focused Proof-search in the Logic of Bunched Implications, in S. Kiefer, and Ch. Tasson, (eds.), Foundations of Software Science and Computation Structures \u2013 FOSSACS 24, vol. 12650 of Lecture Notes in Computer Science, Springer, 2021, pp. 247\u2013267.","DOI":"10.1007\/978-3-030-71995-1_13"},{"key":"10028_CR17","doi-asserted-by":"crossref","unstructured":"Komendantskaya, E., G. McCusker, and J. Power, Coalgebraic Semantics for Parallel Derivation Strategies in Logic Programming, in M. Johnson, and D. Pavlovic, (eds.), International Conference on Algebraic Methodology and Software Technology \u2013 AMAST 13, vol. 6486 of Lecture Notes in Computer Science, Springer, 2011, pp. 111\u2013127.","DOI":"10.1007\/978-3-642-17796-5_7"},{"key":"10028_CR18","unstructured":"Kowalski, R., Logic for Problem Solving, vol. 7 of Artificial Intelligence Series, Elsevier North Holland, 1979."},{"key":"10028_CR19","doi-asserted-by":"crossref","unstructured":"Kowalski, R., and D. Kuehner, Linear Resolution with Selection Function, Artificial Intelligence 2(3):227\u2013260, 1971.","DOI":"10.1016\/0004-3702(71)90012-9"},{"issue":"3","key":"10028_CR20","doi-asserted-by":"publisher","first-page":"317","DOI":"10.2307\/2964291","volume":"23","author":"G Kreisel","year":"1958","unstructured":"Kreisel, G., Elementary Completeness Properties of Intuitionistic Logic with a Note on Negations of Prenex Formulae, The Journal of Symbolic Logic 23(3):317\u2013330, 1958.","journal-title":"The Journal of Symbolic Logic"},{"key":"10028_CR21","doi-asserted-by":"crossref","unstructured":"Kripke, S. A., Semantical Analysis of Intuitionistic Logic I, in J. N. Crossley, and M. A. E. Dummett, (eds.), Formal Systems and Recursive Functions, vol. 40 of Studies in Logic and the Foundations of Mathematics, Elsevier, 1965, pp. 92\u2013130.","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"10028_CR22","doi-asserted-by":"crossref","unstructured":"Milner, R., The Use of Machines to Assist in Rigorous Proof, Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences 312(1522):411\u2013422, 1984.","DOI":"10.1098\/rsta.1984.0067"},{"key":"10028_CR23","doi-asserted-by":"crossref","unstructured":"Negri, S., Proof Analysis in Modal Logic, Journal of Philosophical Logic 34(5):507\u2013544, 2005.","DOI":"10.1007\/s10992-005-2267-3"},{"key":"10028_CR24","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P. W., and D. J. Pym, The Logic of Bunched Implications, The Bulletin of Symbolic Logic 5(2):215\u2013244, 1999.","DOI":"10.2307\/421090"},{"key":"10028_CR25","doi-asserted-by":"crossref","unstructured":"Pym, D. J., The Semantics and Proof Theory of the Logic of Bunched Implications, vol. 26 of Applied Logic Series, Springer, 2002.","DOI":"10.1007\/978-94-017-0091-7"},{"key":"10028_CR26","doi-asserted-by":"crossref","unstructured":"Pym, D. J., P. W. O\u2019Hearn, and H. Yang, Possible Worlds and Resources: The Semantics of BI, Theoretical Computer Science 315(1):257\u2013305, 2004.","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"10028_CR27","doi-asserted-by":"crossref","unstructured":"Pym, D. J., and E. Ritter, Reductive Logic and Proof-search: Proof theory, Semantics, and Control, vol. 45 of Oxford Logic Guides, Clarendon Press, 2004.","DOI":"10.1093\/acprof:oso\/9780198526339.001.0001"},{"key":"10028_CR28","unstructured":"Read, S., Relevant Logic, Basil Blackwell, 1988."},{"key":"10028_CR29","doi-asserted-by":"crossref","unstructured":"Routley, R., and R. Meyer, The Semantics of Entailment, in H. Leblanc, (ed.), Truth, Syntax, and Modality, vol. 68 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1973, pp. 199\u2013243.","DOI":"10.1016\/S0049-237X(08)71541-6"},{"key":"10028_CR30","unstructured":"Schroeder-Heister, P., Proof-Theoretic Semantics, in E. N. Zalta, (ed.), The Stanford Encyclopedia of Philosophy, Metaphysics Research Lab, Stanford University, Spring 2018."},{"key":"10028_CR31","unstructured":"Szabo, M. E., (ed.), The Collected Papers of Gerhard Gentzen, North-Holland Publishing Company, 1969."},{"key":"10028_CR32","doi-asserted-by":"crossref","unstructured":"Troelstra, A. S., and H. Schwichtenberg, Basic Proof Theory, vol. 43 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2000.","DOI":"10.1017\/CBO9781139168717"},{"key":"10028_CR33","doi-asserted-by":"crossref","unstructured":"Urquhart, A., Semantics for Relevant Logics, The Journal of Symbolic Logic 37(1):159\u2013169, 1972.","DOI":"10.2307\/2272559"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-022-10028-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11225-022-10028-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-022-10028-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,5]],"date-time":"2023-12-05T23:08:08Z","timestamp":1701817688000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11225-022-10028-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,31]]},"references-count":33,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,8]]}},"alternative-id":["10028"],"URL":"https:\/\/doi.org\/10.1007\/s11225-022-10028-z","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,31]]},"assertion":[{"value":"28 March 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 November 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 January 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}