论文标题
可选的多项式时间与见证的对称选择
Choiceless Polynomial Time with Witnessed Symmetric Choice
论文作者
论文摘要
我们扩展了无选的多项式时间（CPT），目前仅保留有前途的候选人，以寻求逻辑捕获PTIME，以便该扩展逻辑具有以下属性：对于同构的每类结构都是可定义的，逻辑会自动捕获ptime。 为了构建此逻辑，我们扩展了见证的对称选择操作员的CPT。该操作员允许从可定义的轨道选择。但是，为了确保多项式时间评估，必须提供自动形态，以证明选择集确实是轨道。 我们认为，在这种逻辑上，可定义的同构意味着可定义的典范化。因此，我们的构造消除了将同构性确定性结果扩展到批判性的非平凡步骤。此步骤是证据的一部分，表明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, 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.
