# Unary negation

arXiv: https://arxiv.org/abs/1309.2069 · HTML: https://mlsanity.com/paper/1309.2069/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 9 Sep 2013.

## Built on by (most cited first, 4 of 4)

- [Satisfiability and Containment of Recursive SHACL](https://mlsanity.com/paper/2108.13063/) (2021)
- [Ontology-Mediated Querying on Databases of Bounded Cliquewidth](https://mlsanity.com/paper/2205.02190/) (2022)
- [Decidability of Querying First-Order Theories via Countermodels of Finite Width](https://mlsanity.com/paper/2304.06348/) (2023)
- [Description Logics with Abstraction and Refinement](https://mlsanity.com/paper/2306.03717/) (2023)

## Abstract (arXiv)

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 μ-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.