Barroso-Nascimento, Victor;
Pereira, Luiz Carlos;
Pimentel, Elaine;
(2025)
An ecumenical view of proof-theoretic semantics.
SYNTHESE
, 206
(4)
, Article 197. 10.1007/s11229-025-05269-z.
Preview |
Text
s11229-025-05269-z (9).pdf - Published Version Download (9MB) | Preview |
Abstract
Debates concerning philosophical grounds for the validity of classical and intuitionistic logics often have the very nature of proofs as a point of controversy. The intuitionist advocates for a strictly constructive notion of proof, while the classical logician advocates for a notion which allows the use of non-constructive principles such as reductio ad absurdum. In this paper we show how to coherently combine logical ecumenism and proof-theoretic semantics (PtS) by providing not only a medium in which classical and intuitionistic logics coexist, but also one in which their respective notions of proof coexist. Intuitionistic proofs receive the standard treatment of PtS, whereas classical proofs are given a semantics based on ideas by David Hilbert. Furthermore, we advance the state of the art in PtS by introducing a key contribution: treating the absurdity constant ⊥ as an atomic proposition and requiring all bases to be consistent. This treatment is essential for the obtainment of some ecumenical results, and it can also be used in standard intuitionistic PtS. Additionally, we employ normalization techniques to demonstrate the consistency of simulation bases. These innovations provide fresh technical and conceptual insights into the study of bases in PtS.
| Type: | Article |
|---|---|
| Title: | An ecumenical view of proof-theoretic semantics |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/s11229-025-05269-z |
| Publisher version: | https://doi.org/10.1007/s11229-025-05269-z |
| Language: | English |
| Additional information: | 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/. |
| Keywords: | Arts & Humanities, History & Philosophy Of Science, Philosophy, History & Philosophy of Science, Ecumenical logic, Proof theoretic semantic, Base extension semantic, Intuitionistic logic, Classical logic, TRUTH, LOGIC |
| 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/10216242 |
Archive Staff Only
 |
View Item |
