The Computational Significance of Hausdorff 's Maximal Chain Principle

摘要

As a fairly frequent 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. When attempting to convert Hausdorff's principle into a conservation theorem, we have indeed found out that maximal chains are more reminiscent of maximal ideals than it might seem at first glance. The latter live in richer algebraic structures (rings), and thus are readier to be put under computational scrutiny. Exploiting the newly discovered analogy between maximal chains and ideals, we can carry over the concept of Jacobson radical from a ring to an arbitrary set with an irreflexive symmetric relation. This achievement enables us to present a generalisation of Hausdorff's principle first as a semantic and then as a syntactical conservation theorem. We obtain the latter, which is nothing but the desired computational core of Hausdorff's principle, by passing from maximal chains to paths of finite binary trees of an adequate inductively generated class. In addition to Hausdorff's principle, applications include the Maximal Clique Principle for undirected graphs. Throughout the paper we work within constructive set theory.