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 \textit{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, 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, 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.
翻译:关于经典逻辑和直觉主义逻辑有效性的哲学基础争论,其核心争议点之一往往涉及逻辑证明的本质。直觉主义者倡导一种严格的构造性证明概念,而经典逻辑学家则通过反证法支持允许非构造性证明的概念。时至今日,该争论仍悬而未决,因为争论双方对非构造性方法的确切立场尚未达成共识。当前,两种迥异的逻辑方法正为这场辩论提供有意义的贡献。第一种常被称为逻辑普适主义,旨在构建一个统一框架使两种"对立"逻辑和平共存,从而为争论双方提供某种中立立场。第二种即证明论语义学,不仅致力于阐明逻辑证明的含义,还试图为将其作为语义分析的基本概念提供应用途径。逻辑普适主义为经典逻辑与直觉主义逻辑的有意义互动提供了媒介,而证明论语义学则阐明了接受或拒绝将反证法作为有意义证明方法时涉及的核心问题。本文通过构建一个不仅允许经典逻辑与直觉主义逻辑共存、更允许经典证明概念与直觉主义证明概念共存的框架,展示了如何将两种方法有机融合。