Two-Variable Logic for Hierarchically Partitioned and Ordered Data

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.

Paper

Similar papers

© 2026 NYSGPT2525 LLC