Pimentel, E;
Pereira, LC;
(2023)
A Tour on Ecumenical Systems.
In:
10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023).
(pp. 3:1-3:15).
Proceedings of the 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023): Dagstuhl, Germany.
Preview |
Text
LIPIcs-CALCO-2023-3.pdf - Published Version Download (793kB) | Preview |
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 [35]. 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.
| Type: | Proceedings paper |
|---|---|
| Title: | A Tour on Ecumenical Systems |
| Event: | 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023) |
| ISBN-13: | 978-3-95977-287-7 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.4230/LIPIcs.CALCO.2023.3 |
| Publisher version: | https://doi.org/10.4230/LIPIcs.CALCO.2023.3 |
| Language: | English |
| Additional information: | © Elaine Pimentel and Luiz Carlos Pereira; licensed under Creative Commons License CC-BY 4.0 (https://creativecommons.org/licenses/by/4.0/). |
| Keywords: | Intuitionistic logic, classical logic, modal logic, ecumenical systems, proof theory |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10178210 |
Archive Staff Only
 |
View Item |
