Elaine Pimentel

Associate Professor at University College London, UK

Proof theory for ecumenical systems

 

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 tutorial, we will embark on a journey through ecumenical systems, drawing inspiration from Prawitz’ seminal work [8]. 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.

The tutorial is based on the following papers:

1. Sonia Marin, Luiz Carlos Pereira, Elaine Pimentel, and Emerson Sales. Ecumenical modal logic. In DaLi 2020, volume 12569 of LNCS, pages 187–204. Springer, 2020. doi:10.1007/978-3-030-65840-3_12.
2. 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 ­27^th International Workshop, WoLLIC 2021, Virtual Event, October 5-8, 2021, Proceedings, volume 13038 of Lecture Notes in Computer Science, pages 388–407. Springer, 2021. doi:10.1007/978-3-030-88853-4_24
3. Sonia Marin, Luiz Carlos Pereira, Elaine Pimentel, and Emerson Sales. Separability and harmony in ecumenical systems. CoRR, abs/2204.02076, 2022. arXiv:2204.02076, doi:10.48550/arXiv.2204.02076
4. Victor Nascimento, Luiz Carlos Pereira, and Elaine Pimentel. An ecumenical view of proof-theoretic semantics, 2023. arXiv:2306.03656
5. Carlos Olarte, Elaine Pimentel, and Camilo Rocha. A rewriting logic approach to specifcation, proof-search, and meta-proofs in sequent systems. J. Log. Algebraic Methods Program., 130:100827, 2023. doi:10.1016/j.jlamp.2022.100827
6. Luiz Carlos Pereira and Elaine Pimentel. On an ecumenical natural deduction with stoup - part I: the propositional case. CoRR, abs/2204.02199, 2022. arXiv:2204.02199, doi:10.48550/arXiv.2204.02199
7. Elaine Pimentel, Luiz Carlos Pereira, and Valeria de Paiva. An ecumenical notion of entailment. Synthese, 198(22-S):5391–5413, 2021. doi:10.1007/s11229-019-02226-5
8. 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.

 
Acknowledgements

I want to thank my co-authors in this endeavour: Luiz Carlos Pereira, Valeria de Paiva, Sonia Marin, Emerson Sales, Delia Kesner, Mariana Milicich, Victor Nascimento and Carlos Olarte.
This work has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement Number 101007627.

Course materials

• Slides from Lecture 1 [pdf]
• Slides from Lecture 2 [pdf]
• Slides from Lecture 3 [pdf]
• Slides from Lecture 4 [pdf]

---