  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 structures. In this article we first refute Gurevich's
conjecture. 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. Even more, insignificant
choice can be captured by ASMs with choice restricted to atoms such that a {\em
local insignificance condition} is satisfied. As this condition can be
expressed in the logic of non-deterministic ASMs, we obtain a logic capturing
PTIME. Furthermore, using inflationary fixed-points we can capture problems in
PTIME by fixed-point formulae in a fragment of the logic of non-deterministic
ASMs plus inflationary fixed-points. 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
inseparability theorem, which characterises classes of structures that cannot
be separated by the logic. In particular, this implies that SAT cannot be
decided by an ICPT computation.
