一句话：证明二变量序不变 FO 的序不变性判定是 coNExpTime 完全的，并刻画其表达能力。
本文研究二变量序不变一阶逻辑（order-invariant FO^2）的复杂度与表达力。序不变一阶逻辑允许公式使用结构上的线性序，但要求真值不依赖具体序。作者首先证明判定给定二变量公式是否序不变的问题为 coNExpTime 完全，改进并简化了此前 coN2ExpTime 的上界。其次，论文探讨序不变 FO^2 是否严格强于普通 FO；他们给出无界度有限树状结构类，在其中一种放松的序不变 FO^2 能表达普通 FO 不可定义的性质，从而支持答案为否；同时证明在有界度结构类上，序不变 FO^2 的表达力不超出 FO。
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.Comment: arXiv admin note: text overlap with arXiv:2207.04986
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2304-08410,
title = {About the Expressive Power and Complexity of Order-Invariance with Two Variables},
author = {Bartosz Bednarczyk and Julien Grange},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 1},
year = {2025},
doi = {10.46298/lmcs-21(1:30)2025}
}