On the computational content of Zorn's lemma

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

Authors:

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

Recommendations

• Well quasi-orders and the functional interpretation
• On the computational content of the axiom of choice
• Axiom of choice and Zorn's lemma in Cantor categories
• Zorn's lemma and complete Boolean algebras in intuitionistic type theories
• On the computational content of the Bolzano-Weierstraß Principle

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 (6)

• 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
• Well quasi-orders and the functional interpretation

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)