Two-Variable Logic for Hierarchically Partitioned and Ordered Data

TL;DR

This paper investigates the computational complexity of two-variable first-order logic over hierarchically structured data, revealing NExpTime-completeness and undecidability results for various extensions involving orders and equivalence relations.

Contribution

It introduces new logical frameworks modeling hierarchical data and establishes complexity bounds and decidability results for their satisfiability problems.

Findings

Finite satisfiability for extended FO2 with order is NExpTime-complete.

Weaker variants without order have the exponential model property.

Adding successor relations increases complexity to ExpSpace-complete.

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.