The Guarded Fragment with Nested Equivalences

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