Authors: Victor Nascimento, Luiz Carlos Pereira and Elaine Pimentel

Debates concerning philosophical grounds for the validity of classical and intuitionistic logics often have the very nature of logical proofs as one of the main points of controversy. The intuitionist advocates for a strict notion of constructive proof, while the classical logician advocates for a notion which allows non-construtive proofs through reductio ad absurdum. A great deal of controversy still subsists to this day on the matter, as there is no agreement between disputants on the precise standing of non-constructive methods.

Two very distinct approaches to logic are currently providing interesting contributions to this debate. The first, oftentimes called logical ecumenism [1], aims to provide a unified framework in which two “rival” logics may peacefully coexist, thus providing some sort of neutral ground for the contestants. The second, proof-theoretic semantics [2], aims not only to elucidate the meaning of a logical proof, but also to provide means for its use as a basic concept of semantic analysis. Logical ecumenism thus provides a medium in which meaningful interactions may occur between classical and intuitionistic logic, whilst proof-theoretic semantics provides a way of clarifying what is at stake when one accepts or denies reductio ad absurdum as a meaningful proof method.

In this paper we show how to coherently combine 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.

Bibliography

1. Dag Prawitz. Natural deduction: A proof-theoretical study. Dover Publications, 2006.
2. Peter Schroeder-Heister. A natural extension of natural deduction. Journal of Symbolic Logic, 49:1284–1300, 1984.