Document Open Access Logo

A Tour on Ecumenical Systems (Invited Talk)

Authors Elaine Pimentel , Luiz Carlos Pereira

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2023.3.pdf
  • Filesize: 0.75 MB
  • 15 pages

Document Identifiers

Author Details

Elaine Pimentel
  • Department of Computer Science, University College London, UK
Luiz Carlos Pereira
  • Department of Philosophy, UERJ, Brazil

Funding

  • Pimentel, Elaine: Pimentel has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement Number 101007627.
  • Pereira, Luiz Carlos: Pereira is supported by the following projects: CAPES/PRINT, CNPq-313400/2021-0, and CNPq-Gaps and Gluts.

Acknowledgements

We want to thank Dag Prawitz for the friendship and inspiration, and our co-authors in this endeavour: Valeria de Paiva, Sonia Marin, Emerson Sales, Delia Kesner, Mariana Milicich, Victor Nascimento and Carlos Olarte.

Cite AsGet BibTex

Elaine Pimentel and Luiz Carlos Pereira. A Tour on Ecumenical Systems (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CALCO.2023.3

Abstract

Ecumenism can be understood as a pursuit of unity, where diverse thoughts, ideas, or points of view coexist harmoniously. In logic, ecumenical systems refer, in a broad sense, to proof systems for combining logics. One captivating area of research over the past few decades has been the exploration of seamlessly merging classical and intuitionistic connectives, allowing them to coexist peacefully. In this paper, we will embark on a journey through ecumenical systems, drawing inspiration from Prawitz' seminal work [Dag Prawitz, 2015]. We will begin by elucidating Prawitz' concept of "ecumenism" and present a pure sequent calculus version of his system. Building upon this foundation, we will expand our discussion to incorporate alethic modalities, leveraging Simpson’s meta-logical characterization. This will enable us to propose several proof systems for ecumenical modal logics. We will conclude our tour with some discussion towards a term calculus proposal for the implicational propositional fragment of the ecumenical logic, the quest of automation using a framework based in rewriting logic, and an ecumenical view of proof-theoretic semantics.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
Keywords
  • Intuitionistic logic
  • classical logic
  • modal logic
  • ecumenical systems
  • proof theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. Log. Comput., 2(3):297-347, 1992. URL: https://doi.org/10.1093/logcom/2.3.297.
  2. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. URL: https://doi.org/10.1017/CBO9781107050884.
  3. Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some axioms for mathematics. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 20:1-20:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.20.
  4. Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. A modular construction of type theories. Log. Methods Comput. Sci., 19(1), 2023. URL: https://doi.org/10.46298/lmcs-19(1:12)2023.
  5. Robert Brandom. Articulating Reasons: An Introduction to Inferentialism. Harvard University Press, 2000. Google Scholar
  6. Kai Brünnler. Deep sequent systems for modal logic. Arch. Math. Log., 48:551-577, 2009. Google Scholar
  7. Robert A. Bull. Cut elimination for propositional dynamic logic wihout *. Zeitschr. f. math. Logik und Grundlagen d. Math., 38:85-100, 1992. Google Scholar
  8. Carlos Caleiro and Jaime Ramos. Combining classical and intuitionistic implications. In Boris Konev and Frank Wolter, editors, Frontiers of Combining Systems, 6th International Symposium, FroCoS 2007, Liverpool, UK, September 10-12, 2007, Proceedings, volume 4720 of Lecture Notes in Computer Science, pages 118-132. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74621-8_8.
  9. Luis Fariñas del Cerro and Andreas Herzig. Combinig classical and intuitionistic logic, or: Intuitionistic implication as a conditional. In Franz Baader and Klaus U. Schulz, editors, Frontiers of Combining Systems, First International Workshop FroCoS 1996, Munich, Germany, March 26-29, 1996, Proceedings, volume 3 of Applied Logic Series, pages 93-102. Kluwer Academic Publishers, 1996. Google Scholar
  10. Gilles Dowek. On the definition of the classical connectives and quantifiers. Why is this a Proof?, Festschrift for Luiz Carlos Pereira, 27:228-238, 2016. Google Scholar
  11. Michael Dummett. The Logical Basis of Metaphysics. Cambridge, Mass.: Harvard University Press, 1991. Google Scholar
  12. Melvin Fitting. Nested sequents for intuitionistic logics. Notre Dame Journal of Formal Logic, 55(1):41-61, 2014. URL: https://doi.org/10.1215/00294527-2377869.
  13. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. Google Scholar
  14. Jean-Yves Girard. A new constructive logic: Classical logic. Math. Struct. Comput. Sci., 1(3):255-296, 1991. URL: https://doi.org/10.1017/S0960129500001328.
  15. Jean-Yves Girard. On the unity of logic. Ann. Pure Appl. Logic, 59(3):201-217, 1993. URL: https://doi.org/10.1016/0168-0072(93)90093-S.
  16. Ryo Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53(1):119-136, 1994. URL: https://doi.org/10.1007/BF01053026.
  17. Peter Krauss. A constructive refinement of classical logic. Draft, 1992. Google Scholar
  18. Chuck Liang and Dale Miller. A focused approach to combining logics. Ann. Pure Appl. Logic, 162(9):679-697, 2011. URL: https://doi.org/10.1016/j.apal.2011.01.012.
  19. Chuck C. Liang and Dale Miller. Focusing and polarization in intuitionistic logic. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings, volume 4646 of Lecture Notes in Computer Science, pages 451-465. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74915-8_34.
  20. Paqui Lucio. Structured sequent calculi for combining intuitionistic and classical first-order logic. In Hélène Kirchner and Christophe Ringeissen, editors, Frontiers of Combining Systems, Third International Workshop, FroCoS 2000, Nancy, France, March 22-24, 2000, Proceedings, volume 1794 of Lecture Notes in Computer Science, pages 88-104. Springer, 2000. URL: https://doi.org/10.1007/10720084_7.
  21. Sonia Marin, Dale Miller, Elaine Pimentel, and Marco Volpe. From axioms to synthetic inference rules via focusing. Ann. Pure Appl. Log., 173(5):103091, 2022. URL: https://doi.org/10.1016/j.apal.2022.103091.
  22. Sonia Marin, Luiz Carlos Pereira, Elaine Pimentel, and Emerson Sales. Ecumenical modal logic. In DaLí 2020, volume 12569 of LNCS, pages 187-204. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-65840-3_12.
  23. Sonia Marin, Luiz Carlos Pereira, Elaine Pimentel, and Emerson Sales. A pure view of ecumenical modalities. In Alexandra Silva, Renata Wassermann, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information, and Computation - 27th International Workshop, WoLLIC 2021, Virtual Event, October 5-8, 2021, Proceedings, volume 13038 of Lecture Notes in Computer Science, pages 388-407. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-88853-4_24.
  24. Sonia Marin, Luiz Carlos Pereira, Elaine Pimentel, and Emerson Sales. Separability and harmony in ecumenical systems. CoRR, abs/2204.02076, 2022. URL: https://doi.org/10.48550/arXiv.2204.02076.
  25. Julien Murzi. Classical harmony and separability. Erkenntnis, 85:391-415, 2020. Google Scholar
  26. Victor Nascimento, Luiz Carlos Pereira, and Elaine Pimentel. An ecumenical view of proof-theoretic semantics, 2023. URL: https://arxiv.org/abs/2306.03656.
  27. Sara Negri. Proof analysis in modal logic. J. Philosophical Logic, 34(5-6):507-544, 2005. URL: https://doi.org/10.1007/s10992-005-2267-3.
  28. Carlos Olarte, Elaine Pimentel, and Camilo Rocha. A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems. CoRR, abs/2101.03113, 2021. URL: https://arxiv.org/abs/2101.03113.
  29. Michel Parigot. λμ-calculus: An algorithmic interpretation of classical natural deduction. In LPAR: Logic Programming and Automated Reasoning, International Conference, volume 624 of LNCS, pages 190-201. Springer, 1992. Google Scholar
  30. Luiz Carlos Pereira and Elaine Pimentel. On an ecumenical natural deduction with stoup - part I: the propositional case. CoRR, abs/2204.02199, 2022. URL: https://doi.org/10.48550/arXiv.2204.02199.
  31. Luiz Carlos Pereira and Ricardo Oscar Rodriguez. Normalization, soundness and completeness for the propositional fragment of Prawitz' ecumenical system. Revista Portuguesa de Filosofia, 73(3-3):1153-1168, 2017. Google Scholar
  32. Elaine Pimentel, Luiz Carlos Pereira, and Valeria de Paiva. An ecumenical notion of entailment. Synthese, 198(22-S):5391-5413, 2021. URL: https://doi.org/10.1007/s11229-019-02226-5.
  33. Francesca Poggiolesi. The method of tree-hypersequents for modal propositional logic. In Towards Mathematical Philosophy, volume 28 of Trends In Logic, pages 31-51. Springer, 2009. Google Scholar
  34. Dag Prawitz. Natural Deduction, volume 3 of Stockholm Studies in Philosophy. Almqvist and Wiksell, 1965. Google Scholar
  35. Dag Prawitz. Classical versus intuitionistic logic. In Bruno Lopes Edward Hermann Haeusler, Wagner de Campos Sanz, editor, Why is this a Proof?, Festschrift for Luiz Carlos Pereira, volume 27, pages 15-32. College Publications, 2015. Google Scholar
  36. Greg Restall. Speech acts & the quest for a natural account of classical proof. Available at https://consequently.org/writing/, 2021.
  37. José Espírito Santo, Delia Kesner, and Loïc Peyrot. A faithful and quantitative notion of distant reduction for generalized applications. In Patricia Bouyer and Lutz Schröder, editors, Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, volume 13242 of Lecture Notes in Computer Science, pages 285-304. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99253-8_15.
  38. Peter Schroeder-Heister. Uniform proof-theoretic semantics for logical constants (abstract). Journal of Symbolic Logic, 56:1142, 1991. Google Scholar
  39. Peter Schroeder-Heister. Validity concepts in proof-theoretic semantics. Synthese, 148(3):525-571, 2006. Google Scholar
  40. Alex K. Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, College of Science and Engineering, School of Informatics, University of Edinburgh, 1994. Google Scholar
  41. Lutz Straßburger. Cut elimination in nested sequents for intuitionistic modal logics. In Proceedings of FOSSACS 2013, pages 209-224, 2013. URL: https://doi.org/10.1007/978-3-642-37075-5_14.
  42. Matteo Tesi and Sara Negri. Neighbourhood semantics and labelled calculus for intuitionistic infinitary logic. J. Log. Comput., 31(7):1608-1639, 2021. URL: https://doi.org/10.1093/logcom/exab040.
  43. Luca Viganò. Labelled Non-Classical Logics. Kluwer Academic Publishers, 2000. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact