Polytime embedding of intuitionistic modal logics into their one-variable fragments

Abstract We prove that propositional intuitionistic modal logics $\textbf{FS}$ (also known as $\textbf{IK}$) and $\textbf{MIPC}$ (also known as $\textbf{IS5}$) are polynomial-time embeddable into, and hence polynomial-time equivalent to, their own one-variable fragments. It follows that the one-variable fragment of $\textbf{MIPC}$ is coNEXPTIME-complete. The method of proof applies to a wide range of intuitionistic modal logics characterizable by two-dimensional frames, among them intuitionistic analogues of such classical modal logics as $\textbf{K4}$ and $\textbf{S4}$.