A Simplest Undecidable Modal Logic

TL;DR

This paper demonstrates that even highly restricted, seemingly simple modal logics can be undecidable, highlighting fundamental limits in the computational complexity of modal satisfiability problems.

Contribution

It introduces an undecidable modal logic derived from models constrained by a universal quantifier-only first-order formula, revealing undecidability in simple modal systems.

Findings

Existence of an undecidable modal logic with universal-quantifier restrictions

Undecidability persists despite restrictions to simple model classes

Highlights limits of decidability in modal logic complexity

Abstract

Modal logics are widely used in computer science. The complexity of their satisfiability problems has been an active field of research since the 1970s. We prove that even very "simple" modal logics can be undecidable: We show that there is an undecidable modal logic that can be obtained by restricting the allowed models with a first-order formula in which only universal quantifiers appear.