The Jacobson radical for an inconsistency predicate

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

1. Introduction

Hausdorff’s Maximal Chain Principle asserts that every totally ordered subset of a partially ordered set S is contained in a maximal one. In first-order terms, a chain C is maximal precisely when, for every $a \in S$ , if $C \cup {a}$ is a chain, then $a \in C$ ; or, equivalently, either $a \in C$ or a is incomparable with at least one $b \in C$ . Especially the latter characterisation, which is to say that $\begin{matrix} (1) & a \in C or (\exists b \in C) (a ≰ b \land b ≰ a), \end{matrix}$ is somewhat reminiscent of one of the characterisations of a maximal ideal in a commutative ring A with 1: a proper ideal M of A is maximal if and only if, for every $a \in A$ , $\begin{matrix} (2) & a \in M or (\exists b \in M) (⟨ a, b ⟩ ∋ 1); \end{matrix}$ in other words, either $a \in M$ or a is comaximal with some $b \in M$ .1

¹
Maximality criteria, though to a different end, have also been put under constructive scrutiny in the context of Boolean algebras and locales by Mulvey [40]. One of the anonymous referees kindly brought this to our attention.

Moreover, with the Axiom of Choice AC at hand it is possible to describe in first-order terms the common part of all maximal ideals containing any given ideal I of A: that is, the Jacobson radical [32] of I. This is Krull’s Maximal Ideal Theorem [34] seen as an intersection principle, and has given rise to a first-order notion of the Jacobson radical which suits the needs of constructive algebra [37,61,68].

By analogy, we can give a first-order definition of the Jacobson radical $Jac (C)$ of a chain C in a poset S, and prove with AC that $Jac (C)$ coincides with the intersection of all maximal chains containing C. So Hausdorff’s principle too is recast as an intersection principle. All this, however, can even be done in a more general fashion, and a simple direct and elementary interpretation is possible. Hence the purpose of this paper is twofold: to communicate a potentially new form of AC which in a natural way encompasses both Krull’s theorem and Hausdorff’s principle; and to describe the constructive or syntactical underpinning.

In Sections 2 and 3, alongside the analogy with ring theory, we define our general concepts of coalition and Jacobson radical. In Section 4 we show that the latter is a closure operator (Proposition 1) and as such a covering or consequence relation which can be defined inductively (Theorem 1). In Section 5 we then study the semantics, which is complete coalitions, and prove the appropriate intersection, logical completeness or semantic conservation theorem (Theorem 2, with AC). In Section 6 we discuss several applications: maximal ideals of finitary closure operations with concrete instances for commutative rings and propositional theories, as well as maximal chains and maximal cliques. Section 7 sheds additional light. Here we approximate complete coalitions syntactically by paths in finite binary trees of a suitable inductively generated class $T$ , and thus can prove the syntactical counterpart of our Theorem 2: to belong to $Jac (C)$ for a given coalition C is tantamount to the existence of a tree in $T$ of which all root-to-leaf paths terminate in C (Theorem 3).

1.1. Disclaimer

This is a revised and extended journal version of our CiE 2020 conference paper [59]. The present note deviates from its forerunner by replacing the symmetric irreflexive relation on the underlying set S, as was crucial for [59], with a monotone family of finite subsets of S that is thought as an abstract form of inconsistency. This move not only makes a more natural treatment possible, but widens scope considerably, as witnessed, e.g., by Krull’s Maximal Ideal Theorem (cf. Section 6).

1.2. On method and foundations

The content of this paper is elementary and can be formalised in a suitable fragment of constructive set theory CZF enriched, where necessary, with the regular extension axiom so as to account comprehensively for generalised inductive definitions [3,4,51]. Due to the corresponding choice of intuitionistic logic, some assumptions have to be made explicit which otherwise would be trivial with classical logic. 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$ .

By a finite set we understand a set that can be written as ${a_{1}, \dots, a_{n}}$ for some $n ⩾ 0$ ;2

²
As in [53,54], for the sake of a slicker wording we thus deviate from the prevalent terminology of constructive mathematics and set theory [3,4,8,9,37,39]: (1) to call ‘subfinite’ or ‘finitely enumerable’ a finite set in the sense above, i.e. a set S for which there is a surjection from ${1, \dots, n}$ to S for some $n ⩾ 0$ ; and (2) to reserve the term ‘finite’ to sets which are in bijection with ${1, \dots, n}$ for a necessarily unique $n ⩾ 0$ . Also, finite sets in this stricter sense do not play a role in this paper.

we say that any such number n enumerates the finite set. Every finite set is either empty or inhabited. We denote by

Fin (S)

the class of all finite subsets of a set S, which form a set in

CZF

, while the generic subsets of a set S form a proper class

Pow (S)

. Rather than

U \in Fin (S)

we often write

U \subseteq_{fin} S

, and typically use the letters U, V, W for finite subsets of S.

From formal topology [55] we borrow the overlap symbol: the notation $U ≬ V$ is to say that the sets U and V have an element in common. Where no confusion may arise, we write U, V for set union $U \cup V$ , and similarly U, a for $U \cup {a}$ .

Last but not least, to pin down Theorem 2, and to point out certain of its consequences later on, requires some classical logic and the Axiom of Choice (AC), which will be used in the form of Open Induction (OI) [50], as recalled below. For simplicity we switch in such a case to classical set theory ZFC , signalling this appropriately.

The following lemma is utterly trivial with classical logic but allows for a simple constructive proof, as well. We state this here to be used in the following section. Lemma 1.

Let S and T be sets. If $U \subseteq_{fin} S \cup T$ , then either $U \subseteq S$ or there is $V \subseteq_{fin} T$ such that $U \subseteq S \cup V$ .

Proof.

