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在FO解释下不封闭，将IFPC+WSC与IFPC+WSCI区分开来。通过相同的论证，我们回答了Dawar和Richerby关于IFP中非见证对称选择的一个开放问题。此外，我们利用所谓的CFI图证明嵌套WSC算子会增加表达能力。我们表明：如果IFPC+WSC+I对一类特定的基础图进行规范化，那么它也会对相应的CFI图进行规范化。这与其他多种逻辑不同，在这些逻辑中CFI图提供了困难实例。