An ecumenical view of proof-theoretic semantics
Victor Barroso-Nascimento, Luiz Carlos Pereira, Elaine Gouvêa Pimentel · Synthese · 2025
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 ( $$\boldsymbol{\mathrm{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 $$\boldsymbol{\mathrm{PtS}}$$ , whereas classical proofs are given a semantics based on ideas by David Hilbert. Furthermore, we advance the state of the art in $$\boldsymbol{\mathrm{PtS}}$$ by introducing a key contribution: treating the absurdity constant $$\bot$$ 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 $$\boldsymbol{\mathrm{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 $$\boldsymbol{\mathrm{PtS}}$$ .