# The Computational Significance of Hausdorff’s Maximal Chain Principle

- 37 Downloads

## Abstract

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.

## Keywords

Axiom of Choice Maximal chain Maximal ideal Maximal clique Jacobson radical Proof-theoretic conservation Computational content Constructive set theory Finite binary tree Inductive generation## 1 Introduction

*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 \in S\), if \(C \cup \{\,a\,\}\) is a chain, then \(a \in C\). So a chain

*C*is maximal if and only if, for every \(a \in S\), either \(a \in C\) or

*a*is incomparable with at least one \(b \in C\), i.e.,

*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 \({\text {Jac}}(C)\) of a chain *C*, and prove (assuming the Axiom of Choice AC) that \({\text {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.

**Foundations**

The content of this paper is elementary and can be formalised in a suitable fragment of constructive set theory
Open image in new window
[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 \in S\), either \(a \in T\) or \(a \notin T\). A set *S* is *finitely enumerable* if there is \(n \geqslant 0\) and a surjective function \(f : \{\,1, \dots , n\,\} \rightarrow S\). We write \({\text {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
Open image in new window
, signalling this appropriately.

## 2 Coalitions

*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 \(\lnot aRb\) for all \(a,b \in C\). This is the same as demanding that

*C*be \(\overline{R}\)-

*connected*, which is to say that \(a \in C\) only if \(a \overline{R} b\) for every \(b \in C\), where \(\overline{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 \in S\),

*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 \in S\), this

*a*either belongs to

*C*, or else

*C*exhibits a witness

*b*which opposes

*a*.

### Lemma 1

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 \(a \overline{R} b\) for all \(a,b \in C\), the second alternative of completeness (2) entails that \(a \notin C\); whence *C* is detachable. As regards *C* being maximal, let *D* be a coalition such that \(C \subseteq D\) and let \(a \in D\). By completeness, either \(a \in C\) right away, or else there is \(b \in 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 \notin C\), then \(C' = C \cup \{\,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 \in C\). This yields completeness. \(\square \)

*C*is a coalition, let us write

*C*, with the special case \(\mathrm {Comp} = \mathrm {Comp}/\emptyset \). Since every complete coalition is detachable (Lemma 1), these collections are sets due to the presence in Open image in new window of the Exponentiation Axiom [2, 3].

*A*with 1, recall from [12, 21] that the Jacobson radical [20] of an ideal

*J*of

*A*can be defined as

*Jacobson radical*of an arbitrary subset

*C*of

*S*, of course with respect to our default, irreflexive symmetric relation

*R*:

*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).

### Lemma 2

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 \({\text {Jac}}(C)\).

### Proof

As for the first statement we only show idempotency, i.e., \({\text {Jac}}({\text {Jac}}(C)) \subseteq {\text {Jac}}(C)\), where \(C \subseteq S\). In fact, if \(a \in {\text {Jac}}({\text {Jac}}(C))\) and \(b \in S\) is such that *aRb*, then there is \(c \in {\text {Jac}}(C)\) with *cRb*. It follows that there is \(c' \in C\) such that \(bRc'\), and so \(a \in {\text {Jac}}(C)\).

As regards the second statement, suppose that \(C \subseteq S\) is a coalition, and let \(a_0, a_1 \in {\text {Jac}}(C)\). Assuming that \(a_1Ra_0\), since \(a_1 \in {\text {Jac}}(C)\), there is \(c_0 \in C\) such that \(a_0 R c_0\). Since \(a_0 \in {\text {Jac}}(C)\) too, there is \(c_1 \in C\) such that \(c_0 R c_1\), which is in conflict with *C* being a coalition. \(\square \)

### Proposition 1

**(**Open image in new window

**).**If

*C*is a coalition, then

### Proof

Let \(a \in {\text {Jac}}(C)\) and suppose that *D* is a complete coalition which contains *C*. By completeness, either \(a \in D\) right away, or else there is \(b \in D\) such that *aRb*. But since \(a \in {\text {Jac}}(C)\), the latter case would imply that there were \(c \in C \subseteq 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 \notin {\text {Jac}}(C)\). Accordingly, there is *b* such that *aRb* and \(C' := C \!\cup \!\{\,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 \in D\), then *D* were not a coalition since \(b \in C' \subseteq D\) and *aRb*. \(\square \)

### Remark 1

^{2}directly implies that

*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].

*radical*coalition

*C*we understand one which is closed with respect to \({\text {Jac}}\), i.e., which is such that \({\text {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 Open image in new window the radical coalitions are precisely the intersections of complete coalitions; so in particular

*x*under

*R*, and use \({\text {Jac}}(C,x)\) as a shorthand for \({\text {Jac}}(C \cup \{\,x\,\})\).

### Proposition 2

*C*is an arbitrary subset of

*S*.

### Proof

Given the displayed premises, to check that \(a \in {\text {Jac}}(C)\), consider \(b \in S\) such that *aRb*. We need to find \(c \in C\) such that *bRc*. The left-hand premise yields \(c' \in C \cup \{\,x\,\}\) such that \(bRc'\). If \(c' \in C\), then \(c = c'\) is as required. In case of \(c' = x\), the right-hand premise for \(y = b\) yields \(a \in {\text {Jac}}(C,b)\). Again with *aRb* it follows that there is \(c \in C\cup \{\,b\,\}\) such that *bRc*, whence in fact \(c \in C\) since *R* is irreflexive. \(\square \)

### Remark 2

*R*on

*S*, an

*R*-

*clique*is a subset

*C*such that, for every \(a \in 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 \(\overline{R}\)-clique is a complete

*R*-coalition. Conversely, and constructively, every complete

*R*-coalition is an \(\overline{R}\)-clique. More precisely, a subset

*C*of

*S*is an \(\overline{R}\)-clique if and only if it is \(\overline{R}\)-connected as well as \(\overline{R}\)-

*saturated*, the latter of which is to say that \(a \in C\) already if \(a \overline{R} b\) for all \(b \in C\).

## 3 Entailment for Completeness

*S*the relation \({\rhd } \subseteq {\text {Fin}}(S) \times S\) which is defined by the Jacobson radical, i.e., stipulate

*single-conclusion entailment relation*, which is to say that it is

*reflexive*,

*monotone*, and

*transitive*in the following sense:

*U*, i.e.,

*conservative*[25, 26] over \({\rhd }\). 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].

## 4 Binary Trees for Complete Coalitions

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.

*S*be a set. For every \(a \in S\) we first introduce a corresponding letter \(X_a\). Let

*S*and such letters, with the usual provisos on notation, concatenation, etc. Next, we generate inductively a class \(\mathcal {T}\) of finite rooted binary trees \(T \subseteq \mathcal {S}\) as follows:

*leaf*we understand a sequence \(u \in T\) without immediate successor in

*T*. The second rule is to say that, given \(T \in \mathcal {T}\), if

*u*is a leaf of

*T*, then each element

*a*of

*S*gives rise to a new member of \(\mathcal {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 \in S\):

*C*of

*S*, we introduce a relation \(\Vdash _C\) between elements of

*S*and sorted finite sequences in \(\mathcal {S}\) by defining

*c*is a member of every complete coalition over

*C*that further contains \(a_1, \dots , a_k, x_1, \dots , x_\ell \). The case in which this holds with respect to

*every*leaf of a certain tree \(T \in \mathcal {T}\) will later be of particular interest.

With the relation \({\Vdash _C}\) in place, we can now rephrase Proposition 2 as follows.

### Lemma 3

Let \(a,c \in S\) and let \(u \in \mathcal {S}\) be sorted. If \(c \Vdash _C a u\) and \(c \Vdash _C u X_a\), then \(c \Vdash _C u\).

### Proof

Consider \(u = [a_1, \dots , a_k, X_{b_1}, \dots , X_{b_\ell }]\) and suppose that (i) \(c \Vdash _C a u\) and (ii) \(c \Vdash _C u X_a\). To show that \(c \Vdash _C u\), let \(x_1 \in R(b_1), \dots , x_\ell \in R(b_\ell )\). We write \(C'= C \cup \{\, a_1, \dots , a_k, x_1, \dots , x_\ell \,\}\) and need to check that \(c \in {\text {Jac}}(C')\). With \(x_1, \dots , x_\ell \) fixed, premise (i) yields \(c \in {\text {Jac}}(C', a)\), while (ii) implies that, for every \(x \in R(a)\), \(c \in {\text {Jac}}(C', x)\). Now Proposition 2 implies \(a \in {\text {Jac}}(C')\). \(\square \)

Given a subset *C* and an element *c* of *S*, let us say that a tree \(T \in \mathcal {T}\) *terminates for C in c* if \(c \Vdash _C {\text {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.

### Proposition 3

Let *C* be a subset and *c* an element of *S*. The following are equivalent.

- 1.
\(c \in {\text {Jac}}(C)\).

- 2.
There is \(T \in \mathcal {T}\) which terminates for

*C*in*c*.

### Proof

If \(c \in {\text {Jac}}(C)\), then \(c \Vdash _C []\) by (6), which is to say that [] terminates for *C* in *c*. Conversely, suppose that \(T \in \mathcal {T}\) is such that \(c \Vdash _C {\text {sort}}(u)\) for every leaf *u* of *T*. We argue by induction on *T* to show that \(c \in {\text {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 \Vdash _C {\text {sort}}(ua) = a\,{\text {sort}}(u)\) as well as \(c \Vdash _C {\text {sort}}(uX_a)={\text {sort}}(u)X_a\) for a certain \(a \in S\). Lemma 3 implies that \(c \Vdash _C {\text {sort}}(u)\), whence we reduce to \(T'\), to which the induction hypothesis applies. \(\square \)

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 \in \mathcal {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 \in \mathcal {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 \in 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 \subseteq C_m\), then \(c \in C_m\) because \(c \in {\text {Jac}}(C) \subseteq {\text {Jac}}(C_m) = C_m\) by Proposition 3 and the fact that every complete coalition is radical.

### Remark 4

*C*in

*c*.

^{3}This is due to the constructive character of Proposition 3 and the following Brouwer–style counterexample. Let \(\varphi \) be a bounded formula.

^{4}Let \(S = \{\,0,1\,\}\) and put

*Weak Restricted Law of Excluded Middle*(WREM) holds.

## 5 Applications

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 \(\overline{R}\) is the relation one actually one wants to consider. This clearly fits the concept of coalition we are employing.

**Hausdorff’s Principle**

*S*we consider the binary relation

*R*of

*incomparability*, which is

*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

*S*is not totally ordered by \(\leqslant \), as witnessed by a certain element

*a*of

*S*incomparable to some \(b \in 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 Open image in new window thus turns out equivalent to AC through Hausdorff’s principle [18, 19, 22].

**Maximal Cliques**

*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

*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

^{6}

## 6 Conclusion

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].

## Footnotes

- 1.
Incidentally, the term “coalition”, which we use here for sake of intuition, is standard terminology in game theory to denote a group of agents [39].

- 2.
- 3.
One of the anonymous referees has kindly drawn our attention to this.

- 4.
A set-theoretic formula \(\varphi \) is

*bounded*if only set-bounded quantifiers \(\forall x \in y\) and \(\exists x \in y\) occur in \(\varphi \). - 5.
A caveat on terminology: this notion is

*a priori*different from the one used in Bell’s Clique Property (cf. Remark 2) but which carries over to graph theory. - 6.
Clique problems, e.g., the problem of finding a

*maximum*clique and that of listing all maximal cliques are prominent in finite graph theory and computational complexity theory [7].

## Notes

### 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.

## References

- 1.Aczel, P.: Zorn’s Lemma in CZF (2002). Unpublished noteGoogle Scholar
- 2.Aczel, P., Rathjen, M.: Notes on constructive set theory. Technical report, Institut Mittag-Leffler (2000). Report No. 40Google Scholar
- 3.Aczel, P., Rathjen, M.: Constructive set theory (2010). https://www1.maths.leeds.ac.uk/~rathjen/book.pdf, book draft
- 4.Bell, J.L.: Zorn’s lemma and complete Boolean algebras in intuitionistic type theories. J. Symb. Log.
**62**(4), 1265–1279 (1997)MathSciNetCrossRefGoogle Scholar - 5.Bell, J.L.: Some new intuitionistic equivalents of Zorn’s lemma. Arch. Math. Logic
**42**(8), 811–814 (2003)MathSciNetCrossRefGoogle Scholar - 6.Berger, U.: A computational interpretation of open induction. In: Titsworth, F. (ed.) Proceedings of the Ninetenth Annual IEEE Symposium on Logic in Computer Science, pp. 326–334. IEEE Computer Society (2004)Google Scholar
- 7.Bondy, J., Murty, U.: Graph Theory, Graduate Texts in Mathematics, vol. 244. Springer, London (2008)Google Scholar
- 8.Campbell, P.J.: The origin of “Zorn’s lemma”. Historia Math.
**5**, 77–89 (1978)MathSciNetCrossRefGoogle Scholar - 9.Cederquist, J., Coquand, T.: Entailment relations and distributive lattices. In: Buss, S.R., Hájek, P., Pudlák, P. (eds.) Logic Colloquium 1998. Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Prague, Czech Republic, 9–15 August 1998. Lect. Notes Logic, vol. 13, pp. 127–139. A. K. Peters, Natick, MA (2000)Google Scholar
- 10.Ciraulo, F., Rinaldi, D., Schuster, P.: Lindenbaum’s Lemma via Open Induction. In: Kahle, R., Strahm, T., Studer, T. (eds.) Advances in Proof Theory. PCSAL, vol. 28, pp. 65–77. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-29198-7_3
- 11.Coquand, T.: A note on the open induction principle. Technical report, Göteborg University (1997). www.cse.chalmers.se/~coquand/open.ps
- 12.Coquand, T., Lombardi, H., Quitté, C.: Dimension de Heitmann des treillis distributifs et des anneaux commutatifs. Publications Mathématiques de Besançon. Algèbre et Théorie des Nombres, pp. 57–100 (2006)Google Scholar
- 13.Coste, M., Lombardi, H., Roy, M.F.: Dynamical method in algebra: effective Nullstellensätze. Ann. Pure Appl. Logic
**111**(3), 203–256 (2001)MathSciNetCrossRefGoogle Scholar - 14.Felgner, U.: Untersuchungen über das Zornsche Lemma. Compos. Math.
**18**, 170–180 (1967)zbMATHGoogle Scholar - 15.Fellin, G.: The Jacobson radical: from algebra to logic. Master’s thesis. Università di Verona, Dipartimento di Informatica (2018)Google Scholar
- 16.Fellin, G., Schuster, P., Wessel, D.: The Jacobson radical of a propositional theory. In: Piecha, T., Schroeder-Heister, P. (eds.) Proof-Theoretic Semantics: Assessment and Future Perspectives. Proceedings of the Third Tübingen Conference on Proof-Theoretic Semantics, 27–30 March 2019, pp. 287–299. University of Tübingen (2019). http://dx.doi.org/10.15496/publikation-35319
- 17.Hausdorff, F.: Grundzüge der Mengenlehre. Verlag von Veit & Comp, Leipzig (1914)zbMATHGoogle Scholar
- 18.Herrlich, H.: Axiom of Choice, Lecture Notes in Mathematics, vol. 1876. Springer, Berlin (2006). https://doi.org/10.1007/11601562
- 19.Howard, P., Rubin, J.: Consequences of the Axiom of Choice. American Mathematical Society, Providence (1998)CrossRefGoogle Scholar
- 20.Jacobson, N.: The radical and semi-simplicity for arbitrary rings. Am. J. Math.
**67**(2), 300–320 (1945). https://doi.org/10.2307/2371731MathSciNetCrossRefzbMATHGoogle Scholar - 21.Lombardi, H., Quitté, C.: Commutative Algebra: Constructive Methods. Finite Projective Modules, Algebra and Applications, vol. 20. Springer, Netherlands (2015). https://doi.org/10.1007/978-94-017-9944-7
- 22.Moschovakis, Y.: Notes on Set Teory. Undergraduate Texts in Mathematics, Second edn. Springer, New York (2006)Google Scholar
- 23.Raoult, J.C.: Proving open properties by induction. Inform. Process. Lett.
**29**(1), 19–23 (1988)MathSciNetCrossRefGoogle Scholar - 24.Rinaldi, D., Schuster, P.: A universal Krull-Lindenbaum theorem. J. Pure Appl. Algebra
**220**, 3207–3232 (2016)MathSciNetCrossRefGoogle Scholar - 25.Rinaldi, D., Schuster, P., Wessel, D.: Eliminating disjunctions by disjunction elimination. Bull. Symb. Logic
**23**(2), 181–200 (2017)MathSciNetCrossRefGoogle Scholar - 26.Rinaldi, D., Schuster, P., Wessel, D.: Eliminating disjunctions by disjunction elimination. Indag. Math. (N.S.)
**29**(1), 226–259 (2018)Google Scholar - 27.Rinaldi, D., Wessel, D.: Cut elimination for entailment relations. Arch. Math. Logic
**58**(5–6), 605–625 (2019)Google Scholar - 28.Schlagbauer, K., Schuster, P., Wessel, D.: Der Satz von Hahn-Banach per Disjunktionselimination. Confluentes Math.
**11**(1), 79–93 (2019)MathSciNetCrossRefGoogle Scholar - 29.Schuster, P.: Induction in algebra: a first case study. In: 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012. Dubrovnik, Croatia, pp. 581–585. IEEE Computer Society Publications (2012)Google Scholar
- 30.Schuster, P.: Induction in algebra: a first case study. Log. Methods Comput. Sci.
**9**(3), 20 (2013)MathSciNetCrossRefGoogle Scholar - 31.Schuster, P., Wessel, D.: Syntax for semantics: Krull’s maximal ideal theorem. In: Heinzmann, G., Wolters, G. (eds.) Paul Lorenzen: Mathematician and Logician. Springer, forthcomingGoogle Scholar
- 32.Schuster, P., Wessel, D.: A general extension theorem for directed-complete partial orders. Rep. Math. Logic
**53**, 79–96 (2018)MathSciNetzbMATHGoogle Scholar - 33.Schuster, P., Wessel, D.: Resolving finite indeterminacy: a definitive constructive universal prime ideal theorem. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020), 8–11 July 2020, Saarbrücken, Germany. ACM, New York (2020)Google Scholar
- 34.Schuster, P., Wessel, D., Yengui, I.: Dynamic evaluation of integrity and the computational content of Krull’s lemma (2019, preprint)Google Scholar
- 35.Scott, D.: Completeness and axiomatizability in many-valued logic. In: Henkin, L., Addison, J., Chang, C., Craig, W., Scott, D., Vaught, R. (eds.) Proceedings of the Tarski Symposium (Proceedings of Symposia in Pure Mathematics, vol. XXV, University of California, Berkeley, California (1971). pp. 411–435. American Mathematical Society, Providence (1974)Google Scholar
- 36.Wessel, D.: Points, ideals, and geometric sequents. Technical report, University of Verona (2018)Google Scholar
- 37.Yengui, I.: Making the use of maximal ideals constructive. Theoret. Comput. Sci.
**392**, 174–178 (2008)MathSciNetCrossRefGoogle Scholar - 38.Yengui, I.: Constructive Commutative Algebra. Projective Modules Over Polynomial Rings and Dynamical Gröbner Bases, Lecture Notes in Mathematics, vol. 2138. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19494-3
- 39.Young, H.P., Zamir, S. (eds.): Handbook of Game Theory, Volume 4. Handbooks in Economics, 1st edn. North-Holland, Amsterdam (2015)Google Scholar
- 40.Zorn, M.: A remark on method in transfinite algebra. Bull. Am. Math. Soc.
**41**, 667–670 (1935)MathSciNetCrossRefGoogle Scholar