Witnessed Symmetric Choice and Interpretations in Fixed-Point Logic with Counting

At the core of the quest for a logic for PTime is a mismatch between algorithms making arbitrary choices and isomorphism-invariant logics. One approach to overcome this problem is witnessed symmetric choice. It allows for choices from definable orbits which are certified by definable witnessing automorphisms. We consider the extension of fixed-point logic with counting (IFPC) with witnessed symmetric choice (IFPC+WSC) and a further extension with an interpretation operator (IFP+WSC+I). The latter operator evaluates a subformula in the structure defined by an interpretation. This structure possibly has other automorphisms exploitable by the WSC-operator. For similar extensions of pure fixed-point logic (IFP) it is known that IFP+WSC+I simulates counting which IFP+WSC fails to do. For IFPC it is unknown whether the interpretation operator increases expressiveness and thus allows studying the relation between WSC and interpretations beyond counting. In this paper, we prove that if IFPC+WSC+I canonizes a particular class of base graphs, then it also canonizes the corresponding CFI graphs. This differs from various other logics, where CFI graphs provide difficult instances. To canonize CFI graphs, we nest WSC and interpretation operators. We show that for CFI graphs this deeper nesting is indeed necessary. Lastly, we separate IFPC+WSC from IFPC+WSC+I, so for IFPC the interpretation operator increases expressiveness, too. In particular, IFPC+WSC is not closed under FO-reductions.