Unary negation fragment with equivalence relations has the finite model property

TL;DR

This paper proves that extending the unary negation fragment of first-order logic with equivalence relations retains the finite model property, with models of at most doubly exponential size, and establishes the complexity of satisfiability.

Contribution

It demonstrates that the extended unary negation fragment with equivalence relations has the finite model property and characterizes the complexity of its satisfiability problem.

Findings

Every satisfiable formula has a doubly exponential size model.

The satisfiability problem is TwoExpTime-complete.

Results extend to a restricted guarded negation fragment.

Abstract

We consider an extension of the unary negation fragment of first-order logic in which arbitrarily many binary symbols may be required to be interpreted as equivalence relations. We show that this extension has the finite model property. More specifically, we show that every satisfiable formula has a model of at most doubly exponential size. We argue that the satisfiability (= finite satisfiability) problem for this logic is TwoExpTime-complete. We also transfer our results to a restricted variant of the guarded negation fragment with equivalence relations.