We study Two-Variable First-Order Logic, FO2, under semantic constraints that model hierarchically structured data. Our first logic extends FO2 with a linear order < and a chain of increasingly coarser equivalence relations E_1, E_2, ... . We show that its finite satisfiability problem is NExpTime-complete. We also demonstrate that a weaker variant of this logic without the linear order enjoys the exponential model property. Our second logic extends FO2 with a chain of nested total preorders. We prove that its finite satisfiability problem is also NExpTime-complete.However, we show that the complexity increases to ExpSpace-complete once access to the successor relations of the preorders is allowed. Our last result is the undecidability of FO2 with two independent chains of nested equivalence relations.

翻译：我们研究了在建模层次化结构化数据的语义约束下的二变量一阶逻辑（FO2）。我们的第一种逻辑将FO2扩展为包含线性序<以及一系列逐渐粗化的等价关系链E_1、E_2、...。我们证明了其有限可满足性问题为NExpTime完全。我们还展示了该逻辑的一个较弱变体（不含线性序）具有指数模型性质。我们的第二种逻辑将FO2扩展为包含一系列嵌套全预序链。我们证明了其有限可满足性问题同样为NExpTime完全。然而，一旦允许访问预序的后继关系，其复杂度将上升至ExpSpace完全。我们的最后一项结果是：具有两个独立嵌套等价关系链的FO2是不可判定的。