We argue by induction on the number n enumerating U. The case $n = 0$ , i.e., $U = \emptyset$ is clear. Next consider the case in which $U = U^{'} \cup {a}$ and the inductive hypothesis applies to $U^{'}$ . Accordingly, there are two cases to consider: either (a) $U^{'} \subseteq S$ or else (b) there is $W \subseteq_{fin} T$ such that $U^{'} \subseteq S \cup W$ . Both cases lead to the desired conclusion by another case distinction, respectively, on whether $a \in S$ or $a \in T$ . For (a) this is clear; in the case of (b) we have $\begin{matrix} U = U^{'} \cup {a} \subseteq S \cup W \cup {a}, \end{matrix}$ and so either $V = W$ or $V = W \cup {a}$ – depending on whether $a \in S$ or $a \in T$ – will do. □

2. Coalitions

Throughout, let S be a set, and let $R \subseteq Fin (S)$ be monotone, that is, for all $U, V \in Fin (S)$ , if $U \in R$ and $U \subseteq V$ , then $V \in R$ . We say that $R$ is proper if $R \neq Fin (S)$ , which, however, we do not require from the outset.

Employing predicate notation we write $R (U)$ for $U \in R$ . This extends to arbitrary subsets T of S by writing $R (T)$ for $Fin (T) ≬ R$ , which is to say that there is $U \subseteq_{fin} T$ such that $R (U)$ . Moreover, we carry further our notational convention on set union, i.e., we write $R (U, V)$ for $R (U \cup V)$ etc.

Lemma 2.
Let $T \subseteq S$ and $W \subseteq_{fin} S$ . Then $R (T, W)$ if and only if there is $V \subseteq_{fin} T$ such that $R (V, W)$ .
Proof.
Suppose that there is $U \subseteq_{fin} T \cup W$ such that $R (U)$ . By Lemma 1 either $U \subseteq W$ or there is $V \subseteq_{fin} T$ such that $U \subseteq V \cup W$ . Both cases yield the desired conclusion by monotonicity of $R$ . The converse is immediate. □
Definition 1.
A subset C of S is a coalition (with respect to $R$ ) if $\neg R (C)$ , i.e. $Fin (C) \cap R = \emptyset$ .

For instance, S is a coalition if and only if $R = \emptyset$ . Perhaps more importantly, ∅ is a coalition if and only if $\emptyset \notin R$ ; by monotonicity this amounts to $R$ being proper. Also, coalitions are closed under directed union.

Our choice of terminology follows [59] – on the topic of which the present note sheds further light – simply to have at hand a notion which to our knowledge is not yet of use in any of the concrete settings we consider later on.3
³
The term “coalition”, which we use for sake of intuition, is standard terminology in game theory to denote a group of agents [69]. The present one requires a rather conservative reading: our coalitions don’t allow for disagreement (in terms of $R$ ) amongst their ranks.

Definition 2.
A subset C of S is complete (with respect to $R$ ) if, for every $a \in S$ , $\begin{matrix} (3) & a \in C or R (C, a) . \end{matrix}$

Note that S is always complete; and that ∅ is complete precisely when $R$ has as elements all singleton subsets of S or, equivalently, all inhabited subsets of S.

It is perhaps instructive to brandish any $U \in R$ as “inconsistent” – quite literally in the case of logic, where $R (C)$ is to be read as $C ⊢ ⊥$ . In an algebraic setting, $R (C)$ is to say that C generates a unit element (see Section 6). A coalition is then a subset of S that is free of finite inconsistent subsets, on account of which it may be considered “consistent”. A complete subset C is such that, given any $a \in S$ , this a either belongs to C, or else C has a finite subset which together with a turns out inconsistent. With this intuition, complete coalitions capture in more concrete terms the notion of maximal consistency.
Remark 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 $Fin (C) \cap R = \emptyset$ , the second alternative of completeness (3) entails $a \notin C$ ; whence C is detachable. As for 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 by Lemma 2 there is $U \subseteq_{fin} C$ such that $R (U, a)$ , but the latter case is impossible as D is a coalition. As for the converse, if C is a maximal coalition and $a \notin C$ , then $C \cup {a}$ cannot, due to maximality of C, in turn be a coalition. With classical logic, the latter statement is to say that $R (C, a)$ . □

If C is a coalition, let us write $\begin{matrix} Comp / C \end{matrix}$ for the collection of all complete coalitions that contain C, with the special case $Comp = Comp / \emptyset$ . Since every complete coalition is detachable (Remark 1), these collections are sets due to the presence in CZF of the exponentiation axiom [2–4].
3. Jacobson radical

Recall from [16,37] that the Jacobson radical [32,33] of an ideal J of a commutative ring A with 1 – and likewise for distributive lattices [27,63] – can be defined in first-order terms as $\begin{matrix} (4) & Jac (J) = {a \in A ∣ (\forall b \in A) (1 \in ⟨ a, b ⟩ \to 1 \in ⟨ J, b ⟩)} . \end{matrix}$ Here sharp brackets denote generated ideals, and one can equivalently let b range over finitely generated ideals [37].

Recently this has been adopted in propositional logic, including a variant of Lindenbaum’s Lemma as the semantics of Glivenko’s Theorem [20,22]. In this context ⊢ stands for (deducibility in) an intermediate logic in a propositional language S. Now (4) translates into a definition of the Jacobson radical of a theory T in S as $\begin{matrix} (5) & Jac (T) = {a \in S ∣ (\forall b \in S) (a, b ⊢ ⊥ \to T, b ⊢ ⊥)} \end{matrix}$ by replacing comaximality in (4), i.e., to generate the unit, with inconsistency in (5), i.e., to prove absurdity.

The consequents in the defining properties of (4) and (5) are actually witnessed by single elements of J and T, respectively. With an eye towards a more abstract concept, rather than turning this observation into a requirement, we will ignore it to achieve some leeway for applications; it is here that $R$ comes to play its decisive role.

By analogy with the settings of ring theory and logic, we put the following.

Definition 3.
The Jacobson radical of a subset C of S is defined by $\begin{matrix} Jac (C) = {a \in S ∣ (\forall U \in Fin (S)) (R (a, U) \to R (C, U))} . \end{matrix}$

This can be put more succinctly as $\begin{matrix} (6) & Jac (C) = {a \in S ∣ (\forall U \in R_{a}) R (C, U)}, \end{matrix}$ where $\begin{matrix} R_{a} = {U \in Fin (S) ∣ R (a, U)} \end{matrix}$ is the set of “opponents” U of a, i.e., the U “pseudo-complementing” a with respect to $R$ . Notice that Jac is monotone, i.e., such that $Jac (C) \subseteq Jac (D)$ whenever $C \subseteq D$ ; and expansive, i.e., such that $C \subseteq Jac (C)$ . Also, if $R (C)$ , then $Jac (C) = S$ ; conversely, $R (C)$ whenever $\emptyset \in R_{a}$ for some $a \in Jac (C)$ , e.g., if $R$ is inhabited and $Jac (C) = S$ . Moreover, for the particular case of $C = \emptyset$ , note that $\begin{matrix} (7) & Jac (\emptyset) = {a \in S ∣ R_{a} \subseteq R} . \end{matrix}$

In ZFC , the Jacobson radical of an ideal J as in (4) is the intersection of all maximal ideals that contain J [37], whereas the Jacobson radical of a theory T as in (5) is the intersection of all complete theories that contain T [22]. Similarly, still with AC, the Jacobson radical of a coalition C will prove to be the intersection of all complete coalitions that contain C (Theorem 2 below).
Definition 4.
A coalition C such that $Jac (C) = C$ is said to be radical.
Lemma 3.
Let $C \subseteq S$ and $a \in Jac (C)$ . If $R (C, a)$ , then $R (C)$ .
Proof.
Suppose that $R (C, a)$ for some $a \in Jac (C)$ . By Lemma 2 there is $V \subseteq_{fin} C$ such that $R (V, a)$ . Now $a \in Jac (C)$ implies $R (V, C)$ which is to say that $R (C)$ . □
Proposition 1.
The Jacobson radical defines a closure operator on S and 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)) \subseteq Jac (C)$ , where $C \subseteq S$ . To this end, suppose that $a \in Jac (Jac (C))$ and let $V \in R_{a}$ . Then $R (Jac (C), V)$ and by Lemma 2 there is $U \subseteq_{fin} Jac (C)$ such that $R (U, V)$ . Lemma 3 now implies that $R (C, V)$ . As regards the add-on, we show that if $R (Jac (C))$ , then $R (C)$ . In fact, consider $U \subseteq_{fin} Jac (C)$ and suppose that $R (U)$ . Either this U is empty and nothing need be done. If there is $a \in U$ , then $a \in Jac (C)$ implies $R (C, U)$ , and Lemma 3 yields $R (C)$ . □

In particular, if C is a coalition, then $Jac (C)$ is a radical coalition.
4. Inductive generation

As is well-known, every closure operator corresponds with a consequence relation on S (which is finitary precisely if the former is algebraic; see also Section 6 below), and which in turn can, synonymously, be read as a covering relation [13,17,55], i.e., a relation ⊲ between elements and subsets of S that is reflexive and transitive: $\begin{matrix} a \in U a ⊲ U (R) a ⊲ U (\forall b \in U) b ⊲ V a ⊲ V (T) \end{matrix}$

