Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

About the Expressive Power and Complexity of Order-Invariance with Two Variables

Bartosz Bednarczyk, Julien Grange

TL;DR

This work analyzes the order-invariant two-variable fragment of first-order logic over finite structures. It proves a tight coNExpTime-complete bound for deciding order-invariance of FO^2 formulas and shows a nuanced separation: order-invariant FO^2 can express properties beyond FO on certain tree-like classes, yet on classes of bounded degree its expressive power collapses to FO without using the linear order. The key technique is a neighbourhood-type locality framework that classifies local structures and enables a controlled transfer of orderings; for bounded degree, this yields an FO-equivalence with a computable bound. The results have implications for understanding when adding invariant order to FO yields genuine expressive gain, and they extend to the counting variant C^2 with preserved boundedness consequences. Overall, the paper advances both the complexity-theoretic and model-theoretic understanding of order-invariant logics in finite model theory.

Abstract

Order-invariant first-order logic is an extension of first-order logic FO where formulae can make use of a linear order on the structures, under the proviso that they are order-invariant, i.e. that their truth value is the same for all linear orders. We continue the study of the two-variable fragment of order-invariant first-order logic initiated by Zeume and Harwath, and study its complexity and expressive power. We first establish coNExpTime-completeness for the problem of deciding if a given two-variable formula is order-invariant, which tightens and significantly simplifies the coN2ExpTime proof by Zeume and Harwath. Second, we address the question of whether every property expressible in order-invariant two-variable logic is also expressible in first-order logic without the use of a linear order. We suspect that the answer is ``no''. To justify our claim, we present a class of finite tree-like structures (of unbounded degree) in which a relaxed variant of order-invariant two-variable FO expresses properties that are not definable in plain FO. By contrast, we show that if one restricts their attention to classes of structures of bounded degree, then the expressive power of order-invariant two-variable FO is contained within FO.

About the Expressive Power and Complexity of Order-Invariance with Two Variables

TL;DR

This work analyzes the order-invariant two-variable fragment of first-order logic over finite structures. It proves a tight coNExpTime-complete bound for deciding order-invariance of FO^2 formulas and shows a nuanced separation: order-invariant FO^2 can express properties beyond FO on certain tree-like classes, yet on classes of bounded degree its expressive power collapses to FO without using the linear order. The key technique is a neighbourhood-type locality framework that classifies local structures and enables a controlled transfer of orderings; for bounded degree, this yields an FO-equivalence with a computable bound. The results have implications for understanding when adding invariant order to FO yields genuine expressive gain, and they extend to the counting variant C^2 with preserved boundedness consequences. Overall, the paper advances both the complexity-theoretic and model-theoretic understanding of order-invariant logics in finite model theory.

Abstract

Order-invariant first-order logic is an extension of first-order logic FO where formulae can make use of a linear order on the structures, under the proviso that they are order-invariant, i.e. that their truth value is the same for all linear orders. We continue the study of the two-variable fragment of order-invariant first-order logic initiated by Zeume and Harwath, and study its complexity and expressive power. We first establish coNExpTime-completeness for the problem of deciding if a given two-variable formula is order-invariant, which tightens and significantly simplifies the coN2ExpTime proof by Zeume and Harwath. Second, we address the question of whether every property expressible in order-invariant two-variable logic is also expressible in first-order logic without the use of a linear order. We suspect that the answer is ``no''. To justify our claim, we present a class of finite tree-like structures (of unbounded degree) in which a relaxed variant of order-invariant two-variable FO expresses properties that are not definable in plain FO. By contrast, we show that if one restricts their attention to classes of structures of bounded degree, then the expressive power of order-invariant two-variable FO is contained within FO.
Paper Structure (22 sections, 19 theorems, 34 equations, 1 figure, 1 algorithm)

This paper contains 22 sections, 19 theorems, 34 equations, 1 figure, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Order-invariance
  4. Definability and similarity
  5. The two-pebble Ehrenfeucht-Fraïssé game
  6. Complexity of the invariance problem
  7. Can order-invariant $\textsc{FO}\xspace^2\xspace\xspace$ express properties beyond the scope of $\textsc{FO}$?
  8. Expressive power when the degree is bounded
  9. Overview of the result
  10. Neighbourhoods
  11. Definition and properties of neighbourhoods
  12. Frequency of a neighbourhood type
  13. Constructing linear orders on A0 and A1
  14. Proof of the FO2-similarity of (A0,<0) and (A1,<1)
  15. Base case: proofs of (Sk), (Ek) and (Rk)
  16. ...and 7 more sections

Key Result

Theorem 2.1

DBLP:journals/iandc/ImmermanK89 If the duplicator has a winning strategy in the $k$-round two-pebble Ehrenfeucht-Fraïssé game on $\mathcal{A}_0$ and $\mathcal{A}_1$, then $\mathcal{A}_0\xspace\equiv^{{\textsc{FO}\xspace^2\xspace}}_{k}\mathcal{A}_1\xspace\,.$

Figures (1)

  • Figure 1: Elements from two distinct segments can only be adjacent if there is a black curvy edge between those segments. The order $<$ grows from the left to the right. Note that $N\!R_{0}^{0}$ is empty and thus left out of the picture.

Theorems & Definitions (35)

  • Theorem 2.1
  • Lemma 3.1
  • proof
  • Theorem 3.2
  • Definition 3.4
  • Lemma 3.5
  • proof : Proof sketch.
  • Lemma 3.6
  • proof
  • Theorem 3.7
  • ...and 25 more