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.

翻译：序不变一阶逻辑是一阶逻辑 FO 的扩展，其中公式可以利用结构上的线性序，但前提是它们具有序不变性，即对于所有线性序，其真值保持不变。我们延续了 Zeume 和 Harwath 对序不变一阶逻辑的双变量片段的研究，探讨其复杂性与表达能力。首先，我们证明了判定给定双变量公式是否具有序不变性的问题是 coNExpTime 完全的，这强化并显著简化了 Zeume 和 Harwath 提出的 coN2ExpTime 证明。其次，我们探讨了序不变双变量逻辑可表达的每个属性是否也可在不使用线性序的一阶逻辑中表达的问题。我们推测答案为“否”。为支持这一观点，我们提出了一类有限树状结构（具有无界度），其中序不变双变量 FO 的松弛变体表达了在普通 FO 中不可定义的属性。相比之下，我们证明若将关注点限制在有限度结构的类别上，则序不变双变量 FO 的表达能力包含在 FO 之内。