We show now that membership to the Jacobson radical is an inductively generated predicate. The crucial clause will help in the next Section 5 to prove (in ZFC ) that Jac is determined by complete coalitions. To this end, we define a relation ⊲ between elements and subsets of S inductively by the following rules of reflexivity $(R)$ , extension $(E)$ , and completeness $(C)$ , $\begin{matrix} a \in U a ⊲ U (R) R (U) a ⊲ U (E) a ⊲ U, x (\forall V \in R_{x}) a ⊲ U, V a ⊲ U (C) \end{matrix}$

Our choice of terminology anticipates the semantics of ⊲, which is determined by complete coalitions (see the following Section 5). Rule $(C)$ corresponds to the completeness requirement (3): if U, x covers a, and so does U, V for every $V \in R_{x}$ , then U covers a. This is a form of conservativity, allowing us in Section 7 to do as if a given coalition were complete to test membership in the Jacobson radical. In logic, completeness $(C)$ is related to (the rule corresponding to) tertium non datur, while $(E)$ is related to ex falso quodilbet (see also Example 2).

Theorem 1.
Let $a \in S$ and $U \subseteq S$ . The following are equivalent.
$a ⊲ U$ .

$a \in Jac (U)$ .
In particular, ⊲ is a covering relation, and Jac is inductively generated.
Proof.
To show that the first item implies the second, we argue by induction on $a ⊲ U$ . Both the cases for $(R)$ and $(E)$ are easily handled, so we concentrate on $(C)$ . Accordingly, suppose that (i) $a \in Jac (U, x)$ and (ii) $a \in Jac (U, V)$ for every $V \in R_{x}$ . We need to check that $a \in Jac (U)$ , whence let $U_{0} \in R_{a}$ . Then (i) yields $R (U, x, U_{0})$ , which implies that there is $U_{1} \subseteq_{fin} U$ such that $U_{0} \cup U_{1} \in R_{x}$ . Now (ii) yields $a \in Jac (U, U_{0}, U_{1})$ which is to say that $a \in Jac (U, U_{0})$ . Since $U_{0} \in R_{a}$ , this implies $R (U, U_{0})$ , as required.

Conversely, suppose that $a \in Jac (U)$ . In order to show $a ⊲ U$ , we use $(C)$ . To this end, notice that on the one hand $a ⊲ U$ , a holds by (R). Next we check that $a ⊲ U, V$ for every $V \in R_{a}$ . This holds by (E), for whenever $R (a, V)$ , we obtain $R (U, V)$ from $a \in Jac (U)$ .

The first add-on is a consequence of the fact that Jac is a closure operator (Proposition 1). □

5. Completeness

It will be seen in this section, working in ZFC , that membership in the Jacobson radical of a coalition C can be tested on the complete coalitions in which C is contained. In view of Theorem 1, this amounts to a logical completeness result (Theorem 2). To prove this, it is perhaps best to use Open Induction (OI) [7,15,50], which Raoult [50] has deduced from the Kuratowski–Zorn Lemma, and to which OI is ZF -equivalent.

Recall that OI asserts that if $(X, ⩽)$ is a directed-complete poset (a dcpo)4

⁴
Since for Theorem 2 we switch to ZFC anyway, we do not refer to forms of OI (say, for set-generated directed-complete poclasses [1]) more pertinent to CZF . See, e.g., [58].

and if O is a predicate on X which is both (i) open, i.e., such that whenever

D \subseteq X

is directed and

O (⋁ D)

, then

(\exists x \in D) O (x)

; as well as (ii) progressive, i.e., such that if

O (y)

for every

y > x

, then

O (x)

; then

(\forall x \in X) O (x)

We further need that it be decidable whether or not a coalition C is complete, and if not that it be witnessed by a certain element which gives rise to a proper extension of C. Thus, to state and prove Theorem 2, we have to switch to ZFC , while stressing the fact that OI provides for a rather natural treatment, apt for constructivisation perhaps even beyond Sections 4 and 7 below.5

⁵

For similar and related cases see [14,52,56,57].

