Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Two-Variable Logic for Hierarchically Partitioned and Ordered Data

Oskar Fiuk, Emanuel Kieronski, Vincent Michielini

TL;DR

The paper investigates two-variable first-order logic (FO2) extended with hierarchical data tests: (i) FO2[<,EQ⊆] uses a linear order plus nested equivalence relations E1 ⊆ E2 ⊆ … to model multi-level data; (ii) FO2[≼⊆] uses nested total preorders to capture multi-granularity data values, with and without successive predicates. It proves a precise set of complexity and model properties: finite satisfiability for FO2[<,EQ⊆] is NExpTime-complete with exponential-size models; FO2[≼⊆] likewise has NExpTime-complete finite satisfiability; adding successor predicates to FO2[≼⊆] raises the problem to ExpSpace-complete, while a further variant demonstrates doubly exponential model properties. A crucial negative result shows undecidability for FO2 with two independent chains of nested equivalence relations. The proofs hinge on Scott Normal Form reductions, a central replacement lemma that bounds the size of equivalence classes by carefully controlling witnesses and 2-types, and a space-efficient decision procedure for the successor-augmented preorder variant, complemented by reductions from corridor tiling for hardness. The work clarifies the boundary between decidability and undecidability in FO2 over hierarchically structured data and provides concrete complexity bounds and model-size guarantees that inform reasoning tasks over multi-level data hierarchies and data words.

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.

Two-Variable Logic for Hierarchically Partitioned and Ordered Data

TL;DR

The paper investigates two-variable first-order logic (FO2) extended with hierarchical data tests: (i) FO2[<,EQ⊆] uses a linear order plus nested equivalence relations E1 ⊆ E2 ⊆ … to model multi-level data; (ii) FO2[≼⊆] uses nested total preorders to capture multi-granularity data values, with and without successive predicates. It proves a precise set of complexity and model properties: finite satisfiability for FO2[<,EQ⊆] is NExpTime-complete with exponential-size models; FO2[≼⊆] likewise has NExpTime-complete finite satisfiability; adding successor predicates to FO2[≼⊆] raises the problem to ExpSpace-complete, while a further variant demonstrates doubly exponential model properties. A crucial negative result shows undecidability for FO2 with two independent chains of nested equivalence relations. The proofs hinge on Scott Normal Form reductions, a central replacement lemma that bounds the size of equivalence classes by carefully controlling witnesses and 2-types, and a space-efficient decision procedure for the successor-augmented preorder variant, complemented by reductions from corridor tiling for hardness. The work clarifies the boundary between decidability and undecidability in FO2 over hierarchically structured data and provides concrete complexity bounds and model-size guarantees that inform reasoning tasks over multi-level data hierarchies and data words.

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.

Paper Structure

This paper contains 16 sections, 17 theorems, 57 equations, 1 figure, 1 algorithm.

Table of Contents

  1. Introduction
  2. Logics of Interest and Our Results
  3. Related Work
  4. Expressivity of $\hbox{\rm FO}^2$$[<,{\mathcal{EQ}}^{\scaleto{\subseteq}{5pt}}]$ and $\hbox{\rm FO}^2$$[{\preceq}^{\scaleto{\subseteq}{5pt}}]$
  5. Outline of Technical Sections
  6. Preliminaries
  7. Notation and Conventions
  8. Scott Normal Form
  9. Proof of Theorem \ref{['t:two']}
  10. How to show Theorems \ref{['t:three']} and \ref{['t:one']}
  11. Proof of Theorem \ref{['t:four']}
  12. Proof of Theorem \ref{['t:und']}
  13. Conclusion
  14. Additional Details on Theorems \ref{['t:three']} and \ref{['t:one']}
  15. Proof of Lemma \ref{['l:pumping']}
  16. ...and 1 more sections

Key Result

Theorem 1

Finitely satisfiable sentences of $\hbox{\rm FO}^2$$[<,{\mathcal{EQ}}^{\scaleto{\subseteq}{5pt}}]$ admit models of exponential size. The finite satisfiability problem for $\hbox{\rm FO}^2$$[<,{\mathcal{EQ}}^{\scaleto{\subseteq}{5pt}}]$ is NExpTime-complete.

Figures (1)

  • Figure 1: A succession of configurations.

Theorems & Definitions (33)

  • Theorem 1
  • Theorem 2
  • Theorem 3
  • Theorem 4
  • Theorem 5
  • Theorem 5
  • Lemma 6
  • proof : Proof of Theorem \ref{['t:two']}
  • Claim 7
  • proof
  • ...and 23 more