Bartosz Bednarczyk ; Julien Grange - About the Expressive Power and Complexity of Order-Invariance with Two Variables

lmcs:11206 - Logical Methods in Computer Science, March 28, 2025, Volume 21, Issue 1 - https://doi.org/10.46298/lmcs-21(1:30)2025
About the Expressive Power and Complexity of Order-Invariance with Two VariablesArticle

Authors: Bartosz Bednarczyk ; Julien Grange

    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.


    Volume: Volume 21, Issue 1
    Published on: March 28, 2025
    Accepted on: February 18, 2025
    Submitted on: April 18, 2023
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 80 times.
    This article's PDF has been downloaded 35 times.