带见证对称选择的自由选择多项式时间

我们扩展了自由选择多项式时间（CPT）——这是在寻求捕捉 PTime 的逻辑中目前唯一仍有希望的候选者——使得这一扩展后的逻辑具有以下性质：对于每一个可定义同构的结构类，该逻辑自动捕捉 PTime。为此逻辑的构造，我们通过一个见证对称选择算子来扩展 CPT。该算子允许从可定义轨道中进行选择。但是，为确保多项式时间求值，必须提供自同构来认证所选集合确实是一个轨道。我们论证在此逻辑中，可定义同构蕴含可定义规范化。由此，我们的构造消除了将同构可定义性结果扩展到规范化的非平凡步骤。该步骤曾是证明 CPT 或其他逻辑在特定结构类上捕捉 PTime 的证明的一部分，且通常需要付出大量额外努力。