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. While we were not able to provide a satisfactory answer to the question, 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. On the other hand, 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之内。