Separability and harmony in ecumenical systems

TL;DR

This paper develops a pure sequent calculus for ecumenical first-order logic, integrating classical and intuitionistic connectives, and extends the framework to handle modalities with labeled and nested systems.

Contribution

It introduces a pure sequent calculus for ecumenical logic with polarities and extends it to ecumenical modal logics, advancing the formal foundations.

Findings

Successfully defines a pure sequent calculus with an extended context and polarities.

Extends the calculus to ecumenical modal logics with labeled and nested systems.

Provides a formal framework for combining classical and intuitionistic logics in a unified system.

Abstract

The quest of smoothly combining logics so that connectives from classical and intuitionistic logics can co-exist in peace has been a fascinating topic of research for decades now. In 2015, Dag Prawitz proposed a natural deduction system for an ecumenical first-order logic. We start this work by proposing a {\em pure} sequent calculus version for it, in the sense that connectives are introduced without the use of other connectives. For doing this, we extend sequents with an extra context, the stoup, and define the ecumenical notion of polarities. Finally, we smoothly extend these ideas for handling modalities, presenting pure labeled and nested systems for ecumenical modal logics.