On Generalizing Decidable Standard Prefix Classes of First-Order Logic

TL;DR

This paper introduces new decidable classes of first-order logic by relaxing variable occurrence restrictions, enabling broader fragments while maintaining decidability through translations and model-theoretic methods.

Contribution

It generalizes the separated fragment by allowing certain variable co-occurrences and defines a novel fragment with decidable satisfiability that extends known classes.

Findings

Decidability of satisfiability for the relaxed separated fragment.

Introduction of a new decidable fragment containing Ackermann and monadic fragments.

Effective translations into BSR and monadic fragments established.

Abstract

Recently, the separated fragment (SF) of first-order logic has been introduced. Its defining principle is that universally and existentially quantified variables may not occur together in atoms. SF properly generalizes both the Bernays-Sch\"onfinkel-Ramsey (BSR) fragment and the relational monadic fragment. In this paper the restrictions on variable occurrences in SF sentences are relaxed such that universally and existentially quantified variables may occur together in the same atom under certain conditions. Still, satisfiability can be decided. This result is established in two ways: firstly, by an effective equivalence-preserving translation into the BSR fragment, and, secondly, by a model-theoretic argument. Slight modifications to the described concepts facilitate the definition of other decidable classes of first-order sentences. The paper presents a second fragment which is novel, has a decidable satisfiability problem, and properly contains the Ackermann fragment and---once more---the relational monadic fragment. The definition is again characterized by restrictions on the occurrences of variables in atoms. More precisely, after certain transformations, Skolemization yields only unary functions and constants, and every atom contains at most one universally quantified variable. An effective satisfiability-preserving translation into the monadic fragment is devised and employed to prove decidability of the associated satisfiability problem.