# On the Strength of Uniqueness Quantification in Primitive Positive Formulas

## TL;DR

This paper analyzes the logical strength of uniqueness quantification in primitive positive formulas, classifies when it matches existential quantification, and applies these findings to complexity problems like unique satisfiability.

## Contribution

It provides a complete classification of relation sets where uniqueness quantification equals existential quantification in primitive positive formulas and applies this to complexity theory.

## Key findings

- Classified Boolean relation sets where uniqueness equals existential quantification.
- Provided simplified proof of the trichotomy theorem for unique satisfiability.
- Proved a general result for the unique constraint satisfaction problem.

## Abstract

Uniqueness quantification ($\exists !$) is a quantifier in first-order logic where one requires that exactly one element exists satisfying a given property. In this paper we investigate the strength of uniqueness quantification when it is used in place of existential quantification in conjunctive formulas over a given set of relations $\Gamma$, so-called primitive positive definitions (pp-definitions). We fully classify the Boolean sets of relations where uniqueness quantification has the same strength as existential quantification in pp-definitions and give several results valid for arbitrary finite domains. We also consider applications of $\exists !$-quantified pp-definitions in computer science, which can be used to study the computational complexity of problems where the number of solutions is important. Using our classification we give a new and simplified proof of the trichotomy theorem for the unique satisfiability problem, and prove a general result for the unique constraint satisfaction problem.