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 (IFPC+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+WSCI simulates counting which IFP+WSC fails to do. For IFPC+WSC it is unknown whether the interpretation operator increases expressiveness and thus allows studying the relation between WSC and interpretations beyond counting. We separate IFPC+WSC from IFPC+WSCI by showing that IFPC+WSC is not closed under FO-interpretations. By the same argument, we answer an open question of Dawar and Richerby regarding non-witnessed symmetric choice in IFP. Additionally, we prove that nesting WSC-operators increases the expressiveness using the so-called CFI graphs. We show 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.

翻译：为PTime寻找逻辑的核心难题在于，做出任意选择的算法与同构不变逻辑之间存在不匹配。克服此问题的一种方法是见证对称选择。它允许从可定义轨道中进行选择，并由可定义的见证自同构所保证。我们考虑了带计数的固定点逻辑（IFPC）的扩展，即带有见证对称选择（IFPC+WSC）的扩展，以及进一步带有解释算子（IFPC+WSC+I）的扩展。后一算子在由解释定义的结构中评估子公式。该结构可能具有其他可由WSC算子利用的自同构。对于纯固定点逻辑（IFP）的类似扩展，已知IFP+WSCI可以模拟计数，而IFP+WSC则无法做到。对于IFPC+WSC，目前尚不清楚解释算子是否增加了表达能力，从而允许在计数之外研究WSC与解释之间的关系。我们通过证明IFPC+WSC在一阶逻辑解释下不封闭，从而将IFPC+WSC与IFPC+WSCI区分开来。通过相同的论证，我们回答了Dawar和Richerby关于IFP中非见证对称选择的一个开放性问题。此外，我们利用所谓的CFI图证明了嵌套WSC算子会增加表达能力。我们证明，如果IFPC+WSC+I能够规范化某一类基图，那么它也能规范化相应的CFI图。这与许多其他逻辑不同，在那些逻辑中CFI图通常构成困难实例。