Logics with the axiom of convergence: complexity with a small number of variables in the language (extended version)

TL;DR

This paper examines the computational complexity of specific modal logic fragments with convergence axioms, revealing PSPACE-completeness in small-variable languages for several logics, and extends these results to broader classes.

Contribution

It establishes PSPACE-completeness of convergence-axiom modal logic fragments with limited variables, filling a gap in understanding their complexity.

Findings

S4.2 and Grz.2 are PSPACE-complete with two variables

K4.2 and GL.2* are PSPACE-complete with one variable

Results extend to infinite classes of related logics

Abstract

It is known that many modal and superintuitionistic logics are PSPACE-hard in languages with a small number of variables; however, questions about the complexity of similar fragments of many logics obtained by adding various axioms to "standard" ones remain unexplored. We investigate the complexity of fragments of modal logics obtained by adding an axiom requiring the convergence of the accessibility relation in Kripke frames: S4.2, K4.2, Grz.2, and GL.2. The main result is that S4.2 and Grz.2 are PSPACE-complete in a language with two variables, while K4.2 and GL.2* (a logic near to GL.2) are PSPACE-complete in a language with one variable. The obtained results are extended to infinite classes of logics.