Abstract

In 2015 Dag Prawitz proposed a natural deduction ecumenical system, where classical logic and intuitionistic logic are codified in the same system. In his ecumenical system, Prawitz recovers the harmony of rules, but the rules for the classical operators do not satisfy separability. In fact, the classical rules are not pure, in the sense that negation is used in the definition of the introduction and elimination rules for the classical operators. In this work we propose an ecumenical system adapting, to the natural deduction framework, Girard’s mechanism of stoup. This allows for the definition of a pure harmonic natural deduction system for the propositional fragment of Prawitz’s ecumenical logic. We conclude by presenting an extension proposal to the first-order setting and a different approach to purity based on some ideas proposed by Julien Murzi.