  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.
