Minimal modal logics, constructive modal logics and their relations

TL;DR

This paper introduces a family of minimal modal logics derived from classical modal logics, explores their relationships with constructive modal logic CK, and establishes equivalences between different construction methods.

Contribution

It defines minimal modal logics via two methods, proves their equivalence, and relates these to existing constructive modal logic CK, expanding the understanding of constructive modal systems.

Findings

The two construction methods are equivalent for many modal systems.

Minimal modal logics are tightly related to the constructive modal logic CK.

A family of constructive modal logics extending CK is established.

Abstract

We present a family of minimal modal logics (namely, modal logics based on minimal propositional logic) corresponding each to a different classical modal logic. The minimal modal logics are defined based on their classical counterparts in two distinct ways: (1) via embedding into fusions of classical modal logics through a natural extension of the G\"odel-Johansson translation of minimal logic into modal logic S4; (2) via extension to modal logics of the multi- vs. single-succedent correspondence of sequent calculi for classical and minimal logic. We show that, despite being mutually independent, the two methods turn out to be equivalent for a wide class of modal systems. Moreover, we compare the resulting minimal version of K with the constructive modal logic CK studied in the literature, displaying tight relations among the two systems. Based on these relations, we also define a constructive correspondent for each minimal system, thus obtaining a family of constructive modal logics which includes CK as well as other constructive modal logics studied in the literature.