The Guarded Fragment with Nested Equivalences
Provides foundational complexity results for a decidable fragment of first-order logic with equivalence relations, relevant to logic and database theory.
The paper studies the guarded fragment of first-order logic extended with nested equivalence relations, proving decidability and tight complexity bounds (TOWER-complete in general, (K+2)-ExpTime-complete for fixed K) for the equality-free case, and undecidability when nesting is dropped or equality is added.
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).