Theorem 2 (

ZFC

If C is a coalition, then $\begin{matrix} Jac (C) = ⋂ Comp / C . \end{matrix}$

Proof.
Let $a \in Jac (C)$ and suppose that D is a complete coalition which contains C. By completeness, either $a \in D$ right away, or else $R (D, a)$ . But since $a \in Jac (C) \subseteq Jac (D)$ , the latter case would imply $R (D)$ , by way of which D would fail to be a coalition after all.

As regards the converse, let $D$ denote the family of radical coalitions D that contain C, suppose that $a \in D$ for every complete $D \in D$ , and consider the predicate $O (D) \equiv a \in D$ . This $O$ is certainly open; to see that $O$ is progressive, let $D \in D$ and suppose that $O (E)$ for every $E ⊋ D$ . We distinguish cases. If D is complete, then $a \in D$ by the overall assumption. If D is not complete, then there is some $x \notin D$ such that $D \cup {x}$ is a coalition; whence $Jac (D, x)$ is a radical coalition which properly exceeds D, and therefore $a \in Jac (D, x)$ by the induction hypothesis. In the latter case, moreover, if $V \in R_{x}$ , then $a \in Jac (D, V)$ ! (In fact, since $D \cup {x}$ is a coalition, $V ⊈ D$ . Then two cases come into question: either $D \cup V$ is a coalition, so again $a \in Jac (D, V)$ right away, by the induction hypothesis; or else $R (D, V)$ , but then $a \in Jac (D, V)$ is trivial.) By Theorem 1 and the clause for completeness $(C)$ it now follows that $a \in Jac (D) = D$ . Hence $O (D)$ for every $D \in D$ by OI. In particular $O (Jac (C))$ , which is to say that $a \in Jac (C)$ . □

6. Applications

We will now treat several applications of Theorem 2 in detail: maximal ideals of consequence relations with concrete instances in ring theory and propositional logic, maximal cliques in graphs, and maximal chains of partially ordered sets. Most of the discussion to follow is set in ZFC . In all cases Theorem 1 constitutes the corresponding constructive underpinning.

6.1. Ideals and theories

By a consequence relation or single-conclusion entailment relation we understand a relation $\begin{matrix} ⊢ \subseteq Fin (S) \times S \end{matrix}$ which is reflexive, monotone and transitive in the following sense: $\begin{matrix} U ∋ a U ⊢ a (R) U ⊢ a U, V ⊢ a (M) U ⊢ b U, b ⊢ a U ⊢ a (T) \end{matrix}$ where as usual $U, V \equiv U \cup V$ and $U, b \equiv U \cup {b}$ . It is well-known that every consequence relation ⊢ gives way to an algebraic closure operator $⟨ - ⟩ : Pow (S) \to Pow (S)$ defined by $\begin{matrix} a \in ⟨ T ⟩ \equiv (\exists U \in Fin (T)) U ⊢ a . \end{matrix}$ Conversely, given $⟨ - ⟩$ , by stipulating $\begin{matrix} U ⊢ a \equiv a \in ⟨ U ⟩ \end{matrix}$ we gain back a consequence relation ⊢ from an algebraic closure operator $⟨ - ⟩$ .

The ideals of a consequence relation ⊢ are the subsets J of S which are closed with respect to the corresponding closure operator $⟨ - ⟩$ , which is to say that $J = ⟨ J ⟩$ . Hence the ideals of ⊢ are precisely the subsets J of S such that if $J \supseteq U$ and $U ⊢ a$ , then $a \in J$ . As for ideals of rings, we say that an ideal J of ⊢ is proper whenever $J \neq S$ .

A consequence relation ⊢ gives rise to an inconsistency predicate in a natural way: $\begin{matrix} (8) & R = {U \in Fin (S) ∣ ⟨ U ⟩ = S} . \end{matrix}$ For this choice of $R$ , the Jacobson radical of a subset T of S is $\begin{matrix} Jac (T) = {a \in S ∣ (\forall U \in Fin (S)) (⟨ U, a ⟩ = S \to ⟨ U, T ⟩ = S)} . \end{matrix}$ Note that $Jac (⟨ T ⟩) = Jac (T)$ ; in particular, $⟨ T ⟩ \subseteq Jac (T)$ .

Remark 2.
Every proper ideal of ⊢ is a coalition; and every complete coalition C is an ideal.
Proof.
To show the second statement, let C be a complete coalition. If $C \supseteq U ⊢ a$ , then by completeness either $a \in C$ anyway, or else by Lemma 2 there is $V \subseteq_{fin} C$ such that $S = ⟨ V, a ⟩ \subseteq ⟨ V, U ⟩$ . In the latter case we have $R (C)$ , but C is supposed to be a coalition. □

In the present context, Theorem 2 reads as follows.
Proposition 2 ( ZFC ).

If J is an ideal6

⁶
There is no need to suppose the ideal J to be proper: in ZFC one can tell whether $J = S$ , in which case the claim holds trivially.

of a consequence relation ⊢, then

\begin{matrix} ⋂ Comp / J = {a \in S ∣ (\forall U \in Fin (S)) (⟨ U, a ⟩ = S \to ⟨ U, J ⟩ = S)} . \end{matrix}

In view of Remark 1, Proposition 2 is a universal maximal ideal theorem which subsumes – to mention only two – Krull’s Maximal Ideal Theorem in commutative ring theory, and Lindenbaum’s Lemma for propositional logic, to which we now turn our attention. In both cases there is a convincing element [52–54] for ⊢, i.e., there is $e \in S$ for which $⟨ e ⟩ = S$ ; whence a subset C of S is a coalition if and only if the closure of C is a proper ideal.

6.1.1. Krull’s Maximal Ideal Theorem

Let $S = A$ be a commutative ring with 1 and consider ⊢ on A as given by ideal generation, i.e., $\begin{matrix} a_{1}, \dots, a_{k} ⊢ b \equiv (\exists r_{1}, \dots, r_{k} \in A) \sum_{i = 1}^{k} r_{i} a_{i} = b . \end{matrix}$ The ideals of ⊢ are the ideals of the ring A, and the corresponding inconsistency predicate (8) consists of the finite comaximal subsets of A. Hence the complete coalitions are in ZF precisely the maximal ideals of the ring A, i.e., the ideals which are maximal among the proper ideals; and the Jacobson radical $Jac (J)$ of an ideal J is the expected one (4).

In particular, the related instance of Proposition 2 says that $Jac (J)$ equals the intersection of all maximal ideals that contain J. Incidentally, this variant of Krull’s Maximal Ideal Theorem helps (and so does the instance in Section 6.2 below) to calibrate our intersection principle:

Proposition 3 ( ZF ).

The universal validity of Theorem 2 , for every set S and every monotone family $R \subseteq Fin (S)$ , is equivalent to AC.

Proof.
Krull’s Maximal Ideal Theorem implies AC [5,28,29,34], and follows from Theorem 2 via Proposition 2. □

On the other hand the structure of a ring is rich enough to allow for a concrete application, as follows.
Example 1.
We consider McCabe’s short proof of Zariski’s Lemma [38].7
⁷
An elementary, constructive proof of Zariski’s Lemma has recently been found by Wiesnet [65,66].

Here we focus on the second of only three short paragraphs, in which by way of a generic maximal ideal a certain element is shown to be invertible. Suppose that A is without zero-divisors [37], i.e., such that $\begin{matrix} (\forall a, b \in A) (a b = 0 \to a = 0 \lor b = 0) . \end{matrix}$ The respective argument of McCabe’s boils down to observing that if $a \in A$ is not invertible, and such that the localization $A [a^{- 1}]$ is a field, then $a \in Jac (\emptyset)$ . This can now be shown by an appeal to Theorem 1. To this end, by the corresponding rule for completeness (C) with $U = \emptyset$ and $a = x$ , it suffices to check that $a \in Jac (V)$ for every $V \in Fin (A)$ with $1 \in ⟨ V, a ⟩$ . In fact, suppose that $b \in ⟨ V ⟩$ and $r \in A$ are such that $r a + b = 1$ . Since a is not invertible, $b \neq 0$ in A. Next, because $A [a^{- 1}]$ is a field, either $b = 0$ in $A [a^{- 1}]$ , which is to say that $a^{n} b = 0$ for some $n ⩾ 0$ , and thus $a = 0 \in Jac (V)$ since $b \neq 0$ and A is without zero-divisors; or b is invertible in $A [a^{- 1}]$ , and then there are $c \in A$ and $n ⩾ 0$ such that $b c = a^{n}$ . Now $a^{n} \in Jac (⟨ V ⟩)$ , by which in fact $a \in Jac (V)$ , again as required. (Recall that by (4) the Jacobson radical is a radical ideal, i.e., if $a^{n} \in Jac (J)$ for some $n ⩾ 0$ , then $a \in Jac (J)$ .)

For related approaches to making the use of maximal ideals constructive, cf. [10,18,37,47,48,61,67,68].
6.1.2. Lindenbaum’s Lemma

Let ⊢ stand for (deducibility in) an intermediate logic in a propositional language S. The ideals of ⊢ are the theories of ⊢ in S, i.e., the subsets of S which are deductively closed with respect to ⊢; and the corresponding inconsistency predicate (8) consists of the finite subsets of S which are inconsistent with respect to ⊢. Hence the complete coalitions are in ZF precisely the complete consistent theories; and $Jac (T)$ is the Jacobson radical (5) of a theory T. This is [22] nothing but the stable closure of T, $\begin{matrix} (9) & Jac (T) = {φ \in S ∣ \neg \neg φ \in T}; \end{matrix}$ whence Proposition 2 instantiates to a variant of Lindenbaum’s Lemma [22]: $Jac (T)$ equals the intersection of all complete consistent theories extending T.

Moreover, (9) prompts a proof of Glivenko’s Theorem [24], as follows.

Example 2.
Let $⊢_{i}$ and $⊢_{c}$ stand for intuitionistic and classical logic in a propositional language S.8
⁸
For the present example we leave unsettled whether entailment relations too fall under the reservations about sequent calculi [43,44] against the context-as-sets paradigm as opposed to the context-as-multisets pattern, and if so whether this affect the usability of entailment relations in proof practice.

Recall from [30,42] that $\begin{matrix} Γ ⊢_{c} φ if and only if Γ, Δ ⊢_{i} φ \end{matrix}$ for a suitable finite set Δ of formulas $ψ \lor \neg ψ$ , where ψ is a propositional variable occurring in Γ or φ. This is at the heart of Glivenko’s Theorem [24], for which we can now give a more conceptual proof, similar to [60]. With $⊢_{i}$ as ⊢ and ⊲ as in Section 4 we show first that $\begin{matrix} (10) & (\forall V \in R_{ψ}) φ ⊲ U, V if and only if φ ⊲ U, \neg ψ . \end{matrix}$ While the right-hand side simply is the instance $V = {\neg ψ}$ of the left-hand side, to deduce the latter from the former let $V \in R_{ψ}$ , that is, $V ⊢ \neg ψ$ . By (5) follows $\neg ψ \in Jac (V)$ , which by Theorem 1 means $\neg ψ ⊲ V$ . Now if $φ ⊲ U, \neg ψ$ , then $φ ⊲ U, V$ as required.

By (10) the corresponding rule for completeness $(C)$ boils down to the analogue of the rule for excluded middle: $\begin{matrix} φ ⊲ Γ, ψ φ ⊲ Γ, \neg ψ φ ⊲ Γ \end{matrix}$ With this at hand we swiftly see that $Γ, Δ ⊢_{i} φ$ entails $φ ⊲ Γ$ , which according to Theorem 1 and (9) means $Γ ⊢_{i} \neg \neg φ$ . In all, $Γ ⊢_{c} φ$ implies $Γ ⊢_{i} \neg \neg φ$ , which is Glivenko’s Theorem [24].

Needless to say, proofs of Glivenko’s Theorem usually go along similar lines overall. Recent literature about Glivenko’s result includes [19,21,23,25,31,36,41,45,46].9
⁹
This list of references is by no means meant exhaustive.

The two foregoing applications are summed up in Table 1.

Table 1
Correspondences for ideals and theories

Krull’s Maximal Ideal Theorem (Section 6.1.1) Lindenbaum’s Lemma (Section 6.1.2)

given structure commutative ring propositional logic

consequence relation ⊢ generation deduction

ideals of ⊢ ideals theories

inconsistent comaximal inconsistent

complete coalition maximal ideal consistent complete theory

Jacobson radical Jacobson radical stable closure

6.2. Cliques and chains

	Krull’s Maximal Ideal Theorem (Section 6.1.1)	Lindenbaum’s Lemma (Section 6.1.2)
given structure	commutative ring	propositional logic
consequence relation ⊢	generation	deduction
ideals of ⊢	ideals	theories
inconsistent	comaximal	inconsistent
complete coalition	maximal ideal	consistent complete theory
Jacobson radical	Jacobson radical	stable closure

Let $R \subseteq S \times S$ be an irreflexive and symmetric relation as studied before [59]. Put $\begin{matrix} (11) & R = {U \in Fin (S) ∣ (\exists a, b \in U) a R b} . \end{matrix}$ This $R$ is certainly monotone and proper. Moreover, $R$ contains no singleton subset, and ${a, b} \in R$ if and only if $a R b$ whenever $a \neq b$ . In particular, $Jac (\emptyset)$ consists of the $a \in S$ which are isolated points with respect to R, by which we mean that $a \overline{R} b$ for all $b \in S$ , where $\overline{R}$ denotes the complementary relation. The coalitions for $R$ are precisely the subsets C of S such that $a \overline{R} b$ for all $a, b \in C$ . For example, ${a, b}$ is a coalition if and only if $a \overline{R} b$ .

A coalition C is complete if and only if, for every $a \in S$ , $\begin{matrix} a \in C or (\exists b \in C) a R b; \end{matrix}$ whence we get back the complete coalitions of [59]. Combining in ZFC the corresponding instance of (7) with Theorem 2, we see that the isolated points are exactly the ones which belong to all complete coalitions, that is, $\begin{matrix} (12) & ⋂ Comp = {a \in S ∣ (\forall b \in S) a \overline{R} b}, \end{matrix}$ which generalises to complete coalitions that contain a given one [59, Proposition 1]. By suitable instantiation we obtain principles in ZFC for maximal cliques in graphs, and maximal chains of partially ordered sets, as follows.10

¹⁰
In [59, Remark 2] we have discussed in terms of coalitions Bell’s related notion of cliques for binary relations [6].

6.2.1. Maximal cliques

Let $G = (V, E)$ be an undirected graph, with V as the set of vertices and E as the set of edges; in particular, E is a set of unordered pairs of elements of V. On V we now consider the relation of nonadjacency, putting $\begin{matrix} a R b \equiv a \neq b \land {a, b} \notin E . \end{matrix}$ With classical logic, a coalition for the corresponding $R$ as in (11) is nothing but a clique [11], i.e., a set of mutually adjacent vertices,11

¹¹
In other words, the induced subgraph is complete in the sense of graph theory.

and the complete coalitions are exactly the maximal cliques. We focus on the case of the empty coalition, and notice that

Jac (\emptyset)

consists of the universal vertices, i.e., those adjacent to every other vertex. In

ZFC

, by the corresponding instance of (12), the universal vertices constitute the intersection of all maximal cliques:

\begin{matrix} (13) & ⋂ Comp = {a \in V ∣ (\forall b \in V) (a \neq b \to {a, b} \in E)} . \end{matrix}

This helps to find a maximal clique with AC.12

¹²

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

In fact, if V itself fails to be a clique, as witnessed by non-adjacent distinct vertices

a, b \in V

, then by contraposition (13) yields a maximal clique that avoids a.

6.2.2. Maximal chains

These are special cases of maximal cliques. In fact, to see how Hausdorff’s Maximal Chain Principle fits into the above setting, suppose that $(S, ⩽)$ is a partially ordered set. We consider the comparability graph $G = (V, E)$ , i.e., the elements of S serve as nodes, and we define adjacency as comparability with respect to ⩽, $\begin{matrix} V = S and E = {{a, b} ∣ a ⩽ b \lor b ⩽ a} . \end{matrix}$ Thus, the cliques of G are nothing but the ⩽-chains, among which the maximal ones are precisely the complete coalitions. In ZFC the corresponding instance of (13) then says that $a \in S$ belongs to all maximal chains if and only if a is comparable with every $b \in S$ : $\begin{matrix} (14) & ⋂ Comp = {a \in S ∣ (\forall b \in S) (a ⩽ b \lor b ⩽ a)} . \end{matrix}$ This is a ZF -equivalent of Hausdorff’s Maximal Chain Principle [26], and the argument is similar to the case of cliques: If S is not totally ordered by ⩽, as witnessed by a certain element a of S incomparable to some $b \in S$ , then by contraposition (14) yields a maximal chain that avoids a. Notice how this does not crucially hinge on posets – towards a more general form of Hausdorff’s principle for directed graphs, along with the corresponding radical and intersection theorem, the partial order above may be replaced by an arbitrary binary relation.13

¹³
For instance, Suppes hints at forms of maximal principles in terms of arbitrary relations [64, Chapter 8].

On the lines of Table 1, we recapitulate the latter two applications in Table 2. We now have captured, with increasing generality, chains by cliques,14

¹⁴

Conversely, in order to obtain a maximal clique it suffices to have a maximal chain of cliques.

cliques by coalitions for irreflexive symmetric relations [59], and the latter by inconsistency predicates.

Table 2

Correspondences for cliques and chains

	Maximal Clique Principle (Section 6.2.1)	Hausdorff’s Maximal Chain Principle (Section 6.2.2)
given structure	undirected graph	partially ordered set
irreflexive, symmetric relation R	nonadjacency	incomparability
coalition	clique	chain
complete coalition	maximal clique	maximal chain
elements of $Jac (\emptyset)$	universal vertices	elements comparable to all other

7. Binary trees

In this section we carry over to complete coalitions the avenue recently followed [60] for prime ideals of consequence relations towards a constructive universal form of Krull’s Prime Ideal Theorem.15

¹⁵
For a related but different approach see [48,49].

Readers familiar with dynamical algebra [18,37,68] will draw a connection between the tree methods of [18] and the one employed here.

Let again S be a set. For every $a \in S$ we first introduce a corresponding letter $X_{a}$ . For the set of finite sequences of elements of S and such letters we write $\begin{matrix} S = {(S \cup {X_{a} ∣ a \in S})}^{*} \end{matrix}$ with the usual provisos on notation, concatenation, etc.

Definition 5.

We generate inductively a class $T$ of finite rooted binary trees $T \subseteq S$ by the following rules: $\begin{matrix} (15) & {[]} \in T (root) T \in T u \in Leaf (T) a \in S T \cup {u a, u X_{a}} \in T (branch) \end{matrix}$

As usual, by a leaf we understand a sequence $u \in T$ without immediate successor in T. The second rule is to say that, given $T \in 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 $u a$ and $u X_{a}$ . Here is a possible instance, where $a, b \in S$ :

As an auxiliary tool, we further need a sorting function $sort : S \to 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 a simple manner, as follows: $\begin{matrix} sort ([]) = [], sort (u a) = a sort (u), sort (u X_{a}) = sort (u) X_{a} . \end{matrix}$ Last but not least, given a subset C of S, owe introduce a relation $⊩_{C}$ between elements of S and sorted finite sequences in $S$ by defining $\begin{matrix} c ⊩_{C} [a_{1}, \dots, a_{k}, X_{b_{1}}, \dots, X_{b_{ℓ}}] \equiv (\forall V_{1} \in R_{b_{1}}) \dots (\forall V_{ℓ} \in R_{b_{ℓ}}) c ⊲ C, a_{1}, \dots, a_{k}, V_{1}, \dots, V_{ℓ} . \end{matrix}$ where we drop the quantifier in case of $ℓ = 0$ . In particular, $\begin{matrix} (16) & c ⊩_{C} [] \Leftrightarrow c \in Jac (C) . \end{matrix}$ Keeping in mind Theorem 2, with AC the semantics of this relation is that for u as above, $c ⊩_{C} u$ precisely when, for every simultaneous instantiation of respective opponents $V_{1}, \dots, V_{ℓ}$ of $b_{1}, \dots, b_{ℓ}$ , this c is a member of every complete coalition over C that further contains $a_{1}, \dots, a_{k}$ and $V_{1}, \dots, V_{ℓ}$ . The case in which this holds with respect to every leaf of a certain tree $T \in T$ will later be of particular interest.

Lemma 4.

Let $a, c \in S$ and let $u \in S$ be sorted. If $c ⊩_{C} a u$ and $c ⊩_{C} u X_{a}$ , then $c ⊩_{C} u$ .

Proof.

Consider $u = [a_{1}, \dots, a_{k}, X_{b_{1}}, \dots, X_{b_{ℓ}}]$ and suppose that (i) $c ⊩_{C} a u$ and (ii) $c ⊩_{C} u X_{a}$ . To show that $c ⊩_{C} u$ , let $V_{1} \in R_{b_{1}}, \dots, V_{ℓ} \in R_{b_{ℓ}}$ . We write $C^{'} = C, a_{1}, \dots, a_{k}, V_{1}, \dots, V_{ℓ}$ and need to check that $c ⊲ C^{'}$ . Now, premise (i) yields $c ⊲ C^{'}, a$ , while (ii) implies that $c ⊲ C^{'}, V$ for every $V \in R_{a}$ , so $(C)$ implies $c ⊲ C^{'}$ . □

Definition 6.

Let $C \subseteq S$ and $c \in S$ . A tree $T \in 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 an opponent $V \in R_{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 the completeness clause $(C)$ , to capture termination by way of the Jacobson radical, and thus to resolve indeterminacy in the spirit of [60].

The following is the constructive counterpart of Theorem 2 and does not require that C be a coalition.

Theorem 3.

Let $c \in S$ and $C \subseteq S$ . The following are equivalent.

$c \in Jac (C)$ .

There is $T \in T$ which terminates for C in c.

Proof.

If $c \in Jac (C)$ , then $c ⊩_{C} []$ by (16), which is to say that ${[]}$ terminates for C in c. Conversely, suppose that $T \in T$ is such that $c ⊩_{C} sort (u)$ for every leaf u of T. We argue by induction on T to show that $c \in Jac (C)$ . The case $T = {[]}$ is trivial (16). 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 (u a) = a sort (u)$ as well as $c ⊩_{C} sort (u X_{a}) = sort (u) X_{a}$ for a certain $a \in S$ . Lemma 4 implies that $c ⊩_{C} sort (u)$ , whence we reduce to $T^{'}$ , to which the induction hypothesis applies. □

Membership in a radical coalition is thus tantamount to termination. Remark 3.

Very much in the spirit of dynamical algebra [18,37,62,67,68], every tree $T \in 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 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 for $R (C_{m})$ . 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 Jac (C) \subseteq Jac (C_{m}) = C_{m}$ by Theorem 3 and the fact that every complete coalition is radical.

8. Conclusion

Hausdorff’s Maximal Chain Principle, a forerunner of the Kuratowski–Zorn Lemma [12,35,70], is presumably one of the best 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 criterion for completeness, reminiscent of the case in commutative ring theory for maximal ideals. By analogy with Krull’s Theorem for maximal ideals, and employing a suitable adaptation of the Jacobson radical, we could phrase a versatile generalisation of Hausdorff’s principle as an intersection principle. This has paved the way to a constructive, purely syntactical rereading, both by an inductively generated covering relation, as well as by means of finite binary trees which encode computations along generic complete objects. Concrete applications can be found in algebra (see, e.g., our recasting of a part of McCabe’s proof of Zariski’s Lemma in Section 6.1.1 above); it remains to be seen to what extent our method allows to bypass other maximality principles.

Footnotes

Acknowledgements

The present study was carried out within the project “A New Dawn of Intuitionism: Mathematical and Philosophical Advances” (ID 60842) funded by the John Templeton Foundation, the project “Reducing complexity in algebra, logic, combinatorics – REDCOM” belonging to the programme “Ricerca Scientifica di Eccellenza 2018” of the Fondazione Cariverona, and the Gruppo Nazionale per le Strutture Algebriche, Geometriche e le loro Applicazioni (GNSAGA) of the Italian Istituto Nazionale di Alta Matematica (INdAM).16

¹⁶

The opinions expressed in this paper are solely those of the authors.

The anonymous referees’ helpful remarks on both the conference paper [59] as well as the present journal version are gratefully acknowledged, and the authors wish to thank the organizers of CiE 2020 for the opportunity to present a forerunner of this work. The revised version of this article profited from both authors’ participation at the Dagstuhl Seminar 21472 “Geometric Logic, Constructivisation, and Automated Theorem Proving” in November 2021. Giuseppe Mazzuoccolo was so kind as to help out with up-to-date graph-theoretic terminology. Last but not least, this paper would not have been possible without Giulio Fellin’s path-paving work about the Jacobson radical in logic [20,

], and the related discussions at a distance.

References

Aczel, Aspects of general topology in constructive set theory, Ann. Pure Appl. Logic 137(1–3) (2006), 3–29. doi:10.1016/j.apal.2005.05.016.

Aczel,

Crosilla,

Ishihara,

Palmgren and

Schuster, Binary refinement implies discrete exponentiation, Studia Logica 84(3) (2006), 361–368. doi:10.1007/s11225-006-9014-9.

Aczel and

Rathjen, Notes on constructive set theory, Technical report, Institut Mittag–Leffler, 2000, Report No. 40.

Aczel and

Rathjen, Constructive set theory, 2010, Book draft, https://www1.maths.leeds.ac.uk/~rathjen/book.pdf.

Banaschewski, A new proof that “Krull implies Zorn”, Math. Log. Quart. 40 (1994), 478–480. doi:10.1002/malq.19940400405.

J.L.

Bell, Some new intuitionistic equivalents of Zorn’s lemma, Arch. Math. Logic 42(8) (2003), 811–814. doi:10.1007/s00153-003-0191-1.

Berger, A computational interpretation of open induction, in: Proceedings of the Ninetenth Annual IEEE Symposium on Logic in Computer Science,

Titsworth, ed., IEEE Computer Society, 2004, pp. 326–334.

Bishop, Foundations of Constructive Analysis, McGraw-Hill, New York, 1967.

Bishop and

Bridges, Constructive Analysis, Springer, 1985. doi:10.1007/978-3-642-61667-9.

10.

Blechschmidt and

Schuster, Maximal ideals in countable rings, constructively, in Revolutions and Revelations in Comutability. 18th Conference on Computability in Europe,

Berger and

Franklin, eds, Lect. Notes Comput. Sci., Springer, 2022, forthcoming.

11.

J.A.

Bondy and

U.S.R.

Murty, Graph Theory, Graduate Texts in Mathematics, Vol. 244, Springer-Verlag, London, 2008. doi:10.1007/978-1-84628-970-5.

12.

P.J.

Campbell, The origin of “Zorn’s lemma”, Historia Math. 5 (1978), 77–89. doi:10.1016/0315-0860(78)90136-2.

13.

Ciraulo,

M.E.

Maietti and

Sambin, Convergence in formal topology: A unifying notion, J. Log. Anal. 5(2) (2013), 1–45. doi:10.4115/jla.2013.5.2.

14.

Ciraulo,

Rinaldi and

Schuster, Lindenbaum’s lemma via open induction, in: Advances in Proof Theory,

Kahle,

Strahm and

Studer, eds, Progress in Computer Science and Applied Logic, Vol. 28, Springer International Publishing Switzerland, Cham, 2016, pp. 65–77. doi:10.1007/978-3-319-29198-7_3.

15.

Coquand, A note on the open induction principle, Technical report, Göteborg University, 1997, www.cse.chalmers.se/~coquand/open.ps .

16.

Coquand,

Lombardi and

Quitté, Dimension de Heitmann des treillis distributifs et des anneaux commutatifs, Publications Mathématiques de Besançon. Algèbre et Théorie des Nombres (2006), 57–100.

17.

Coquand,

Sambin,

Smith and

Valentini, Inductively generated formal topologies, Ann. Pure Appl. Logic 124 (2003), 71–106. doi:10.1016/S0168-0072(03)00052-6.

18.

Coste,

Lombardi and

M.-F.

Roy, Dynamical method in algebra: Effective Nullstellensätze, Ann. Pure Appl. Logic 111(3) (2001), 203–256. doi:10.1016/S0168-0072(01)00026-4.

19.

Espíndola, A short proof of Glivenko theorems for intermediate predicate logics, Archive for Mathematical Logic 52(7–8) (2013), 823–826. doi:10.1007/s00153-013-0346-7.

20.

Fellin, The Jacobson radical: From algebra to logic, 2018, Master’s thesis. Università di Verona, Dipartimento di Informatica.

21.

Fellin and

Schuster, A general Glivenko–Gödel theorem for nuclei, in: Proceedings of the 37th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2021, Salzburg, Austria, August 29–September 3, 2021,

Sokolova, ed., Electronic Notes in Theoretical Computer Science, Elsevier, 2021.

22.

Fellin,

Schuster and

Wessel, The Jacobson radical of a propositional theory, Bull. Symbolic Logic (2021), forthcoming.

23.

Galatos and

Ono, Glivenko theorems for substructural logics over FL, J. Symbolic Logic 71(4) (2006), 1353–1384. doi:10.2178/jsl/1164060460.

24.

Glivenko, Sur quelques points de la Logique de M. Brouwer, Acad. Roy. Belg. Bull. Cl. Sci. (5) 15 (1929), 183–188.

25.

Guerrieri and

Naibo, Postponement of

raa

and Glivenko’s theorem, revisited, Studia Logica 107(1) (2019), 109–144. doi:10.1007/s11225-017-9781-5.

26.

Hausdorff, Grundzüge der Mengenlehre, Verlag von Veit & Comp., Leipzig, 1914.

27.

Haykazyan, More on a curious nucleus, J. Pure Appl. Algebra 224 (2020), 860–868. doi:10.1016/j.jpaa.2019.06.014.

28.

Hodges, Krull implies Zorn, J. Lond. Math. Soc. 19 (1979), 285–287. doi:10.1112/jlms/s2-19.2.285.

29.

Howard and

Rubin, Consequences of the Axiom of Choice, American Mathematical Society, Providence, RI, 1998. doi:10.1090/surv/059.

30.

Ishihara, Classical propositional logic and decidability of variables in intuitionistic propositional logic, Log. Methods Comput. Sci. 10(3) (2014), 3:1, 7. doi:10.2168/LMCS-10(3:1)2014.

31.

Ishihara and

Schwichtenberg, Embedding classical in minimal implicational logic, MLQ Math. Log. Q. 62(1–2) (2016), 94–101. doi:10.1002/malq.201400099.

32.

Jacobson, The radical and semi-simplicity for arbitrary rings, Amer. J. Math. 67(2) (1945), 300–320. doi:10.2307/2371731.

33.

Kertész, Einführung in die transfinite Algebra, Birkhäuser Verlag, Basel, 1975, Elemente der Mathematik vom höheren Standpunkt aus, Band VII. doi:10.1007/978-3-0348-7673-5.

34.

Krull, Idealtheorie in Ringen ohne Endlichkeitsbedingung, Math. Ann. 101 (1929), 729–744. doi:10.1007/BF01454872.

35.

Kuratowski, Une méthode d’élimination des nombres transfinis des raisonnements mathématiques, Fundamenta Math. 3 (1922), 76–108. doi:10.4064/fm-3-1-76-108.

36.

Litak,

Polzer and

Rabenstein, Negative translations and normal modality, in: 2nd International Conference on Formal Structures for Computation and Deduction, LIPIcs. Leibniz Int. Proc. Inform., Vol. 84, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2017, Art. No. 27, 18.

37.

Lombardi and

Quitté, Commutative Algebra: Constructive Methods. Finite Projective Modules, Algebra and Applications, Vol. 20, Springer Netherlands, Dordrecht, 2015. doi:10.1007/978-94-017-9944-7.

38.

McCabe, A note on Zariski’s lemma, Amer. Math. Monthly 83(7) (1976), 560–561. doi:10.1080/00029890.1976.11994170.

39.

Mines,

Richman and

Ruitenburg, A Course in Constructive Algebra, Springer, New York, 1988, Universitext. doi:10.1007/978-1-4419-8640-5.

40.

C.J.

Mulvey, The maximality of filters, J. Pure Appl. Algebra 68 (1990), 253–258. doi:10.1016/0022-4049(90)90148-B.

41.

Negri, Glivenko sequent classes in the light of structural proof theory, Archive for Mathematical Logic 55(3–4) (2016), 461–473. doi:10.1007/s00153-016-0474-y.

42.

Negri and

von Plato, Structural Proof Theory, Cambridge University Press, Cambridge, 2001. doi:10.1017/CBO9780511527340.

43.

Negri and

von Plato, Proof Analysis. A Contribution to Hilbert’s Last Problem, Cambridge University Press, Cambridge, 2011. doi:10.1017/CBO9781139003513.

44.

Negri and

von Plato, Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen’s altitude line construction, in: Concepts of Proof in Mathematics, Philosophy, and Computer Science,

Probst and

Schuster, eds, Ontos Mathematical Logic, Vol. 6, Walter de Gruyter, Berlin, 2016, pp. 269–290. doi:10.1515/9781501502620-016.

45.

Ono, Glivenko theorems revisited, Ann. Pure Appl. Logic 161(2) (2009), 246–250. doi:10.1016/j.apal.2009.05.006.

46.

L.C.

Pereira and

E.H.

Haeusler, On constructive fragments of classical logic, in: Dag Prawitz on Proofs and Meaning, Outst. Contrib. Log., Vol. 7, Springer, Cham, 2015, pp. 281–292.

47.

Powell, On the computational content of Zorn’s lemma, in: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’20, Association for Computing Machinery, New York, NY, USA, 2020, pp. 768–781.

48.

Powell,

Schuster and

Wiesnet, An algorithmic approach to the existence of ideal objects in commutative algebra, in: 26th Workshop on Logic, Language, Information and Computation (WoLLIC 2019), Utrecht, Netherlands, 2–5 July 2019, Proceedings,

Iemhoff and

Moortgat, eds, Lect. Notes Comput. Sci., Vol. 11541, Springer, Berlin, 2019, pp. 533–549.

49.

Powell,

Schuster and

Wiesnet, A universal algorithm for Krull’s theorem, Inform. and Comput. (2021), In press. Paper 104761, available online 5 May 2021.

50.

J.-C.

Raoult, Proving open properties by induction, Inform. Process. Lett. 29(1) (1988), 19–23. doi:10.1016/0020-0190(88)90126-3.

51.

Rathjen, Generalized inductive definitions in constructive set theory, in: From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics,

Crosilla and

Schuster, eds, Oxford Logic Guides, Vol. 48, Clarendon Press, Oxford, 2005, Chapter 16.

52.

Rinaldi and

Schuster, A universal Krull–Lindenbaum theorem, J. Pure Appl. Algebra 220 (2016), 3207–3232. doi:10.1016/j.jpaa.2016.02.011.

53.

Rinaldi,

Schuster and

Wessel, Eliminating disjunctions by disjunction elimination, Bull. Symb. Logic 23(2) (2017), 181–200. doi:10.1017/bsl.2017.13.

54.

Rinaldi,

Schuster and

Wessel, Eliminating disjunctions by disjunction elimination, Indag. Math. (N.S.) 29(1) (2018), 226–259. doi:10.1016/j.indag.2017.09.011.

55.

Sambin, Some points in formal topology, Theoret. Comput. Sci. 305(1–3) (2003), 347–408. doi:10.1016/S0304-3975(02)00704-1.

56.

Schuster, Induction in algebra: A first case study, in: 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE Computer Society Publications, 2012, pp. 581–585, Proceedings, LICS 2012, Dubrovnik, Croatia. doi:10.1109/LICS.2012.68.

57.

Schuster, Induction in algebra: A first case study, Log. Methods Comput. Sci. 9(3) (2013), 20. doi:10.2168/LMCS-9(3:20)2013.

58.

Schuster and

Wessel, A general extension theorem for directed-complete partial orders, Rep. Math. Logic 53 (2018), 79–96.

59.

Schuster and

Wessel, The computational significance of Hausdorff’s maximal chain principle, in: Beyond the Horizon of Computability. 16th Conference on Computability in Europe,

Anselmo,

G.d.

Vedova,

Manea and

Pauly, eds, Lect. Notes Comput. Sci., Vol. 12098, Springer, 2020, pp. 239–250. doi:10.1007/978-3-030-51466-2_21.

60.

Schuster and

Wessel, 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 ’20, Association for Computing Machinery, New York, NY, USA, 2020, pp. 820–830.

61.

Schuster and

Wessel, Syntax for semantics: Krull’s maximal ideal theorem, in: Paul Lorenzen: Mathematician and Logician,

Heinzmann and

Wolters, eds, Log. Epistemol. Unity Sci., Vol. 51, Springer, Cham, 2021, pp. 77–102. doi:10.1007/978-3-030-65824-3_6.

62.

Schuster,

Wessel and

Yengui, Dynamic evaluation of integrity and the computational content of Krull’s lemma, J. Pure Appl. Algebra 226(1) (2022), paper 106794, available online 17 May 2021.

63.

Simmons, A curious nucleus, J. Pure Appl. Algebra 214 (2010), 2063–2073. doi:10.1016/j.jpaa.2010.02.011.

64.

Suppes, Axiomatic Set Theory, Dover Publications, New York, 1972.

65.

Wiesnet, An algorithmic version of Zariski’s lemma, in: Connecting with Computability. 17th Conference on Computability in Europe, CiE 2021 Virtual Event, Ghent, July 5–9, 2021, Proceedings,

De Mol,

Weiermann,

Manea and

Fernández-Duque, eds, Lecture Notes in Computer Science, Vol. 12813, Springer, 2021, pp. 469–482.

66.

Wiesnet, The computational content of abstract algebra and analysis, PhD thesis, Ludwig-Maximilians Universtät München, Università degli Studi di Trento, Università degli Studi di Verona, 2021.

67.

Yengui, Making the use of maximal ideals constructive, Theoret. Comput. Sci. 392 (2008), 174–178. doi:10.1016/j.tcs.2007.10.011.

68.

Yengui, Constructive Commutative Algebra. Projective Modules over Polynomial Rings and Dynamical Gröbner Bases, Lecture Notes in Mathematics, Vol. 2138, Springer, Cham, 2015.

69.

H.P.

Young and

Zamir (eds), Handbook of Game Theory, Volume 4, 1st edn, Handbooks in Economics, North-Holland, Amsterdam, 2015.

70.

Zorn, A remark on method in transfinite algebra, Bull. Amer. Math. Soc. 41 (1935), 667–670. doi:10.1090/S0002-9904-1935-06166-X.

The Jacobson radical for an inconsistency predicate

Abstract

Keywords

1. Introduction

1 Maximality criteria, though to a different end, have also been put under constructive scrutiny in the context of Boolean algebras and locales by Mulvey [40]. One of the anonymous referees kindly brought this to our attention.

1.2. On method and foundations

4 Since for Theorem 2 we switch to ZFC anyway, we do not refer to forms of OI (say, for set-generated directed-complete poclasses [1]) more pertinent to CZF . See, e.g., [58].

6.1. Ideals and theories

6 There is no need to suppose the ideal J to be proper: in ZFC one can tell whether J = S , in which case the claim holds trivially.

Proposition 3 ( ZF ).

10 In [59, Remark 2] we have discussed in terms of coalitions Bell’s related notion of cliques for binary relations [6].

11 In other words, the induced subgraph is complete in the sense of graph theory.

13 For instance, Suppes hints at forms of maximal principles in terms of arbitrary relations [64, Chapter 8].

15 For a related but different approach see [48,49].

Footnotes

Acknowledgements

References

¹
Maximality criteria, though to a different end, have also been put under constructive scrutiny in the context of Boolean algebras and locales by Mulvey [40]. One of the anonymous referees kindly brought this to our attention.

⁴
Since for Theorem 2 we switch to ZFC anyway, we do not refer to forms of OI (say, for set-generated directed-complete poclasses [1]) more pertinent to CZF . See, e.g., [58].

⁶
There is no need to suppose the ideal J to be proper: in ZFC one can tell whether $J = S$ , in which case the claim holds trivially.

¹⁰
In [59, Remark 2] we have discussed in terms of coalitions Bell’s related notion of cliques for binary relations [6].

¹¹
In other words, the induced subgraph is complete in the sense of graph theory.

¹³
For instance, Suppes hints at forms of maximal principles in terms of arbitrary relations [64, Chapter 8].

¹⁵
For a related but different approach see [48,49].