等级逻辑已死，等级逻辑万岁！
Rank logic is dead, long live rank logic!
摘要：
出于寻找多项式时间的逻辑的动机，我们研究了秩逻辑（FPR），它通过确定有限域上矩阵秩的算子来扩展计数不动点逻辑（FPC）。虽然FPR可以表达大多数将FPC与PTIME分开的已知查询，但几乎没有人知道它的表达能力的局限性。在我们的第一个主要结果中，我们证明了FPC的秩算子在不同素域上的扩张是不可比较的。这解决了Dawar和Holm提出的一个公开问题，也意味着秩逻辑在其原始定义中每个字段都有一个不同的秩运算符，无法捕获多项式时间。特别是，我们证明了秩逻辑FPR* 的变体与一个运营商，一致表示矩阵秩在有限域上是更有表现力的FPR。在我们的证明中的一个重要步骤是考虑可解性逻辑FPS这是类似的扩展FPC的量词表示可解性问题的线性方程组在有限域上。可解性逻辑可以很容易地嵌入到秩逻辑中，但它是否是严格片段是开放的。在我们的第二个主要结果中，我们给出了这个问题的部分答案：在没有计数的情况下，秩算子比可解性量词更严格地表达。
英文摘要：
Motivated by the search for a logic for polynomial time, we study rank logic (FPR) which extends fixed-point logic with counting (FPC) by operators that determine the rank of matrices over finite fields. While FPR can express most of the known queries that separate FPC from PTIME, nearly nothing was known about the limitations of its expressive power. In our first main result we show that the extensions of FPC by rank operators over different prime fields are incomparable. This solves an open question posed by Dawar and Holm and also implies that rank logic, in its original definition with a distinct rank operator for every field, fails to capture polynomial time. In particular we show that the variant of rank logic FPR* with an operator that uniformly expresses the matrix rank over finite fields is more expressive than FPR. One important step in our proof is to consider solvability logic FPS which is the analogous extension of FPC by quantifiers which express the solvability problem for linear equation systems over finite fields. Solvability logic can easily be embedded into rank logic, but it is open whether it is a strict fragment. In our second main result we give a partial answer to this question: in the absence of counting, rank operators are strictly more expressive than solvability quantifiers.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
