On the computational content of Zorn's lemma

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

3 Citations (SciVal)


We give a computational interpretation to an abstract instance of Zorn's lemma formulated as a wellfoundedness principle in the language of arithmetic in all finite types. This is achieved through Gödel's functional interpretation, and requires the introduction of a novel form of recursion over non-wellfounded partial orders whose existence in the model of total continuous functionals is proven using domain theoretic techniques. We show that a realizer for the functional interpretation of open induction over the lexicographic ordering on sequences follows as a simple application of our main results.
Original languageEnglish
Title of host publicationProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
Place of PublicationU. S. A.
PublisherAssociation for Computing Machinery
Number of pages14
ISBN (Electronic)9781450371049
Publication statusPublished - 8 Jul 2020

Publication series

NameACM International Conference Proceeding Series


  • Gödel's functional interpretation
  • Zorn's lemma
  • continuous functionals
  • domain theory
  • higher-order computability

ASJC Scopus subject areas

  • Human-Computer Interaction
  • Computer Networks and Communications
  • Computer Vision and Pattern Recognition
  • Software

Cite this