Separating Rank Logic from Polynomial Time

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.

54 pages. Full version of a paper appeared at LICS 2021. [v3] Fixed some minor mistakes/typos in the proofs [v4] Fixed a mistake in the CFI construction [v5] added more details in some proofs, corrected minor mistakes

References in corpus (1)

• Canonization for Bounded and Dihedral Color Classes in Choiceless Polynomial Time

Cited by in corpus (3)

• Choiceless Polynomial Time, Symmetric Circuits and Cai-Fürer-Immerman Graphs
• Group Order Logic
• Compressing CFI Graphs and Lower Bounds for the Weisfeiler-Leman Refinements