On an ecumenical natural deduction with stoup -- Part I: The propositional case

TL;DR

This paper introduces a novel harmonic natural deduction system for propositional ecumenical logic, combining intuitionistic and classical logic features using Girard's stoup mechanism, aiming to preserve meta-logical properties.

Contribution

It adapts Girard's stoup to natural deduction, creating a pure harmonic system for Prawitz's ecumenical logic's propositional fragment, improving logical harmony.

Findings

Defines a harmonic natural deduction system using stoup

Maintains meta-logical properties like harmony

Applies to propositional ecumenical logic

Abstract

Natural deduction systems, as proposed by Gentzen and further studied by Prawitz, is one of the most well known proof-theoretical frameworks. Part of its success is based on the fact that natural deduction rules present a simple characterization of logical constants, especially in the case of intuitionistic logic. However, there has been a lot of criticism on extensions of the intuitionistic set of rules in order to deal with classical logic. Indeed, most of such extensions add, to the usual introduction and elimination rules, extra rules governing negation. As a consequence, several meta-logical properties, the most prominent one being harmony, are lost. Dag Prawitz proposed a natural deduction ecumenical system, where classical logic and intuitionistic logic are codified in the same system. In this system, the classical logician and the intuitionistic logician would share the universal quantifier, conjunction, negation and the constant for the absurd, but they would each have their own existential quantifier, disjunction and implication, with different meanings. Prawitz' main idea is that these different meanings are given by a semantical framework that can be accepted by both parties. In this paper, we propose a different approach adapting, to the natural deduction framework, Girard's mechanism of stoup. This will allow the definition of a pure harmonic natural deduction system for the propositional fragment of Prawitz' ecumenical logic.