A Decidable Bundled Fragment of First-Order Modal Logic Without Finite Model Property

TL;DR

This paper identifies a specific decidable fragment of first-order modal logic by analyzing bundled quantifier-modal combinations, expanding understanding of decidability beyond finite model property constraints.

Contribution

It proves that a particular bundled fragment without finite model property is decidable over increasing domain models, refining previous trichotomy results.

Findings

The identified fragment is decidable over increasing domain models.

The paper refines the classification of bundled fragments into a dichotomy.

It extends the understanding of decidability in first-order modal logic.

Abstract

The satisfiability problem for First-order Modal Logic (\FOML) is undecidable even for simple fragments like having only unary predicates, two variables etc. Recently a new way to identify decidable fragments of \FOML has been introduced called the "bundled fragments", where the quantifiers and modalities are restricted to appear together. Since there are many ways to bundle the quantifiers together, some of them lead to (un)decidable fragments. In (Liu et.al, 2023) the authors prove a `trichotomy', where they show that every bundled fragment falls into one of the following three categories: (1) Those that satisfy "finite model property" (and hence decidable), (2) Those that are undecidable, and (3) Those that do not satisfy "finite model property" (whose decidability is left open). In this paper we collapse the trichotomy into a dichotomy over "increasing domain models" by proving that the one combination that falls into the last category is indeed decidable.