On the computational content of Zorn's lemma

DOI10.1145/3373718.3394745zbMATH Open1498.03153arXiv2001.03540OpenAlexW3099555404MaRDI QIDQ5145679FDOQ5145679

Author name not available (Why is that?)

Publication date: 21 January 2021

Published in: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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"odel'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.

Full work available at URL: https://arxiv.org/abs/2001.03540

zbMATH Keywords

domain theorycontinuous functionalsZorn's lemmahigher-order computabilityGödel's functional interpretation

Mathematics Subject Classification ID

Higher-type and set recursion theory (03D65) Axiom of choice and related propositions (03E25) Relative consistency and interpretations (03F25) Functionals in proof theory (03F10)

Cited In (5)

• Maximal ideals in countable rings, constructively
• A universal algorithm for Krull's theorem
• On the computational content of the Bolzano-Weierstraß Principle
• The Jacobson radical for an inconsistency predicate
• The computational content of Walras' existence theorem

This page was built for publication: On the computational content of Zorn's lemma

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145679)