On algorithmic expressivity of finite-variable fragments of intuitionistic modal logics

TL;DR

This paper demonstrates that certain intuitionistic modal logics can be efficiently embedded into their simpler one-variable fragments, revealing insights into their expressivity and computational properties.

Contribution

It provides polynomial-time embeddings of FS and MIPC into their positive one-variable fragments, advancing understanding of their algorithmic expressivity.

Findings

Poly-time embeddings of FS and MIPC into one-variable fragments

Enhanced understanding of the algorithmic expressivity of these logics

Potential implications for computational complexity in modal logic

Abstract

We obtain poly-time embeddings of the intuitionistic modal logics FS and MIPC into their positive one-variable fragments.