The Guarded Fragment with Nested Equivalences

TL;DR

This paper extends the Guarded Fragment of first-order logic with nested equivalence relations, proving decidability, finite model property, and establishing tight complexity bounds, while also identifying conditions leading to undecidability.

Contribution

It introduces a new extension of GF with nested equivalences, analyzes its decidability, complexity, and identifies boundaries where satisfiability becomes undecidable.

Findings

GF with nested equivalences has the finite model property.

Decidability of satisfiability is established with tight complexity bounds.

Satisfiability becomes undecidable if nesting is dropped or equality is introduced.

Abstract

The Guarded Fragment (GF) is a well-established decidable fragment of first-order logic. We study an extension of GF with nested equivalence relations, namely a family of distinguished binary predicates $E_1, E_2, \dots$ interpreted as equivalence relations such that $E_{k+1}$ is coarser than $E_k$ for every $k$. We show that the equality-free GF with nested equivalence relations enjoys the finite model property and has a decidable satisfiability problem. Moreover, we establish tight complexity bounds for satisfiability: TOWER-completeness in general, and $(K{+}2)$-ExpTime-completeness when the number of distinguished predicates is fixed to $K$. Finally, we show that satisfiability becomes undecidable if either the nesting condition is dropped (already with two equivalence relations) or equality is admitted (already with a single equivalence relation).