Elementary Multimodal Logics

TL;DR

This paper investigates the complexity of multimodal logics over classes of frames defined by first-order formulas, revealing undecidability results even with transitivity constraints.

Contribution

It demonstrates that certain universal Horn formulas can define frame classes where the satisfiability problem remains undecidable, even for bimodal logics with transitive relations.

Findings

Universal Horn formulas can define undecidable frame classes.

Undecidability persists in bimodal logics with transitive relations.

Satisfiability remains undecidable under certain first-order definable classes.

Abstract

We study multimodal logics over universally first-order definable classes of frames. We show that even for bimodal logics, there are universal Horn formulas that define set of frames such that the satisfiability problem is undecidable, even if one or two of the binary relations are transitive.