带计数的不动点逻辑中的见证对称选择与解释
计算机科学中的逻辑
2026-04-14 v8 逻辑
摘要
在寻求PTime逻辑的核心处，是进行任意选择的算法与同构不变逻辑之间的不匹配。克服此问题的一种方法是见证对称选择（witnessed symmetric choice）。它允许从可定义轨道中进行选择，并由可定义的见证自同构所认证。我们考虑带计数的不动点逻辑（IFPC）加上见证对称选择（IFPC+WSC）的扩展，以及进一步带有解释算子（IFPC+WSC+I）的扩展。后一算子在由解释定义的结构中求值子公式。该结构可能具有可被WSC算子利用的其他自同构。对于纯不动点逻辑（IFP）的类似扩展，已知IFP+WSCI可模拟计数，而IFP+WSC做不到。对于IFPC+WSC，解释算子是否增加表达能力从而允许在计数之外研究WSC与解释之间的关系尚属未知。我们通过证明IFPC+WSC在FO解释下不封闭，将IFPC+WSC与IFPC+WSCI区分开。此外，我们利用所谓的CFI图证明嵌套WSC算子可增加表达能力。我们证明若IFPC+WSC+I规范化一类特定的基图，则它也规范化相应的CFI图。这与各种其他逻辑不同，在那些逻辑中CFI图提供了困难实例。
引用
@article{arxiv.2210.07869,
title = {Witnessed Symmetric Choice and Interpretations in Fixed-Point Logic with Counting},
author = {Moritz Lichter},
journal= {arXiv preprint arXiv:2210.07869},
year = {2026}
}
备注
51 pages, 7 figures, [v2], [v3], [v4] Corrected minor mistakes, added figures, and some smaller improvements, [v5] typos, [v6] added lmcs style file, [v7] corrected an issue with the reduct semantics, [v8] replaced some proof sketches with full proofs