Complexity and Expressivity of Uniform One-Dimensional Fragment with Equality

TL;DR

This paper investigates the complexity and expressivity of the uniform one-dimensional fragment with equality, establishing NEXPTIME-completeness for satisfiability and finite satisfiability, and comparing it with two-variable logic with counting.

Contribution

It proves the NEXPTIME-completeness of satisfiability for UF1^= and shows undecidability when extended with counting quantifiers, also comparing its expressivity with FOC^2.

Findings

Satisfiability and finite satisfiability of UF1^= are NEXPTIME-complete.

Extension of UF1^= with counting quantifiers is undecidable.

UF1^= is strictly contained in FOC^2 for vocabularies with arity two.

Abstract

Uniform one-dimensional fragment UF1^= is a formalism obtained from first-order logic by limiting quantification to applications of blocks of existential (universal) quantifiers such that at most one variable remains free in the quantified formula. The fragment is closed under Boolean operations, but additional restrictions (called uniformity conditions) apply to combinations of atomic formulas with two or more variables. The fragment can be seen as a canonical generalization of two-variable logic, defined in order to be able to deal with relations of arbitrary arities. The fragment was introduced recently, and it was shown that the satisfiability problem of the equality-free fragment of UF1^= is decidable. In this article we establish that the satisfiability and finite satisfiability problems of UF1^= are NEXPTIME-complete. We also show that the corresponding problems for the extension of UF1^= with counting quantifiers are undecidable. In addition to decidability questions, we compare the expressivities of UF1^= and two-variable logic with counting quantifiers FOC^2. We show that while the logics are incomparable in general, UF1^= is strictly contained in FOC^2 when attention is restricted to vocabularies with the arity bound two.