# Decidable fragments of first-order modal logics with counting quantifiers over varying domains

## TL;DR

This paper analyzes the computational complexity of one-variable fragments of first-order modal logics with counting quantifiers over varying domains, providing tight bounds for satisfiability problems in different settings.

## Contribution

It establishes optimal complexity bounds for the satisfiability of these fragments, including cases with binary and unary encoding of counting quantifiers over different domain types.

## Key findings

- Optimal NExpTime upper bounds for minimal first-order modal logic QK with counting quantifiers.
- PSpace-completeness for unary-encoded counting quantifiers over expanding domains.
- ExpTime-hardness for decreasing domains with unary-encoded counting quantifiers.

## Abstract

This paper explores the computational complexity of various natural one-variable fragments of first-order modal logics with the addition of counting quantifiers, over both constant and varying domains. The addition of counting quantifiers provides us a rich language with which to succinctly express statements about the quantity of objects satisfying a given first-order property, using a single variable. Optimal NExpTime upper-bounds are provided for the satisfiability problems of the one-variable fragment of the minimal first-order modal logic QK, over both constant and expanding/decreasing domain models, where counting quantifiers are encoded as binary strings. For the case where the counting quantifiers are encoded as unary strings, or are restricted to a finite set of quantifiers, it is shown that the satisfiability problem over expanding domains is PSpace-complete, whereas over decreasing domains the problem is shown to be ExpTime-hard.