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₁, E₂, … 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).