The Complexity of the Constructive Master Modality

TL;DR

This paper introduces new constructive master-modality logics, proves their EXPTIME-completeness, and demonstrates their applicability by embedding other modal logics, thus advancing understanding of their computational complexity.

Contribution

It defines the semantically-based logics $ extsf{CK}^*$ and $ extsf{WK}^*$, establishes their EXPTIME-completeness, and applies these results to embed and analyze other modal logics.

Findings

Both $ extsf{CK}^*$ and $ extsf{WK}^*$ are EXPTIME-complete.

Their diamond-free fragments are also EXPTIME-complete.

Embedding $ extsf{CS4}$ and $ extsf{WS4}$ into these logics shows their validity problems are in EXPTIME.

Abstract

We introduce the semantically-defined constructive master-modality logics $\sf CK^*$ and $\sf WK^*$, extending the basic constructive modal logic $\sf CK$ and the Wijesekera-style logic $\sf WK$ obtained by impossing infallibility. Using translations between our logics and fragments of $\sf PDL$, we show that both $\sf CK^*$ and $\sf WK^*$ are EXPTIME-complete and admit an exponential-size finite model property. In particular, for their diamond-free fragment, also studied by Afshari et al. and Celoni, we establish EXPTIME-completeness, thereby settling the conjecture of Afshari et al. As an application, we embed $\sf CS4$ and $\sf WS4$ into the master-modality logics, showing that their validity problems are in EXPTIME.