Separating Rank Logic from Polynomial Time

TL;DR

The paper demonstrates that rank logic cannot define the isomorphism problem for certain graphs, while Choiceless Polynomial Time can, thereby separating the expressive power of these two logics in capturing polynomial time.

Contribution

It establishes a separation between rank logic and CPT by showing rank logic's limitations in defining specific graph isomorphism problems.

Findings

Rank logic cannot define isomorphism for CFI graphs over Z_{2^i}.

CPT can define the isomorphism problem for these graphs.

This separation clarifies the expressive boundaries of rank logic versus CPT.

Abstract

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.