Victor Barroso-Nascimento

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}}$$.

The relation between ex falso and disjunctive syllogism, or even the justification of ex falso based on disjunctive syllogism, is an old topic in the history of logic. This old topic reappears in contemporary logic since the introduction of minimal logic by Johansson. The disjunctive syllogism seems to be part of our general non-problematic inferential practices and superficially it does not seem to be related to or to depend on our acceptance of the frequently disputable ex falso rule. We know that the acceptance of the ex falso is a sufficient condition for the acceptance of the disjunctive syllogism, but the interesting question is: is the ex falso a necessary condition for the acceptance of the disjunctive syllogism? The aim of the present paper is to discuss some possible ways to define systems that combines the preservation of the disjunctive syllogism with the rejection of the ex falso.

Prawitz conjectured that the proof-theoretically valid logic is intuitionistic logic. Recent work on proof-theoretic validity has disproven this. In fact, it has been shown that proof-theoretic validity is not even closed under substitution. In this paper, we make a minor modification to the definition of proof-theoretic validity found in Prawitz’s 1973paper ‘Towards a foundation of a general proof theory’ and refined by Schroeder-Heister in ‘Validity concepts in proof-theoretic semantics’ (2006). We will call the new notion generalized proof-theoretic validity and show that the logic of generalized proof-theoretic validity is intuitionistic logic.