Pereira, LC;
Pimentel, E;
(2024)
On an Ecumenical Natural Deduction with Stoup. Part I: The Propositional Case.
In:
Perspectives on Deduction: Contemporary Studies in the Philosophy, History and Formal Theories of Deduction.
(pp. 139-169).
Springer, Cham
Preview |
PDF
Ecumenical-ND-VF-Revised.pdf - Published Version Download (369kB) | Preview |
Abstract
In 2015 Dag Prawitz proposed a natural deduction ecumenical system, where classical logic and intuitionistic logic are codified in the same system. In his ecumenical system, Prawitz recovers the harmony of rules, but the rules for the classical operators do not satisfy separability. In fact, the classical rules are not pure, in the sense that negation is used in the definition of the introduction and elimination rules for the classical operators. In this work we propose an ecumenical system adapting, to the natural deduction framework, Girard’s mechanism of stoup. This allows for the definition of a pure harmonic natural deduction system for the propositional fragment of Prawitz’s ecumenical logic. We conclude by presenting an extension proposal to the first-order setting and a different approach to purity based on some ideas proposed by Julien Murzi.
| Type: | Book chapter |
|---|---|
| Title: | On an Ecumenical Natural Deduction with Stoup. Part I: The Propositional Case |
| ISBN-13: | 9783031514050 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-031-51406-7_7 |
| Publisher version: | https://doi.org/10.1007/978-3-031-51406-7_7 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10216316 |
Archive Staff Only
 |
View Item |
