We study the decidability of modal satisfiability over classes of Kripke frames defined by universal first-order sentences. Although some such classes yield undecidable satisfiability problems, decidability is guaranteed for wide families of frame conditions, including universal Horn sentences and universal sentences implying transitivity. A more than decade-old open problem asks a natural question: can decidable and undecidable cases be distinguished algorithmically? We prove that this is impossible, already for equality-free universal frame conditions over a single binary relation. More precisely, there is no algorithm that, given such a condition, decides whether its associated local modal satisfiability problem is decidable. We first establish the result for conditions with equality and then eliminate equality by passing to quotients of worlds with identical incoming and outgoing edges.

翻译：暂无翻译