Group Order Logic

We introduce an extension of fixed-point logic (FP) with a group-order operator (ord), that computes the size of a group generated by a definable set of permutations. This operation is a generalization of the rank operator (rk). We show that FP + ord constitutes a new candidate logic for the class of polynomial-time computable queries (P). As was the case for FP + rk, the model-checking of FP + ord formulae is polynomial-time computable. Moreover, the query separating FP + rk from P exhibited by Lichter in his recent breakthrough is definable in FP + ord. Precisely, we show that FP + 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 FP + ord.