关于双变量序不变性的表达力与复杂性
计算机科学中的逻辑
2025-04-09 v8
摘要
序不变一阶逻辑是经典一阶逻辑 FO 的扩展，其中公式可利用结构上的线性序，但前提是它们序不变，即对所有线性序其真值相同。我们延续 Zeume 与 Harwath 所开创的序不变一阶逻辑双变量片段的研究，考察其复杂性与表达力。我们首先确立了判定给定双变量公式是否序不变的 coNExpTime 完全性，该结果收紧并显著简化了 Zeume 与 Harwath 的 coN2ExpTime 证明。其次，我们探讨序不变双变量逻辑中可表达的每个性质是否也能在不使用线性序的一阶逻辑中表达这一问题。我们推测答案为“否”。为佐证该主张，我们给出一类有限树状结构（度数无界），其中序不变双变量 FO 的一种松弛变体可表达在普通 FO 中不可定义的性质。相比之下，我们证明若将注意力限制于有界度数结构类，则序不变双变量 FO 的表达力包含于 FO 之中。
引用
@article{arxiv.2304.08410,
title = {About the Expressive Power and Complexity of Order-Invariance with Two Variables},
author = {Bartosz Bednarczyk and Julien Grange},
journal= {arXiv preprint arXiv:2304.08410},
year = {2025}
}
备注
arXiv admin note: text overlap with arXiv:2207.04986