A Uniform One-Dimensional Fragment with Alternation of Quantifiers

TL;DR

This paper introduces a new variant of the uniform one-dimensional fragment of first-order logic that allows mixed quantifier blocks, maintaining decidability and the finite model property.

Contribution

It defines a novel logic with mixed quantifier blocks that preserves key properties like decidability and finite models, extending previous fragments.

Findings

Retains finite (exponential) model property

Decidable with NExpTime-complete satisfiability

Allows mixing of quantifier blocks

Abstract

The uniform one-dimensional fragment of first-order logic was introduced a few years ago as a generalization of the two-variable fragment of first-order logic to contexts involving relations of arity greater than two. Quantifiers in this logic are used in blocks, each block consisting only of existential quantifiers or only of universal quantifiers. In this paper we consider the possibility of mixing quantifiers in blocks. We identify a non-trivial variation of the logic with mixed blocks of quantifiers which retains some good properties of the two-variable fragment and of the uniform one-dimensional fragment: it has the finite (exponential) model property and hence decidable, NExpTime-complete satisfiability problem.