{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:15:10Z","timestamp":1760080510300,"version":"3.37.3"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2021,6,16]],"date-time":"2021-06-16T00:00:00Z","timestamp":1623801600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,6,16]],"date-time":"2021-06-16T00:00:00Z","timestamp":1623801600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004702","name":"Universit\u00e0 degli Studi di Genova","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004702","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2021,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper introduces a<jats:italic>natural deduction calculus for intuitionistic logic of belief<\/jats:italic><jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {IEL}^{-}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mrow><mml:mi>IEL<\/mml:mi><\/mml:mrow><mml:mo>-<\/mml:mo><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>which is easily turned into a<jats:italic>modal<\/jats:italic><jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03bb<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula><jats:italic>-calculus<\/jats:italic>giving a computational semantics for deductions in<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {IEL}^{-}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mrow><mml:mi>IEL<\/mml:mi><\/mml:mrow><mml:mo>-<\/mml:mo><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>. By using that interpretation, it is also proved that<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {IEL}^{-}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mrow><mml:mi>IEL<\/mml:mi><\/mml:mrow><mml:mo>-<\/mml:mo><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>has<jats:italic>good proof-theoretic properties<\/jats:italic>. The correspondence between deductions and typed terms is then extended to a<jats:italic>categorical semantics<\/jats:italic>for identity of proofs in<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {IEL}^{-}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mrow><mml:mi>IEL<\/mml:mi><\/mml:mrow><mml:mo>-<\/mml:mo><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>showing the general structure of such a modality for belief in an intuitionistic framework.<\/jats:p>","DOI":"10.1007\/s11225-021-09952-3","type":"journal-article","created":{"date-parts":[[2021,6,16]],"date-time":"2021-06-16T06:12:46Z","timestamp":1623823966000},"page":"1441-1461","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Curry\u2013Howard\u2013Lambek Correspondence for Intuitionistic Belief"],"prefix":"10.1007","volume":"109","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7883-5727","authenticated-orcid":false,"given":"Cosimo","family":"Perini Brogi","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,6,16]]},"reference":[{"key":"9952_CR1","doi-asserted-by":"crossref","unstructured":"Akama, Y., On Mints\u2019 reduction for ccc-calculus, in International Conference on Typed Lambda Calculi and Applications, Springer, 1993, pp. 1\u201312.","DOI":"10.1007\/BFb0037094"},{"issue":"2","key":"9952_CR2","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1017\/S1755020315000374","volume":"9","author":"Sergei Artemov","year":"2016","unstructured":"Artemov, S., and T. Protopopescu, Intuitionistic epistemic logic, The Review of Symbolic Logic 9(2):266\u2013298, 2016.","journal-title":"The Review of Symbolic Logic"},{"issue":"4","key":"9952_CR3","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1093\/logcom\/14.4.447","volume":"14","author":"Steve Awodey","year":"2004","unstructured":"Awodey, S., and A. Bauer, Propositions as [types], Journal of Logic and Computation 14(4):447\u2013471, 2004","journal-title":"Journal of Logic and Computation"},{"key":"9952_CR4","doi-asserted-by":"crossref","unstructured":"de\u00a0Groote, P., On the strong normalisation of intuitionistic natural deduction with permutation-conversions, Information and Computation 178(2):441\u2013464, 2002.","DOI":"10.1006\/inco.2002.3147"},{"key":"9952_CR5","unstructured":"de\u00a0Paiva, V., and E. Ritter, Basic constructive modality, in J.-Y. Beziau, and M. E. Coniglio, (eds.), Logic without Frontiers: Festschrift for Walter Alexandre Carnielli on the occasion of his 60th Birthday, College Publications, 2011, pp. 411\u2013428."},{"key":"9952_CR6","doi-asserted-by":"crossref","unstructured":"Dummett, M., Elements of intuitionism, Oxford University Press, 2000.","DOI":"10.1093\/oso\/9780198505242.001.0001"},{"key":"9952_CR7","unstructured":"Girard, J.-Y., P. Taylor, and Y. Lafont, Proofs and types, Cambridge University Press, 1989."},{"key":"9952_CR8","unstructured":"Kakutani, Y., Calculi for intuitionistic normal modal logic, arXiv preprint arXiv:1606.03180, 2016."},{"key":"9952_CR9","doi-asserted-by":"crossref","unstructured":"Kripke, S.\u00a0A., Semantical analysis of intuitionistic logic i, in Studies in Logic and the Foundations of Mathematics, vol.\u00a040, Elsevier, 1965, pp. 92\u2013130.","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"9952_CR10","unstructured":"Lambek, J., and P.\u00a0J. Scott, Introduction to higher-order categorical logic, vol.\u00a07, Cambridge University Press, 1988."},{"key":"9952_CR11","unstructured":"Mac\u00a0Lane, S., Categories for the working mathematician, vol.\u00a05, Springer Science & Business Media, 2013."},{"key":"9952_CR12","unstructured":"Negri, S., J. Von\u00a0Plato, and A. Ranta, Structural proof theory, Cambridge University Press, 2008."},{"key":"9952_CR13","unstructured":"Rijke, E., M. Shulman, and B. Spitters, Modalities in homotopy type theory, arXiv preprint arXiv:1706.07526, 2017."},{"key":"9952_CR14","doi-asserted-by":"crossref","unstructured":"S\u00f8rensen, M.\u00a0H., and P. Urzyczyn, Lectures on the Curry-Howard isomorphism, vol. 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006.","DOI":"10.1016\/S0049-237X(06)80005-4"},{"issue":"2","key":"9952_CR15","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"William W Tait","year":"1967","unstructured":"Tait, W.\u00a0W., Intensional interpretations of functionals of finite type i, The Journal of Symbolic Logic 32(2):198\u2013212, 1967.","journal-title":"The Journal of Symbolic Logic"},{"key":"9952_CR16","doi-asserted-by":"crossref","unstructured":"Troelstra, A., Principles of Intuitionism, Springer, 1969.","DOI":"10.1007\/BFb0080643"},{"key":"9952_CR17","unstructured":"van Dalen, D., Logic and Structure, 4th edn., Springer, 2008."},{"key":"9952_CR18","unstructured":"van Dalen, D., and A. Troelstra, Constructivism in Mathematics. An Introduction I, vol. 121 of Studies in Logic and the Foundations of Mathematics, Elsevier, 1988."},{"key":"9952_CR19","unstructured":"von Plato, J., The development of proof theory, in Edward\u00a0N. Zalta, (ed.), The Stanford Encyclopedia of Philosophy, winter 2018 edn., Metaphysics Research Lab, Stanford University, 2018."},{"issue":"1","key":"9952_CR20","first-page":"63","volume":"21","author":"Timothy Williamson","year":"1992","unstructured":"Williamson, T., On intuitionistic modal epistemic logic, Journal of Philosophical Logic 21(1):63\u201389, 1992.","journal-title":"Journal of Philosophical Logic"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-021-09952-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11225-021-09952-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-021-09952-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,4]],"date-time":"2023-11-04T23:09:11Z","timestamp":1699139351000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11225-021-09952-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,16]]},"references-count":20,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["9952"],"URL":"https:\/\/doi.org\/10.1007\/s11225-021-09952-3","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2021,6,16]]},"assertion":[{"value":"18 April 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 June 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}