Wijesekera-style constructive modal logics

TL;DR

This paper introduces a family of propositional constructive modal logics aligned with classical modal systems, combining proof-theoretic and semantic approaches to ensure consistency and constructive validity.

Contribution

It defines new constructive modal logics based on Wijesekera's style, integrating hereditariness of intuitionistic models with classical modal satisfaction clauses.

Findings

Proof-theoretic and semantic approaches yield the same constructive systems.

The logics correspond to single-succedent restrictions of classical modal sequent calculi.

The systems incorporate hereditariness into satisfaction clauses.

Abstract

We define a family of propositional constructive modal logics corresponding each to a different classical modal system. The logics are defined in the style of Wijesekera's constructive modal logic, and are both proof-theoretically and semantically motivated. On the one hand, they correspond to the single-succedent restriction of standard sequent calculi for classical modal logics. On the other hand, they are obtained by incorporating the hereditariness of intuitionistic Kripke models into the classical satisfaction clauses for modal formulas. We show that, for the considered classical logics, the proof-theoretical and the semantical approach return the same constructive systems.