The Complexity of the Constructive Master Modality

Abstract

We introduce the semantically-defined constructive master-modality logics $\mathsf{C}{\mathsf{K}}^{\ast }$ and $\mathsf{W}{\mathsf{K}}^{\ast }$, extending the basic constructive modal logic $\mathsf{CK}$ and the Wijesekera-style logic $\mathsf{WK}$ obtained by impossing infallibility. Using translations between our logics and fragments of $\mathsf{PDL}$, we show that both $\mathsf{C}{\mathsf{K}}^{\ast }$ and $\mathsf{W}{\mathsf{K}}^{\ast }$ 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 $CS4$ and $WS4$ into the master-modality logics, showing that their validity problems are in EXPTIME.