Ecumenical modal logic

TL;DR

This paper extends the ecumenical approach to modal logic, combining classical and intuitionistic systems with alethic K-modalities within a unified framework.

Contribution

It introduces a novel ecumenical modal logic system that integrates classical and intuitionistic modalities with a shared semantic foundation.

Findings

Established proof-theoretic properties of the new system

Demonstrated compatibility of classical and intuitionistic modalities

Extended Prawitz's ecumenical framework to modal logic

Abstract

The discussion about how to put together Gentzen's systems for classical and intuitionistic logic in a single unified system is back in fashion. Indeed, recently Prawitz and others have been discussing the so called Ecumenical Systems, where connectives from these logics can co-exist in peace. In Prawitz' 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 a recent work, Ecumenical sequent calculi and a nested system were presented, and some very interesting proof theoretical properties of the systems were established. In this work we extend Prawitz' Ecumenical idea to alethic K-modalities.