What is a proof? In the context of logic and mathematics, a proof is a logical argument that establishes the correctness of a claim based on a set of assumed axioms and definitions, together with previously proven statements. Nevertheless, since the construction methods of these arguments may vary, a proof that appears satisfactory to a classical logician may not necessarily meet the criteria for an intuitionistic (constructive) logician. For instance, constructive logicians do not accept mathematical proofs that explicitly employ the principle of excluded middle --- any formula is either valid or its negation is valid. But does this discrepancy solely pertain to proof methods? What is the real nature of this disagreement?
This project rises in the context of these questions. We seek at giving answers by employing an ecumenical view to proof-theoretic semantics. As the name indicates, PtS aims not only to elucidate the meaning of logical proofs, but also to provide means for its use as a basic concept of semantic analysis. Logical ecumenism, on the other hand, provides a medium in which meaningful interactions may occur between 'rival' logics.
This project aims at coherently combining both approaches by providing not only a medium in which classical and intuitionistic logics may coexist, but also one in which classical and intuitionistic notions of proof may coexist. This opens the door for the systematic study of proofs in different logics and logical systems, and it reflects the essence of logical ecumenism: embracing diverse views and ideas to construct a shared platform where different logical approaches can coexist.
This project has, as an overall objective, to deepen our understanding of logical reasoning disagreements by investigating further into the ecumenical approach and developing a unified proof-theoretic foundation for logical reasoning. In particular, we intend to proceed with a careful analysis on different aspects of PtS for logical systems where classical and intuitionistic notions of proof coexist in peace (i.e., without collapsing) in several contexts and frameworks.
Our goal is to bring a fresh perspective to the interpretation of connectives, formulas and proofs. By combining ecumenism with proof-theoretic semantics, we aim to improve the understanding of how logical systems work and to suggest new ways of using them in different situations. Indeed, the ecumenical approach to PtS not only enables revisiting the notion of the meaning of well known logics, but also highlights fundamental properties of semantic entailment that may not be readily apparent in traditional semantic analysis. And this can be broadly used in order to propose new semantical analysis of many logics, such as epistemic (dealing with knowledge and belief), dynamic (capable of encoding properties of computer programs) and temporal logics.