On the computational content of Zorn's lemma

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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
Pages768-781
Number of pages14
ISBN (Electronic)9781450371049
DOIs
Publication statusPublished - 8 Jul 2020

Publication series

NameACM International Conference Proceeding Series

Keywords

  • 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

Profiles

No photo of Thomas Powell

Cite this

Powell, T. (2020). On the computational content of Zorn's lemma. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 (pp. 768-781). [3394745] (ACM International Conference Proceeding Series). Association for Computing Machinery. https://doi.org/10.1145/3373718.3394745