一句话：通过引入带见证对称选择扩展 CPT，使可定义同构自动蕴含可定义规范化，并在同构可定义结构类上自动捕捉 Ptime。
Choiceless Polynomial Time（CPT）是当前有望刻画 Ptime 的逻辑候选。本文针对在特定结构类上证明 CPT 捕捉 Ptime 时，从同构可定义性推广到规范化需要大量额外工作的难题，扩展 CPT 引入带见证的对称选择算子。该算子允许从可定义轨道中选择元素，但要求提供自同构作为见证以证明选择集确为轨道，从而保证多项式时间求值。作者证明，在该扩展逻辑中，可定义同构蕴含可定义规范化。因此，对任何同构可定义的结构类，该逻辑自动捕捉 Ptime，消除了原有证明中非平凡的推广步骤。
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, we remove 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.