Two-Variable Logic for Hierarchically Partitioned and Ordered Data
Abstract
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.
Cite
@article{arxiv.2512.09508,
title = {Two-Variable Logic for Hierarchically Partitioned and Ordered Data},
author = {Oskar Fiuk and Emanuel Kieronski and Vincent Michielini},
journal= {arXiv preprint arXiv:2512.09508},
year = {2025}
}
Comments
This is an extended version of the paper presented at KR 2025