On the computational content of Zorn's lemma

DOI10.1145/3373718.3394745MaRDI QIDQ5145679zbMATH OpenOpenAlexFDO

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)

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

zbMATH Keywords

continuous functionalsdomain theoryGödel's functional interpretationhigher-order computabilityZorn's lemma

Mathematics Subject Classification ID

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

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.

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

Cited in

(16)

• Maximal ideals in countable rings, constructively
• A universal algorithm for Krull's theorem
• On the computational content of the Bolzano-Weierstraß Principle
• Well quasi-orders and the functional interpretation
• Zorn's lemma and complete Boolean algebras in intuitionistic type theories
• The Jacobson radical for an inconsistency predicate
• The computational content of Walras' existence theorem
• On the Weihrauch degree of the additive Ramsey theorem
• Hilbert's tenth problem for term algebras with a substitution operator
• Complemented subsets and Boolean-valued, partial functions
• Defining long words succinctly in FO and MSO
• On the first-order parts of problems in the Weihrauch degrees
• Algorithmically random series
• Ideal presentations and numberings of some classes of effective quasi-Polish spaces
• Lower bounds on () and other properties of -register machines
• Reifying dynamical algebra: maximal ideals in countable rings, constructively

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)