Unary negation

TL;DR

This paper investigates unary negation fragments of first-order and fixed point logics, establishing their decidability, complexity, and favorable model-theoretic properties, with implications for various logical systems.

Contribution

It proves decidability and complexity results for unary negation fragments, and demonstrates their strong model-theoretic properties, unifying several known formalisms.

Findings

Decidability of satisfiability and finite satisfiability.

Complexity classifications for satisfiability and model checking.

The fragment enjoys Craig Interpolation and the Projective Beth Property.

Abstract

We study fragments of first-order logic and of least fixed point logic that allow only unary negation: negation of formulas with at most one free variable. These logics generalize many interesting known formalisms, including modal logic and the $\mu$-calculus, as well as conjunctive queries and monadic Datalog. We show that satisfiability and finite satisfiability are decidable for both fragments, and we pinpoint the complexity of satisfiability, finite satisfiability, and model checking. We also show that the unary negation fragment of first-order logic is model-theoretically very well behaved. In particular, it enjoys Craig Interpolation and the Projective Beth Property.