We extend Choiceless Polynomial Time (CPT), the currently only remaining promising candidate in the quest for a logic capturing PTime, so that this extended logic has the following property: for every class of structures for which isomorphism is definable, the logic automatically captures PTime. For the construction of this logic we extend CPT by a witnessed symmetric choice operator. This operator allows for choices from definable orbits. But, to ensure polynomial time evaluation, automorphisms have to be provided to certify that the choice set is indeed an orbit. We argue that, in this logic, definable isomorphism implies definable canonization. Thereby, our construction removes the non-trivial step of extending isomorphism definability results to canonization. This step was a part of proofs that show that CPT or other logics capture PTime on a particular class of structures. The step typically required substantial extra effort.

翻译：我们扩展了无穷多项式时间（CPT）——当前在寻找捕获PTime的逻辑中唯一尚存的有前景的候选者——使得这个扩展逻辑具有以下性质：对于每个其上同构可定义的结构类，该逻辑自动捕获PTime。为构造此逻辑，我们通过一个见证对称选择算子扩展了CPT。该算子允许从可定义的轨道中进行选择。但为确保多项式时间评估，必须提供自同构来证明所选集合确实是一个轨道。我们论证，在此逻辑中，可定义同构蕴含可定义规范形。由此，我们的构造消除了将同构可定义性结果扩展至规范形这一非平凡步骤。该步骤曾是证明CPT或其他逻辑在特定结构类上捕获PTime的组成部分，通常需要大量额外工作。