In the search for a logic capturing polynomial time the most promising candidates are Choiceless Polynomial Time (CPT) and rank logic. Rank logic extends fixed-point logic with counting by a rank operator over prime fields. We show that the isomorphism problem for CFI graphs over $\mathbb{Z}_{2^i}$ cannot be defined in rank logic, even if the base graph is totally ordered. However, CPT can define this isomorphism problem. We thereby separate rank logic from CPT and in particular from polynomial time.

翻译：在寻找能刻画多项式时间的逻辑的过程中，最有希望的候选者是“无选择多项式时间”（CPT）与“秩逻辑”。秩逻辑通过在素数域上引入秩算子，扩展了具有计数功能的定点逻辑。我们证明，即使基础图是全序的，$\mathbb{Z}_{2^i}$ 上 CFI 图的同构问题也无法在秩逻辑中定义。然而，CPT 能够定义这个同构问题。由此，我们将秩逻辑与 CPT 分离，特别是与多项式时间分离。