两变量一阶逻辑片段中带计数量的分离与可定义性
计算机科学中的逻辑
2025-08-18 v3
摘要
对于带计数量的第一阶逻辑 (FO) 的片段 L，我们考虑可定义性问题，即给定的 L 公式是否可以等价地表示为不含计数量的 L 某片段中的公式，以及更一般的分离问题，即两个互不相容的 L 公式是否可以在不含计数量的 L 某片段中被分离。我们证明，对于带计数量的两变量片段 FO 以及带逆向、名词和全模态的格拉德模态逻辑，分离是不可判定的。相反，如果去除逆向或名词，分离问题则变为共指数时间或双指数时间完备，具体取决于是否存在全模态。在 contrast 中，可定义性通常可以多项式时间内化约为 L 中的有效性问题。我们也考虑了统一分离问题，表明其往往类似于可定义性。
引用
@article{arxiv.2504.20491,
title = {Separation and Definability in Fragments of Two-Variable First-Order Logic with Counting},
author = {Louwe Kuijer and Tony Tan and Frank Wolter and Michael Zakharyaschev},
journal= {arXiv preprint arXiv:2504.20491},
year = {2025}
}
备注
The article has been accepted for LICS 2025