Abstract
This paper introduces a natural deduction calculus for intuitionistic logic of belief \(\mathsf {IEL}^{-}\) which is easily turned into a modal \(\lambda \)-calculus giving a computational semantics for deductions in \(\mathsf {IEL}^{-}\). By using that interpretation, it is also proved that \(\mathsf {IEL}^{-}\) has good proof-theoretic properties. The correspondence between deductions and typed terms is then extended to a categorical semantics for identity of proofs in \(\mathsf {IEL}^{-}\) showing the general structure of such a modality for belief in an intuitionistic framework.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Akama, Y., On Mints’ reduction for ccc-calculus, in International Conference on Typed Lambda Calculi and Applications, Springer, 1993, pp. 1–12.
Artemov, S., and T. Protopopescu, Intuitionistic epistemic logic, The Review of Symbolic Logic 9(2):266–298, 2016.
Awodey, S., and A. Bauer, Propositions as [types], Journal of Logic and Computation 14(4):447–471, 2004
de Groote, P., On the strong normalisation of intuitionistic natural deduction with permutation-conversions, Information and Computation 178(2):441–464, 2002.
de Paiva, 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–428.
Dummett, M., Elements of intuitionism, Oxford University Press, 2000.
Girard, J.-Y., P. Taylor, and Y. Lafont, Proofs and types, Cambridge University Press, 1989.
Kakutani, Y., Calculi for intuitionistic normal modal logic, ar**v preprint ar**v:1606.03180, 2016.
Kripke, S. A., Semantical analysis of intuitionistic logic i, in Studies in Logic and the Foundations of Mathematics, vol. 40, Elsevier, 1965, pp. 92–130.
Lambek, J., and P. J. Scott, Introduction to higher-order categorical logic, vol. 7, Cambridge University Press, 1988.
Mac Lane, S., Categories for the working mathematician, vol. 5, Springer Science & Business Media, 2013.
Negri, S., J. Von Plato, and A. Ranta, Structural proof theory, Cambridge University Press, 2008.
Rijke, E., M. Shulman, and B. Spitters, Modalities in homotopy type theory, ar**v preprint ar**v:1706.07526, 2017.
Sørensen, M. H., and P. Urzyczyn, Lectures on the Curry-Howard isomorphism, vol. 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006.
Tait, W. W., Intensional interpretations of functionals of finite type i, The Journal of Symbolic Logic 32(2):198–212, 1967.
Troelstra, A., Principles of Intuitionism, Springer, 1969.
van Dalen, D., Logic and Structure, 4th edn., Springer, 2008.
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.
von Plato, J., The development of proof theory, in Edward N. Zalta, (ed.), The Stanford Encyclopedia of Philosophy, winter 2018 edn., Metaphysics Research Lab, Stanford University, 2018.
Williamson, T., On intuitionistic modal epistemic logic, Journal of Philosophical Logic 21(1):63–89, 1992.
Acknowledgements
These results were obtained during my first year of PhD studies at DiMa of University of Genoa. After discussing a preliminary version of categorical semantics for intuitionistic belief during the Logic and Philosophy of Science Seminar of University of Florence in May 2019, I had the great opportunity to present more refined results during the poster session of The Proof Society Summer School in September 2019: My gratitude goes to all logicians of the Computational Foundry of Swansea University who hosted the event, along with the invited lecturers and the participants. In particular, I wish to thank Reuben Rowe for an enlightening discussion on the way to Rhossili about the behaviour of the \(\Box \) in my formal system. A sincere acknowledgement goes to an anonymous reviewer for suggesting further investigations on the proof theory of the calculus I originally presented to this journal: Her/His comments have been very important for structuring the final version of this work.
Funding
Open access funding provided by Universitá degli Studi di Genova within the CRUI-CARE Agreement.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Presented by Yde Venema
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Perini Brogi, C. Curry–Howard–Lambek Correspondence for Intuitionistic Belief. Stud Logica 109, 1441–1461 (2021). https://doi.org/10.1007/s11225-021-09952-3
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-021-09952-3