Affiliations: [a] Dipartimento di Informatica, Università degli Studi di Verona, Italy | [b] Dipartimento di Informatica, Università degli Studi di Verona, Italy
Abstract: As a form of the Axiom of Choice about relatively simple structures (posets), Hausdorff’s Maximal Chain Principle appears to be little amenable to computational interpretation. This received view, however, requires revision: maximal chains are more reminiscent of maximal ideals than it seems at first glance. The latter live in richer algebraic structures (rings), and thus are readier to be put under computational scrutiny. Exploiting this, and of course the analogy between maximal chains and maximal ideals, the concept of Jacobson radical carries over from a ring to an arbitrary set with an abstract inconsistency predicate: that is, a distinguished monotone family of finite subsets. All this makes possible not only to generalise Hausdorff’s principle, but also to express it as a syntactical conservation theorem. The latter, which encompasses the desired computational core of Hausdorff’s principle, is obtained by a generalised inductive definition. The over-all setting is constructive set theory.
Keywords: Axiom of choice, maximal chain, maximal ideal, consistent theory, Jacobson radical, syntactical conservation, computational content, constructive set theory, inductive definition, finite binary tree
DOI: 10.3233/COM-210365
Journal: Computability, vol. 11, no. 2, pp. 147-162, 2022
