Group Order Logic
Anatole Dahan
TL;DR
We introduce FP+ord, extending fixed-point logic with a group-order operator that computes the size of the group generated by a definable set of permutations, broadening the expressive power beyond the rk operator. The paper establishes polynomial-time model-checking for FP+ord and demonstrates its ability to define rk, while showing that FP+ord canonizes structures with Abelian colors, thereby capturing a Lichter-style separation between FP+rk and P on CFIs. A core technical contribution is a morphism-based, isomorphism-invariant representation of labeling cosets, enabling group-theoretic canonization within the logic via morphism-definable subgroups and their intersections. Together, these results position FP+ord as a meaningful advance in the quest for a PTIME-logic and pave the way for new group-theoretic techniques in definable canonization and graph isomorphism contexts.
Abstract
We introduce an extension of fixed-point logic ($\mathsf{FP}$) with a group-order operator ($\mathsf{ord}$), that computes the size of a group generated by a definable set of permutations. This operation is a generalization of the rank operator ($\mathsf{rk}$). We show that $\mathsf{FP} + \mathsf{ord}$ constitutes a new candidate logic for the class of polynomial-time computable queries ($\mathsf{P}$). As was the case for $\mathsf{FP} + \mathsf{rk}$, the model-checking of $\mathsf{FP} + \mathsf{ord}$ formulae is polynomial-time computable. Moreover, the query separating $\mathsf{FP} + \mathsf{rk}$ from $\mathsf{P}$ exhibited by Lichter in his recent breakthrough is definable in $\mathsf{FP} + \mathsf{ord}$. Precisely, we show that $\mathsf{FP} + \mathsf{ord}$ canonizes structures with Abelian colors, a class of structures which contains Lichter's counter-example. This proof involves expressing a fragment of the group-theoretic approach to graph canonization in the logic $\mathsf{FP}+ \mathsf{ord}$.