key: cord-0046149-52blv0lv authors: Schuster, Peter; Wessel, Daniel title: The Computational Significance of Hausdorff’s Maximal Chain Principle date: 2020-06-24 journal: Beyond the Horizon of Computability DOI: 10.1007/978-3-030-51466-2_21 sha: ffa442ed16d4822e5bfd1feab5f3ae8c670a106c doc_id: 46149 cord_uid: 52blv0lv 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. Hausdorff's maximal chain principle asserts that every totally ordered subset of a partially ordered set S is contained in a maximal one. Equivalently, this can be put as a completeness criterion in first-order terms: a chain C is maximal precisely when, for every x ∈ S, if C ∪ { a } is a chain, then a ∈ C. So a chain C is maximal if and only if, for every a ∈ S, either a ∈ C or a is incomparable with at least one b ∈ C, i.e., This is somewhat reminiscent of the characterisation of maximal ideals in commutative ring theory [21] . In this setting an ideal J of a commutative unital ring takes the place of C, and the respective right-hand disjunct of (1) expresses that the ring element a is invertible modulo J. Moreover, it is possible to describe the common part of all maximal ideals in first-order terms. This encodes Krull's Maximal Ideal Theorem as an intersection principle, and yields a notion of Jacobson radical suitable for constructive algebra [21, 31, 38] . By analogy, we can define the Jacobson radical Jac(C) of a chain C, and prove (assuming the Axiom of Choice AC) that Jac(C) coincides with the intersection of all maximal chains containing C. Hence Hausdorff's principle too can be recast as an intersection principle. All this will even be done in a slightly more general fashion. The main point to be stressed is that a simple constructive interpretation is possible, whence the purpose of this paper is twofold: we communicate a new choice principle, and describe its constructive underpinning. We proceed as follows. In Sect. 2, alongside the analogy with ring theory, we describe our concepts of coalition and Jacobson radical. In Sect. 3 we briefly relate this to past work [25] [26] [27] on the interplay of single-and multi-conclusion entailment relations [9, 35] . In Sect. 4 we give a constructive account of complete coalitions by means of a suitable inductively generated class of binary trees. In Sect. 5 we briefly discuss two applications: maximal chains of partially ordered sets, and maximal cliques of undirected graphs. The main results are Proposition 1 and its constructive companion Proposition 3. The content of this paper is elementary and can be formalised in a suitable fragment of constructive set theory CZF [2, 3] . Due to the choice of this setting, sometimes certain assumptions have to be made explicit which otherwise would be trivial in classical set theory. For instance, a subset T of a set S is detachable if, for every a ∈ S, either a ∈ T or a / ∈ T . A set S is finitely enumerable if there is n 0 and a surjective function f : { 1, . . . , n } → S. We write Fin(S) for the set of finitely enumerable subsets of S. To pin down a rather general, classical intersection principle, and to point out certain of its incarnations, requires some classical logic and the Axiom of Choice (AC) in its classically equivalent form of Zorn's Lemma (ZL) [40] . For simplicity we switch in such a case to classical set theory ZFC, signalling this appropriately. Throughout, let S be a set, and let R be an irreflexive symmetric relation on S. We say that a subset C of S be a coalition 1 (with respect to R) if ¬aRb for all a, b ∈ C. This is the same as demanding that C be R-connected, which is to say that a ∈ C only if aRb for every b ∈ C, where R denotes the complementary relation. For instance, the empty subset is a coalition, as is every singleton subset of S, by the irreflexivity of R. Notice that coalitions are closed under directed union. A coalition C is called complete if, for every a ∈ S, a ∈ C ∨ (∃b ∈ C) aRb. ( It is perhaps instructive to read aRb as "a opposes b" (and vice versa, to account for symmetry), under which reading it makes sense to require irreflexivity. A coalition is then a subset of S in which no two members oppose one another. A complete coalition C is such that, given any a ∈ S, this a either belongs to C, or else C exhibits a witness b which opposes a. Every complete coalition is detachable and maximal (with respect to set inclusion) among coalitions. Conversely, with classical logic every maximal coalition is complete. Proof. Let C be a complete coalition. Since aRb for all a, b ∈ C, the second alternative of completeness (2) entails that a / ∈ C; whence C is detachable. As regards C being maximal, let D be a coalition such that C ⊆ D and let a ∈ D. By completeness, either a ∈ C right away, or else there is b ∈ C such that aRb, but the latter case is impossible as D is a coalition. As regards the converse, if C is a complete coalition and a / ∈ C, then C = C ∪{ a } cannot, due to maximality of C, in turn be a coalition. With classical logic, the latter statement is witnessed by a certain element b ∈ C. This yields completeness. If C is a coalition, let us write Comp/C for the collection of all complete coalitions that contain C, with the special case Comp = Comp/∅. Since every complete coalition is detachable (Lemma 1), these collections are sets due to the presence in CZF of the Exponentiation Axiom [2, 3] . All this is fairly reminiscent of the characteristics of maximal ideals in ring theory [21] . Given a commutative ring A with 1, recall from [12, 21] that the Jacobson radical [20] of an ideal J of A can be defined as where sharp brackets denote generated ideals. By plain analogy with the ringtheoretic setting, let us then define the Jacobson radical of an arbitrary subset C of S, of course with respect to our default, irreflexive symmetric relation R: In particular, the Jacobson radical of the empty coalition is Thus, we substitute the property of mutual opposition in (4) for the one of comaximality in (3), i.e., for the property of two ring elements to generate the unit ideal. Assuming AC, the Jacobson radical of an ideal J is the intersection of all maximal ideals that contain J [21] . Similarly, and still with AC, the Jacobson radical of a coalition C turns out to be the intersection of all complete coalitions containing C (Proposition 1). The Jacobson radical defines a closure operator on S which restricts to a mapping on coalitions, i.e., if C is a coalition, then so is Jac(C). Proof. As for the first statement we only show idempotency, i.e., Jac(Jac(C)) ⊆ Jac(C), where C ⊆ S. In fact, if a ∈ Jac(Jac(C)) and b ∈ S is such that aRb, then there is c ∈ Jac(C) with cRb. It follows that there is c ∈ C such that bRc , and so a ∈ Jac(C). As regards the second statement, suppose that C ⊆ S is a coalition, and let a 0 , a 1 ∈ Jac(C). Assuming that a 1 Ra 0 , since a 1 ∈ Jac(C), there is c 0 ∈ C such that a 0 Rc 0 . Since a 0 ∈ Jac(C) too, there is c 1 ∈ C such that c 0 Rc 1 , which is in conflict with C being a coalition. Proof. Let a ∈ Jac(C) and suppose that D is a complete coalition which contains C. By completeness, either a ∈ D right away, or else there is b ∈ D such that aRb. But since a ∈ Jac(C), the latter case would imply that there were c ∈ C ⊆ D with bRc, by way of which D would fail to be a coalition after all. For the right-to-left inclusion we concentrate on the contrapositive. Thus, suppose that a / ∈ Jac(C). Accordingly, there is b such that aRb and C := C ∪{ b } is a coalition. ZL yields a coalition D which is maximal among those containing C . This D is complete by way of being maximal, and it must avoid a, because if a ∈ D, then D were not a coalition since b ∈ C ⊆ D and aRb. Remark 1. The argument in the right-to-left part of the proof of Proposition 1 can also be used in a more affirmative manner. ZL, which is said to be constructively neutral [4] , 2 directly implies that where Max/C denotes the collection of all maximal coalitions over C. The crucial direction of Proposition 1 can also be proved in a more direct manner by using Open Induction [6, 11, 23] in place of Zorn's Lemma. For similar cases see [10, 24, 29, 30] . By a radical coalition C we understand one which is closed with respect to Jac, i.e., which is such that Jac(C) = C. Clearly, every complete coalition is radical, and by Lemma 2 so is the intersection of an inhabited family of complete coalitions. By Proposition 1, in ZFC the radical coalitions are precisely the intersections of complete coalitions; so in particular With Proposition 3 we will give a constructive version of Proposition 1 in Sect. 4, to which end Proposition 2 below will be crucial. In the following, we write for the image of x under R, and use Jac(C, x) as a shorthand for Jac(C ∪ { x }). The following is provable for the Jacobson radical: where a, x ∈ S and C is an arbitrary subset of S. Proof. Given the displayed premises, to check that a ∈ Jac(C), consider b ∈ S such that aRb. We need to find c ∈ C such that bRc. The left-hand premise yields c ∈ C ∪ { x } such that bRc . If c ∈ C, then c = c is as required. In case of c = x, the right-hand premise for y = b yields a ∈ Jac(C, b). Again with aRb it follows that there is c ∈ C ∪ { b } such that bRc, whence in fact c ∈ C since R is irreflexive. Remark 2. Given a binary relation R on S, an R-clique is a subset C such that, for every a ∈ S, a ∈ C ⇔ (∀b ∈ C) aRb. Bell's Clique Property asserts that, for any reflexive symmetric relation R on S, an R-clique exists. This is in fact an intuitionistic equivalent of ZL [5] . Classically, given an irreflexive symmetric relation R, every R-clique is a complete R-coalition. Conversely, and constructively, every complete R-coalition is an Rclique. More precisely, a subset C of S is an R-clique if and only if it is Rconnected as well as R-saturated, the latter of which is to say that a ∈ C already if aRb for all b ∈ C. Consider on S the relation ⊆ Fin(S) × S which is defined by the Jacobson radical, i.e., stipulate U a ≡ a ∈ Jac(U ). Lemma 2 tells us that this is a single-conclusion entailment relation, which is to say that it is reflexive, monotone, and transitive in the following sense: where the usual shorthand notation is at work with U, V ≡ U ∪ V and U, b ≡ U ∪ {b}. In ZFC, the consequences with respect to of a coalition U ∈ Fin(S) are semantically determined by the complete coalitions over U , i.e., Proposition 2 implies that the following is provable: This is to say that the infinitary axiom of completeness (2) , which in the present context can be put in the form is in fact conservative [25, 26] over . To make this precise requires extending the results of [25, 26] to an infinitary setting [36] , but upon which those results go through verbatim. We do not require such a development here; an elementary constructive interpretation of Proposition 1 will be given in the following section using instead a suitable inductively generated collection of finite binary trees. For related uses of conservativity see also, e.g., [16, 27, 28] . In this section we carry over the approach recently followed in [34] for prime ideals of commutative rings, so as to accommodate complete coalitions. Readers familiar with dynamical algebra [13, 21, 38] will draw a connection between the tree methods of [13] and the one employed here. Let again S be a set. For every a ∈ S we first introduce a corresponding letter X a . Let be the set of finite sequences of elements of S and such letters, with the usual provisos on notation, concatenation, etc. Next, we generate inductively a class T of finite rooted binary trees T ⊆ S as follows: As usual, by a leaf we understand a sequence u ∈ T without immediate successor in T . The second rule is to say that, given T ∈ T , if u is a leaf of T , then each element a of S gives rise to a new member of T by way of an additional branching at u. More precisely, u gives birth to two children ua and uX a . Here is a possible instance, where a, b ∈ S: [] As an auxiliary tool, we further need a sorting function sort : S → S which gathers all occurring letters X a at the tail of a finite sequence. As the resulting order of the entries won't matter later on, this function may be defined recursively in the simplest manner, as follows: Last but not least, given a subset C of S, we introduce a relation C between elements of S and sorted finite sequences in S by defining x j Rb j → c ∈ Jac (C, a 1 , . . . , a k , x 1 , . . . , x ) , where we drop the quantifier in case of = 0. In particular, Keeping in mind Proposition 1, with AC the semantics of this relation is that if u = [a 1 , . . . , a k , X b1 , . . . , X b ] as above, then c C u precisely when, for every simultaneous instantiation of respective opponents x 1 , . . . , x of b 1 , . . . , b , this c is a member of every complete coalition over C that further contains a 1 , . . . , a k , x 1 , . . . , x . The case in which this holds with respect to every leaf of a certain tree T ∈ T will later be of particular interest. With the relation C in place, we can now rephrase Proposition 2 as follows. Let a, c ∈ S and let u ∈ S be sorted. If c C au and c C uX a , then c C u. Proof. Consider u = [a 1 , . . . , a k , X b1 , . . . , X b ] and suppose that (i) c C au and (ii) c C uX a . To show that c C u, let x 1 ∈ R(b 1 ), . . . , x ∈ R(b ). We write C = C ∪ { a 1 , . . . , a k , x 1 , . . . , x } and need to check that c ∈ Jac(C ). With x 1 , . . . , x fixed, premise (i) yields c ∈ Jac(C , a), while (ii) implies that, for every x ∈ R(a), c ∈ Jac(C , x). Now Proposition 2 implies a ∈ Jac(C ). Given a subset C and an element c of S, let us say that a tree T ∈ T terminates for C in c if c C sort(u) for every leaf u of T . Intuitively, this is to say that, along every path of T , no matter how we instantiate indeterminates X b that we might encounter with a corresponding opponent x of b, if C is a complete coalition over C and contains the elements we will have collected at the leaf, then c is a member of C . The idea is now to fold up branchings by inductive application of Lemma 3, to capture termination by way of the Jacobson radical, and thus to resolve indeterminacy in the spirit of [33] . The following is the constructive counterpart of Proposition 1 and does not require that C be a coalition to start with. 1. c ∈ Jac(C). Proof. If c ∈ Jac(C), then c C [] by (6) , which is to say that [] terminates for C in c. Conversely, suppose that T ∈ T is such that c C sort(u) for every leaf u of T . We argue by induction on T to show that c ∈ Jac(C). The case T = [] is trivial (6) . Suppose that T is the result of a branching at a certain leaf u of an immediate subtree T , and suppose further that c C sort(ua) = a sort(u) as well as c C sort(uX a ) = sort(u)X a for a certain a ∈ S. Lemma 3 implies that c C sort(u), whence we reduce to T , to which the induction hypothesis applies. Membership in a radical coalition C is thus tantamount to termination. Remark 3. Very much in the spirit of dynamical algebra [13, 21, 37, 38] , every tree T ∈ T represents the course of a dynamic argument as if a given coalition were complete. Note that every complete coalition C m of S gives rise to a path through a given tree T ∈ T . In fact, at each branching, corresponding to an element a of S, by way of completeness this a either belongs to C m or else the latter assigns a value to X a in the sense of exhibiting a witness b ∈ C m for which aRb. The entries in the terminal node of this path, with values assigned appropriately, then belong to C m . In particular, if T terminates in c for a certain subset C ⊆ C m , then c ∈ C m because c ∈ Jac(C) ⊆ Jac(C m ) = C m by Proposition 3 and the fact that every complete coalition is radical. In general it cannot be decided effectively, i.e., without using some excluded middle, whether, given c ∈ S and C ⊆ S, there is a tree T ∈ T which terminates for C in c. 3 This is due to the constructive character of Proposition 3 and the following Brouwer-style counterexample. Let ϕ be a bounded formula. 4 Let S = { 0, 1 } and put By definition, this relation clearly is irreflexive and symmetric. Consider now the corresponding Jacobson radical Jac(∅). It is easy to see that 0 ∈ Jac(∅) ⇔ ¬ϕ. Therefore, if Jac(∅) is detachable, then ¬ϕ ∨ ¬¬ϕ. This is to say that the Weak Restricted Law of Excluded Middle (WREM) holds. We will now briefly discuss two instantiations of Proposition 1, concerning maximal chains of partially ordered sets and maximal cliques in undirected graphs. In both cases Proposition 3 provides the corresponding constructive underpinning, which we leave to the reader to spell out in detail. Incidentally, the trick is to start with a relation R of which only the complement R is the relation one actually one wants to consider. This clearly fits the concept of coalition we are employing. Let (S, ) be a partially ordered set. On S we consider the binary relation R of incomparability, which is and for which R means comparability. Classically, a coalition for R is nothing but a chain, i.e., a totally ordered subset of S, and the complete coalitions are the maximal chains. As regards the Jacobson radical in this setting, Proposition 1 applied to the empty chain yields that This is a way to rephrase Hausdorff's maximal chain principle [17] . In fact, if S is not totally ordered by , as witnessed by a certain element a of S incomparable to some b ∈ S, then by (7) and classical logic there is a maximal chain that avoids a. Incidentally, this application helps to calibrate Proposition 1, which over classical set theory ZF thus turns out equivalent to AC through Hausdorff's principle [18, 19, 22] . Let G = (V, E) be an undirected graph, V being its set of vertices, E its set of edges, i.e., E is a set of unordered pairs of elements of V . On the set of vertices we consider the binary relation R of nonadjacency, which is In this setting, classically, a coalition for R is nothing but a clique 5 [7] , i.e., a subset of V every two distinct elements of which are adjacent, and the complete coalitions are the maximal cliques. Concerning the Jacobson radical, Proposition 1 implies that Similar to the preceding application, this yields a solution to the problem of finding a maximal clique with AC. 6 Hausdorff's Maximal Chain Principle, a forerunner of Zorn's Lemma [8, 40] , is presumably one of the most well-known order-theoretic forms of the Axiom of Choice. We have seen that the property of a chain to be maximal can be put as a completeness criterion, reminiscent of the case in commutative ring theory for maximal ideals. By analogy with Krull's Theorem for maximal ideals, employing a suitably adapted form of Jacobson radical, it has become possible to put a new variant of Hausdorff's Principle in terms of a universal statement. This has paved the way to a constructive, purely syntactic rereading by means of an inductively defined class of finite binary trees which encode computations along generic maximal chains. It remains to be seen, however, to what extent in a concrete setting our method allows to bypass invocations of Hausdorff's Principle. Along similar lines, we have carried over the concept of Jacobson radical from commutative rings to the setting of universal algebra and thus to broaden considerably the range of applications that our approach has opened up so far [33, 34] . In fact, every single-conclusion entailment relation is accompanied by a Jacobson radical which in turn encodes a corresponding maximality principle. In particular, this encompasses the Jacobson radical for distributive lattices [12] , commutative rings [31] , as well as for propositional theories [15, 16] . We keep for future research to put all this under computational scrutiny, and to compare with ours the related methods employed in dynamical algebra [13] . Zorn's Lemma in CZF Notes on constructive set theory Constructive set theory Zorn's lemma and complete Boolean algebras in intuitionistic type theories Some new intuitionistic equivalents of Zorn's lemma A computational interpretation of open induction Graph Theory The origin of "Zorn's lemma Entailment relations and distributive lattices Lindenbaum's Lemma via Open Induction A note on the open induction principle Dimension de Heitmann des treillis distributifs et des anneaux commutatifs. Publications Mathématiques de Besançon. Algèbre et Théorie des Nombres Dynamical method in algebra: effective Nullstellensätze Untersuchungenüber das Zornsche Lemma The Jacobson radical: from algebra to logic The Jacobson radical of a propositional theory Grundzüge der Mengenlehre Axiom of Choice Consequences of the Axiom of Choice The radical and semi-simplicity for arbitrary rings Commutative Algebra: Constructive Methods. Finite Projective Modules Notes on Set Teory. Undergraduate Texts in Mathematics Proving open properties by induction A universal Krull-Lindenbaum theorem Eliminating disjunctions by disjunction elimination Eliminating disjunctions by disjunction elimination Cut elimination for entailment relations Der Satz von Hahn-Banach per Disjunktionselimination Induction in algebra: a first case study Induction in algebra: a first case study Syntax for semantics: Krull's maximal ideal theorem A general extension theorem for directed-complete partial orders Resolving finite indeterminacy: a definitive constructive universal prime ideal theorem Dynamic evaluation of integrity and the computational content of Krull's lemma Completeness and axiomatizability in many-valued logic Points, ideals, and geometric sequents Making the use of maximal ideals constructive Projective Modules Over Polynomial Rings and Dynamical Gröbner Bases Handbooks in Economics, 1st edn A remark on method in transfinite algebra Acknowledgements. The present study was carried out within the projects "A New Dawn of Intuitionism: Mathematical and Philosophical Advances" (ID 60842) funded by the John Templeton Foundation, and "Reducing complexity in algebra, logic, combinatorics -REDCOM" belonging to the programme "Ricerca Scientifica di Eccellenza 2018" of the Fondazione Cariverona. The authors are members of the Gruppo Nazionale per le Strutture Algebriche, Geometriche e le loro Applicazioni (GNSAGA) within the Italian Istituto Nazionale di Alta Matematica (INdAM) (The opinions expressed in this paper are those of the authors and do not necessarily reflect the views of those foundations.). The anonymous referees' careful readings of the manuscript and several helpful remarks and suggestions are gratefully acknowledged.