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

翻译：守卫片段（GF）是一阶逻辑中一个公认的可判定片段。我们研究带嵌套等价关系的GF扩展，即一族有区别的二元谓词$E_1, E_2, \dots$，它们被解释为等价关系，且对于每个$k$，$E_{k+1}$比$E_k$更粗。我们证明，不带等式的带嵌套等价关系的GF具有有限模型性质，且其可满足性问题可判定。此外，我们建立了可满足性的紧致复杂度界限：一般情况为TOWER-完全，而当有区别谓词数量固定为$K$时为$(K{+}2)$-ExpTime-完全。最后，我们证明，如果去掉嵌套条件（即使只有两个等价关系）或允许等式（即使只有一个等价关系），可满足性将变得不可判定。