Choiceless Polynomial Time with Counting

Choiceless polynomial time with counting is a computational formalism on unordered finite structures that operates on hereditarily finite sets built from the input elements as atoms. It permits invariant set operations, comprehension, and cardinality, with a fixed polynomial bound on computation and on the number of recursively occurring objects. It does not select an arbitrary ordering of the atoms. The counting operation returns a finite von Neumann ordinal, and no fixed bound on set rank is imposed (Blass et al. 1999, §4.8). Capturing polynomial time would mean defining every isomorphism-invariant polynomial-time Boolean query on every fixed finite relational vocabulary.