Complexity of finite-variable fragments of propositional modal logics of symmetric frames

TL;DR

This paper investigates how symmetry in propositional modal logics affects the computational complexity of their finite-variable fragments, revealing that symmetry maintains intractability similar to reflexive and transitive frames.

Contribution

It demonstrates that symmetry alone or with reflexivity results in PSPACE-hard finite-variable fragments, clarifying the complexity boundary in modal logics.

Findings

Symmetry alone leads to PSPACE-hard fragments.

Symmetry with reflexivity does not reduce complexity.

Finite-variable fragments of symmetric logics are intractable.

Abstract

While finite-variable fragments of the propositional modal logic S5--complete with respect to reflexive, symmetric and transitive frames--are polynomial-time decidable, the restriction to finite-variable formulas for logics of reflexive and transitive frames yields fragments that remain "intractable." The role of the symmetry condition in this context has not been investigated. We show that symmetry either by itself or in combination with reflexivity produces logics that behave just like logics of reflexive and transitive frames, i.e. their finite-variable fragments remain intractable, namely PSPACE-hard. This raises the question of where exactly the borderline lies between modal logics whose finite-variable fragments are tractable and the rest.