将 LREC 与 LFP 分离

LREC= 是一阶逻辑的一种扩展，带有对数递归算子。它由 Grohe 等人引入，并被证明在树和区间图上刻画复杂度类 L。它一般并不能刻画 L，因为它包含于 FPC——带计数的不动点逻辑。我们证明该包含关系是严格的。具体而言，我们证明路径系统问题（一个经典的 P 完全问题，可在 LFP——不动点逻辑——中定义）不能在 LREC= 中定义。这表明对数递归机制可证地弱于一般最小不动点。该证明基于一种为这一逻辑量身定制的新型 Spoiler-Duplicator 博弈。