Choiceless Computation and Symmetry: Limitations of Definability

Author Benedikt Pago

Thumbnail PDF


  • Filesize: 0.51 MB
  • 21 pages

Document Identifiers

Author Details

Benedikt Pago
  • Mathematical Foundations of Computer Science, RWTH Aachen University, Germany


I would like to thank my advisor Erich Grädel for helpful comments and discussions.

Cite AsGet BibTex

Benedikt Pago. Choiceless Computation and Symmetry: Limitations of Definability. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


The search for a logic capturing PTIME is a long standing open problem in finite model theory. One of the most promising candidate logics for this is Choiceless Polynomial Time with counting (CPT). Abstractly speaking, CPT is an isomorphism-invariant computation model working with hereditarily finite sets as data structures. While it is easy to check that the evaluation of CPT-sentences is possible in polynomial time, the converse has been open for more than 20 years: Can every PTIME-decidable property of finite structures be expressed in CPT? We attempt to make progress towards a negative answer and show that Choiceless Polynomial Time cannot compute a preorder with colour classes of logarithmic size in every hypercube. The reason is that such preorders have super-polynomially many automorphic images, which makes it impossible for CPT to define them. While the computation of such a preorder is not a decision problem that would immediately separate P and CPT, it is significant for the following reason: The so-called Cai-Fürer-Immerman (CFI) problem is one of the standard "benchmarks" for logics and maybe best known for separating fixed-point logic with counting (FPC) from P. Hence, it is natural to consider this also a potential candidate for the separation of CPT and P. The strongest known positive result in this regard says that CPT is able to solve CFI if a preorder with logarithmically sized colour classes is present in the input structure. Our result implies that this approach cannot be generalised to unordered inputs. In other words, CFI on unordered hypercubes is a PTIME-problem which provably cannot be tackled with the state-of-the-art choiceless algorithmic techniques.

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
  • Mathematics of computing → Permutations and combinations
  • finite model theory
  • descriptive complexity
  • choiceless computation
  • symmetries of combinatorial objects


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Matthew Anderson and Anuj Dawar. On symmetric circuits and fixed-point logics. Theory of Computing Systems, 60(3):521-551, 2017. URL:
  2. Andreas Blass, Yuri Gurevich, and Saharon Shelah. Choiceless polynomial time. Annals of Pure and Applied Logic, 100(1-3):141-187, 1999. URL:
  3. Jin-yi Cai, Martin Fürer, and Neil Immerman. An optimal lower bound on the number of variables for graph identification. Combinatorica, 12:389-410, 1992. URL:
  4. Ashok K Chandra and David Harel. Structure and complexity of relational queries. In 21st Annual Symposium on Foundations of Computer Science (sfcs 1980), pages 333-347. IEEE, 1980. URL:
  5. Anuj Dawar. The nature and power of fixed-point logic with counting. ACM SIGLOG News, 2(1):8-21, 2015. Google Scholar
  6. Anuj Dawar, Martin Grohe, Bjarki Holm, and Bastian Laubner. Logics with rank operators. In 2009 24th Annual IEEE Symposium on Logic In Computer Science, pages 113-122. IEEE, 2009. URL:
  7. Anuj Dawar, David Richerby, and Benjamin Rossman. Choiceless polynomial time, counting and the Cai-Fürer-Immerman graphs. Annals of Pure and Applied Logic, 152(1-3):31-50, 2008. URL:
  8. Erich Grädel and Martin Grohe. Is Polynomial Time Choiceless? In Fields of Logic and Computation II, pages 193-209. Springer, 2015. URL:
  9. Erich Grädel, Wied Pakusa, Svenja Schalthöfer, and Łukasz Kaiser. Characterising Choiceless Polynomial Time with First-order Interpretations. In Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 677-688, 2015. URL:
  10. Martin Grohe. The quest for a logic capturing PTIME. In 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pages 267-271. IEEE, 2008. URL:
  11. Yuri Gurevich. Logic and the Challenge of Computer Science. In Current Trends in Theoretical Computer Science. Computer Science Press, 1988. Google Scholar
  12. Neil Immerman. Relational queries computable in polynomial time. In Proceedings of the fourteenth annual ACM symposium on Theory of computing, pages 147-152, 1982. URL:
  13. Wied Pakusa. Linear Equation Systems and the Search for a Logical Characterisation of Polynomial Time. PhD thesis, RWTH Aachen, 2015. Google Scholar
  14. Wied Pakusa, Svenja Schalthöfer, and Erkal Selman. Definability of Cai-Fürer-Immerman problems in Choiceless Polynomial Time. ACM Transactions on Computational Logic (TOCL), 19(2):1-27, 2018. URL:
  15. Benjamin Rossman. Choiceless computation and symmetry. In Fields of Logic and Computation, Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, volume 6300 of Lecture Notes in Computer Science, pages 565-580. Springer, 2010. URL:
  16. Svenja Schalthöfer. Choiceless Computation and Logic. PhD thesis, RWTH Aachen, 2020. Google Scholar
  17. Moshe Y Vardi. The complexity of relational query languages. In Proceedings of the fourteenth annual ACM symposium on Theory of computing, pages 137-146, 1982. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail