An extension of fixpoint logic with a symmetry-based choice construct

We propose a mechanism of restricted non-determinism in logical languages that uses a so-called symmetry-based choice operator whose application is restricted only on symmetric elements. Based on this mechanism, we define a logical language that is in PTIME but strictly more expressive than fixed-point logic with counting. This language is based, on the one hand, on an extension of the inflationary fixed-point logic with a choice operator, called specified symmetry choice, and, on the other hand, on an introduction of a so-called logical reduction operator, which when added to the above extension of fixpoint logic, allows us to increase the expressive power.