Our Lunch Seminar series continues on Monday, April 4th! We will host Elaine Pimentel (UCL London) who will give a talk on Ecumenical systems: from natural deduction with stoup to pure modal systems.

See below for more information and the abstract:

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.

In 2015, 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 semantic framework that can be accepted by both parties.  

In this talk, 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.

We then show how to extend these ideas to modalities in the sequent calculus presentation.

This is a joint work with Luiz Carlos Pereira, Sonia Marin and Emerson Sales. 

Zoom link:  https://us02web.zoom.us/j/81225169037?pwd=NWRCWU5GeVNLcnZ4VmlmakZldm0yQT09