Modelling of logical systems by means of their fragments

TL;DR

This paper explores how non-classical logics can be simplified by reducing their complexity to smaller fragments, revealing conditions for such reductions and establishing new complexity bounds and incompleteness results.

Contribution

It introduces conditions for reducing superintuitionistic and modal logics to their smaller fragments and provides new complexity bounds and incompleteness results for predicate calculi.

Findings

Propositional logics are reducible to small variable fragments with polynomial-time algorithms.

Predicate logics can be reduced to fragments with unary predicates and few variables.

New complexity bounds and Kripke-incompleteness results for certain logics.

Abstract

This work investigates the algorithmic complexity of non-classical logics, focusing on superintuitionistic and modal systems. It is shown that propositional logics are usually polynomial-time reducible to their fragments with at most two variables (often to the one-variable or even variable-free fragments). Also, it is proved that predicate logics are usually reducible to their fragments with one or two unary predicate letters and two or three individual variables. The work describes conditions sufficient for such reductions and provides examples where they fail, establishing non-reducibility in those cases. Furthermore, the work provides new complexity bounds for several logics, results on Kripke-incompleteness of predicate calculi, and analogues of the classical theorems of Church and Trakhtenbrot for the logic of quasiary predicates.