Insignificant Choice Polynomial Time

In the late 1980s Gurevich conjectured that there is no logic capturing PTIME, where "logic" has to be understood in a very general way comprising computation models over isomorphism classes of structures. In this article we first show that Gurevich's conjecture is false. For this we extend the seminal research of Blass, Gurevich and Shelah on {\em choiceless polynomial time} (CPT), which exploits deterministic Abstract State Machines (ASMs) supporting unbounded parallelism to capture the choiceless fragment of PTIME. CPT is strictly included in PTIME. We observe that choice is unavoidable, but that a restricted version suffices, which guarantees that the final result is independent from the choice. Such a version of polynomially bounded ASMs, which we call {\em insignificant choice polynomial time} (ICPT) will indeed capture PTIME. This can be expressed in the logic of non-deterministic ASMs plus inflationary fixed-point. We use this result for our second contribution showing that PTIME differs from NP. For the proof we build again on the research on CPT first establishing a limitation on permutation classes of the sets that can be activated by an ICPT computation. We then prove an equivalence theorem, which characterises structures that cannot be distinguished by the logic. In particular, this implies that SAT cannot be decided by an ICPT computation.