Choiceless Polynomial Time with Witnessed Symmetric Choice

TL;DR

This paper extends Choiceless Polynomial Time (CPT) with a witnessed symmetric choice operator, enabling the logic to automatically capture PTime on classes where isomorphism is definable, simplifying proofs of PTime capture.

Contribution

Introduction of a witnessed symmetric choice operator to CPT, ensuring definable isomorphism implies definable canonization, thus streamlining PTime capture proofs.

Findings

Logic captures PTime on classes with definable isomorphism.

Automorphisms certify orbit choices, maintaining polynomial time evaluation.

Simplifies the process of proving PTime capture by removing extra steps.

Abstract

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.