Reifying dynamical algebra: Maximal ideals in countable rings,constructively

Abstract

The existence of a maximal ideal in a general nontrivial commutative ring is tied together with the axiom of choice. Following Berardi, Valentini and thus Krivine but using the relative interpretation of negation (that is, as “implies $0 = 1$ ”) we show, in constructive set theory with minimal logic, how for countable rings one can do without any kind of choice and without the usual decidability assumption that the ring is strongly discrete (membership in finitely generated ideals is decidable). By a functional recursive definition we obtain a maximal ideal in the sense that the quotient ring is a residue field (every noninvertible element is zero), and with strong discreteness even a geometric field (every element is either invertible or else zero). Krull’s lemma for the related notion of prime ideal follows by passing to rings of fractions. By employing a construction variant of set-theoretic forcing due to Joyal and Tierney, we expand our treatment to arbitrary rings and establish a connection with dynamical algebra: We recover the dynamical approach to maximal ideals as a parametrized version of the celebrated double negation translation. This connection allows us to give formal a priori criteria elucidating the scope of the dynamical method. Along the way we do a case study for proofs in algebra with minimal logic, and generalize the construction to arbitrary inconsistency predicates. A partial Agda formalization is available at an accompanying repository.1

See https://github.com/iblech/constructive-maximal-ideals/. This text is a revised and extended version of the conference paper (In Revolutions and Revelations in Computability. 18th Conference on Computability in Europe (2022) Springer). The conference paper only briefly sketched the connection with dynamical algebra; did not compare this connection with other flavors of set-theoretic forcing; and sticked to the case of commutative algebra only, passing on the generalization to inconsistency predicates and well-orders.

Keywords

Maximal ideals set-theoretic forcing constructive commutative algebra dynamical algebra

Let A be a commutative ring with unit. The standard way of constructing a maximal ideal of A is to apply Zorn’s lemma to the set of proper ideals of A; but this method is less an actual construction and more an appeal to the transfinite.

If A is countable with enumeration $x_{0}, x_{1}, \dots$ , we can hope to provide a more explicit construction by successively adding generators to the zero ideal, skipping those which would render it improper: $\begin{matrix} (⋆) & \begin{aligned} m_{0} = {0}, \\ m_{n + 1} = \{\begin{array}{ll} m_{n} + (x_{n}), & if 1 \notin m_{n} + (x_{n}), \\ m_{n}, & else. \end{array} \end{aligned} \end{matrix}$ A maximal ideal is then obtained in the limit as the union of the intermediate stages $m_{n}$ . For instance, Krull in his 1929 Annalen contribution [78, Hilfssatz] and books on constructive algebra [84, Lemma VI.3.2], [80, comment after Theorem VII.5.2] proceed in this fashion. A similar construction concocts Henkin models for the purpose of proving Gödel’s completeness theorem for countable languages, successively adding formulas which do not render the current set inconsistent [138, Satz I.56], [141, Lemma 1.5.7], [133, Lemma III.5.4], [67, Lemma 2.1], [39, Section A.4].

This procedure avoids all forms of choice by virtue of being a functional recursive definition, but still requires some form of omniscience in order to carry out the case distinction. In Section 1 we study a variant of this construction, due to Berardi and Valentini [19], which avoids non-constructive principles and decidability assumptions, similar to a construction which has been studied by Krivine [77, p. 410] and later Herbelin and Ilik [63, p. 11] in the context of Gödel’s completeness theorem.

In this generality, the resulting maximal ideal has an elusive quality to it, but useful properties and positive information can still be extracted. We recover the original construction under certain decidability assumptions (Proposition 1.8). To further elucidate the essential aspects of the construction, Section 5 contains a streamlined account in the setting of abstract inconsistency predicates.

0.1. Extraction of computational content

We illustrate the scope of applications of the maximal ideal construction of Section 1 by exploring, in Section 2, several established test cases for Hilbert’s program in commutative algebra. Among them is the following (Proposition 2.6):

Proposition.
Let A be a ring. Let $M \in A^{n \times m}$ be a matrix with more rows than columns. Assume that the induced linear map $A^{m} \to A^{n}$ is surjective. Then $1 = 0$ in A.
Proof.
Assume for the sake of a contradiction that $1 \neq 0$ in A. Then, by the axiom of choice, there exists a maximal ideal $m$ . The quotient ring $k : = A / m$ is a field and the induced linear map $k^{m} \to k^{n}$ is still surjective. Hence we have a contradiction to basic linear algebra over fields. □
This proof is short, elegant, a prototypical examplar of a common reduction technique in commutative algebra – and wholly unconstructive. Is there also a direct computational argument?

Since the statement of the proposition is, for fixed matrix dimensions, a coherent sequent (in the language of rings), the completeness theorem for coherent logic [74, Corollary D1.5.10] implies a priori that there exists a proof in coherent logic, hence in particular a constructive proof. The completeness theorem, however, rests on the Boolean prime ideal theorem, a version of the axiom of choice [74, Remark D1.5.11], [7,62,130]. Do we actually know a direct computational argument?

Yes (for brevity, case $n = 2$ , $m = 1$ only – see [108] for a general proof): Write $M = (\binom{x}{y})$ . By surjectivity, there are ring elements u, v with $u (\binom{x}{y}) = (\binom{1}{0})$ and $v (\binom{x}{y}) = (\binom{0}{1})$ . Hence $1 = (v y) (u x) = (u y) (v x) = 0$ .

The challenge in mathematical logic is to extract a direct computational argument from the given classical proof, and for this particular example there are several techniques which meet this challenge. Section 2 shows that also the explicit maximal ideal construction of Section 1 can be used to this end – assuming that the ring is countable.
0.2. Extension to the uncountable case

What if the ring A is not countable, or if it is countable but an enumeration $N ↠ A$ is expensive to evaluate?

In absence of the axiom of choice, some restriction on the rings is required, as it is well-known that the statement that any nontrivial ring has a maximal ideal implies (over Zermelo–Fraenkel set theory zf) the axiom of choice [8,46,64,65,130]. However, this limitation only pertains to the abstract existence of maximal ideals, not to concrete consequences of their existence. Mathematical logic teaches us by way of diverse examples to not conflate these two concerns.

For instance, although zf does not prove the axiom of choice, it does prove every theorem of zfc pertaining only to natural numbers (by interpreting a given zfc-proof in the constructible universe L and exploiting that the natural numbers are absolute between V and L [56,120]); similarly, although intuitionistic Zermelo–Fraenkel set theory izf does not prove the law of excluded middle, it does prove every $Π_{2}^{0}$ -theorem of zf (by the double negation translation combined with Friedman’s continuation trick [51]).

A similar phenomenon concerns countability. Set theory teaches us that whether a given set is countable depends not only on the set itself, but is more aptly regarded as a property of the ambient universe [60]: Given any set M, there is a forcing extension [53,54,87,147] of the universe in which M becomes countable.2

²
An analogous situation in commutative algebra is the following. Whether a ring element x is invertible not only depends on the element itself, but is more aptly regarded as a property of the ring A it is an element of. Any element x can become invertible by passing from the base ring A to the localization $A [x^{- 1}]$ .

The process of traveling to this extension is called Lévy collapse [69, Section I.6], [18, Chapter 5]. Set theorists have used this technique and other forcing models with great success, mostly in order to explore the range of set-theoretic possibility. However, they can also be used as tools to deduce results about the base universe.

More precisely, to apply the iterative step-by-step construction of a maximal ideal to a ring A which might not be countable in a constructive setting, we employ a constructive variant of Lévy collapse due to Joyal and Tierney [75, pp. 36f.]: Given a ring A, there is an extension of the universe – a certain sheaf topos with a concrete computational interpretation – in which the ring A appears countable; this extended universe contains what is called the generic surjection from $N$ to A. We can then apply the iterative construction in this extended universe to obtain a maximal ideal of A there; from the point of view of the base universe, we will not actually have constructed an ideal of A but rather a “sheaf of ideals of the constant sheaf associated to A”.

Crucially, the passage to such an extension preserves and reflects bounded first-order statements, those first-order statements where all quantifiers range over sets of the base universe.3

This property is well-known for classical set-theoretic forcing, for the plain reason that the base model V is a transitive subset of the forcing extension $V [G]$ . Constructively, it is a property enjoyed only by some particular forcing notions. In topos-theoretic language, the canonical geometric morphism from any Grothendieck topos to the base topos is open if the base satisfies the law of excluded middle [75, p. 57], so every Grothendieck topos is overt. In contrast, overtness is a nontrivial property if the law of excluded middle is not available. We are grateful to Robert Lubarsky for pointing out this difference to classical forcing to us.

Hence we have the following metatheorem:

Countability assumptions from intuitionistic proofs of bounded first-order statements can always be mechanically eliminated.

To wit: If our aim is to verify some bounded first-order statement P about a perhaps uncountable ring A, such as the statement about surjective matrices above, we may just as well assume that A is countable, because it actually will be so in the extended universe and because every bounded first-order property which holds there will also hold for A in the base universe.

Crucially, the first-order restriction is only on the form of the statements, not on the form of the proofs. These may freely employ higher-order constructs. “First-order” statements are statements which only refer to elements, not to subsets. The statement “there is a maximal ideal” is a higher-order statement, hence we cannot eliminate countability assumptions from proofs of this statement; but we can eliminate countability assumptions from proofs of first-order consequences of the existence of a maximal ideal.

We present details of this technique in Section 4. Unlike Joyal and Tierney, who pursued a semantic approach employing the language of toposes, our presentation leans on the syntactical side and is explicitly computational in nature. Owing to the central role played by a certain generalized inductive definition, we connect forcing with established notions in theoretical computer science. No familiarity with categories, sheaves or toposes is required.

In classical set theory, the feature that forcing preserves and reflects bounded first-order formulas is sometimes regarded as a deficiency of the forcing technique, limiting us in the range of models of set theory we can construct. We turn this view upside down: This feature is the central property enabling the applications we desire. We hence bolster Judith Roitman’s thesis that “mainstream mathematics […] is beginning to see results using modern set theoretic techniques” [116] by providing an instance in constructive algebra, and hope to make forcing more accessible.

Summarizing, our approach strengthens the view of maximal ideals as convenient fictions [126, Section 1], in line with a famous motto of Poincaré [102]:

Never lose sight of the fact that every proposition concerning infinity must be the translation, the precise statement of propositions concerning the finite.

Maximal ideals can carry out their work by any of the following possibilities:

For countable (or well-founded) rings, no help is required. Section 1 presents an explicit construction of a maximal ideal.

For arbitrary rings, the existence of a maximal ideal follows from the axiom of choice.

Intuitionistic first-order consequences of the existence of a maximal ideal are true even if no actual maximal ideal can be constructed.

0.3. Connection with dynamical algebra

In Section 4.4 we turn to the general toolbox of dynamical algebra [43], [80, Section XV.6], [45,90,153]. Since its independent inventions by Dominique Duval and Paul Lorenzen, this toolbox has been widely successful in extracting computational content from classical proofs appealing to the transfinite, including proofs of prominent theorems such as Suslin’s lemma [136,152] or a theorem by Becher [16], a consequence of a theorem by Merkurjev.

The specific use case we are interested in concerns the wide class of classical commutative algebra proofs pursuing the following general outline:

Assume for the sake of contradiction that $1 \neq 0$ . Then, by the axiom of choice, there exists a maximal ideal $m$ . By (…computation and arguments…), we obtain that $1 \in m$ . This is a contradiction. Hence $1 = 0$ .

The aim is to extract from such a classical proof a direct computational argument that $1 = 0$ . To this end, the toolbox of dynamical algebra suggests a dynamical rereading of the given proof. Instead of appealing to the transfinite in order to concoct a completed maximal ideal $m$ , we make do with finitely generated approximations to a maximal ideal, starting out with the zero ideal $a = (0)$ and repeatedly refining this approximation over the course of the proof.

Classically, the fundamental property of a maximal ideal $m$ is that for every ring element x, either $x \in m$ or $1 \in m + (x)$ . When the given classical proof appeals to this property, we tentatively refine the current approximation from $a$ to $a + (x)$ , pretending that the first alternative holds, and resume the proof. When the proof reaches the conclusion $1 \in m$ , we have learnt the positive information that $1 \in a + (x)$ . Equipped with this information, we reset the current approximation back to $a$ and again follow the classical proof, now pretending that the second alternative holds. When the proof reaches the conclusion $1 \in m$ a second time, we have learnt that $1 \in a$ . In this way we fold up branches of the proof until, in the end, we obtain $1 \in (0)$ , so $1 = 0$ .

In good circumstances, this approach allows us to constructivize the given classical proof. However, from the point of view of a metamathematical analysis, several questions remain: What are the precise conditions on the given classical proof for this method to succeed? Which restriction on its means is required? Can we extend this method in case the desired conclusion is of a more general form than the simple identity $1 = 0$ ?

We answer these questions in Section 4.4 by connecting the dynamical method with the iterative construction of an actual maximal ideal of Section 1. More precisely:

The dynamical approach to maximal ideals is equivalent to

the iterative construction of a maximal ideal,

applied to the generic enumeration.

In this way we reify the dynamical approach to maximal ideals.

Conventions. Throughout this note, we fix a ring A, and work in a constructive metatheory. In the spirit of Lombardi and Quitté [80], we employ minimal logic [70], where by “not φ” we mean “ $φ \Rightarrow 1 =_{A} 0$ ”, and do not assume any form of the axiom of choice. Consequently, by “ $x \notin M$ ” we mean $x \in M \Rightarrow 1 =_{A} 0$ , and a subset $M \subseteq A$ is detachable if and only if for all $x \in A$ , either $x \in M$ or $x \notin M$ . For general background on constructive mathematics, we refer to [14,15,32].

For an arbitrary subset $M \subseteq A$ , not necessarily detachable, the ideal $(M)$ generated by M is given by ${\sum_{i = 1}^{n} a_{i} v_{i} | n ⩾ 0, a_{1}, \dots, a_{n} \in A, v_{1}, \dots, v_{n} \in M}$ . Notice that, for every element $v \in (M)$ , it holds that $v = 0$ or that M is inhabited, depending on whether $n = 0$ or $n > 0$ in $\sum_{i = 1}^{n} a_{i} v_{i}$ . This can also be seen from the alternative inductive generation of $(M)$ by the following rules: $\begin{matrix} \frac{v = 0}{v \in (M)} \frac{v \in M}{v \in (M)} \frac{v \in (M) w \in (M)}{v + w \in (M)} \frac{a \in A v \in (M)}{a v \in (M)} \end{matrix}$ Here we adhere to the paradigm of generalized inductive definitions [1,3,4,105].

Throughout the online version of this paper, the symbol “⊛” is a clickable link to the corresponding machine-checked statement. In several cases, the formalized version is slightly more general than the version in this text; conversely, in cases where we have felt that no additional insight is gained, the formalization only implements a special case.

1. An iterative construction of maximal ideals

We assume that the ring A is countable, with $x_{0}, x_{1}, \dots$ an enumeration of the elements of A. We do not assume that A is discrete (that is, that $x = y$ or $x \neq y$ for all elements of A) or that it is strongly discrete (that is, that finitely generated ideals of A are detachable). Up to Corollary 1.2(a) below we follow [19].

We study the following recursive construction of ideals $m_{0}, m_{1}, \dots$ of A (⊛): $\begin{aligned} m_{0} : = {0}, \\ m_{n + 1} : = m_{n} + ({x_{n} | 1 \notin m_{n} + (x_{n})}) . \end{aligned}$ Finally, we set $m : = ⋃_{n} m_{n}$ . The construction of $m_{n + 1}$ from $m_{n}$ is uniquely specified, requiring no choices of any form.

The set $M_{n} : = {x_{n} | 1 \notin m_{n} + (x_{n})}$ occurring in this construction contains the element $x_{n}$ if and only if $1 \notin m_{n} + (x_{n})$ ; it is obtained from the singleton set ${x_{n}}$ by bounded separation. This set $M_{n}$ is inhabited precisely if $1 \notin m_{n} + (x_{n})$ , in which case $m_{n + 1} = m_{n} + (x_{n})$ . However, in the generality we work in, we cannot assume that $M_{n}$ is empty or inhabited.

We can avoid the case distinction by the flexibility of nondetachable subsets, rendering it somewhat curious that – despite the conveyed flavor of a conjuring trick – the construction can still be used to obtain concrete positive results.

The ideal $(M_{n})$ is given by $(M_{n}) = {a x_{n} | (a = 0) \lor (1 \notin m_{n} + (x_{n}))}$ .

Lemma 1.1 (⊛).

The subset $m$ is an ideal.

The ideal $m$ is proper in the sense that $1 \notin m$ .

For every number $n \in N$ , the following are equivalent:

(1) $x_{n} \in m_{n + 1}$ . (2) $x_{n} \in m$ . (3) $1 \notin m + (x_{n})$ . (4) $1 \notin m_{n} + (x_{n})$ .

Proof.

Directed unions of ideals are ideals.

Assume $1 \in m$ . Then $1 \in m_{n}$ for some number $n ⩾ 0$ . We verify $1 = 0$ by induction over n. If $n = 0$ , then $1 \in m_{0} = {0}$ . Hence $1 = 0$ .

If $n > 0$ , then $1 = y + a x_{n - 1}$ for some elements $a, y \in A$ such that $y \in m_{n - 1}$ and such that $a = 0$ or $1 \notin m_{n - 1} + (x_{n - 1})$ . In the first case, we have $1 = y \in m_{n - 1}$ , hence $1 = 0$ by the induction hypothesis. In the second case we have $1 = 0$ by modus ponens applied to the implication $1 \notin m_{n - 1} + (x_{n - 1})$ and the fact $1 \in m_{n - 1} + (x_{n - 1})$ (which follows directly from the equation $1 = y + a x_{n - 1}$ ).

It is clear that $(3) \Rightarrow (4) \Rightarrow (1) \Rightarrow (2)$ . It remains to show that $(2) \Rightarrow (3)$ .

Assume $x_{n} \in m$ . In order to verify $1 \notin m + (x_{n})$ , assume $1 \in m + (x_{n})$ . Since $m + (x_{n}) \subseteq m$ , we have $1 \in m$ . Hence $1 = 0$ by properness of $m$ .
□
Corollary 1.2 (⊛).

The ideal $m$ is maximal in the sense that it is proper and that for all elements $x \in A$ , if $1 \notin m + (x)$ , then $x \in m$ .

The ideal $m$ is prime in the sense that it is proper and that for all elements $x, y \in A$ , if $x y \in m$ and $x \notin m$ , then $y \in m$ .

The ideal $m$ is radical in the sense that for every $k ⩾ 0$ , if $x^{k} \in m$ , then $x \in m$ .

Proof.

Immediate by Lemma 1.1(c).

This claim is true even for arbitrary maximal ideals: By maximality, it suffices to verify that $1 \notin m + (y)$ . If $1 \in m + (y)$ , then $x = x \cdot 1 \in (x) \cdot m + (x y) \subseteq m$ by $x y \in m$ , hence $x \in m$ , thus $1 = 0$ by $x \notin m$ .

Let $x^{k} \in m$ . Then $1 \notin m + (x)$ , for if $1 \in m + (x)$ , then also $1 = 1^{k} \in {(m + (x))}^{k} \subseteq m + (x^{k}) \subseteq m$ . Hence $x \in m$ by maximality.
□
Remark 1.3.
The ideal $m$ is double negation stable: for every ring element x, if $\neg \neg (x \in m)$ , then $x \in m$ . This is because by Lemma 1.1(c) membership of $m$ is a negative condition and $\neg \neg \neg φ \Rightarrow \neg φ$ is a tautology of minimal logic.

This first-order maximality condition of Corollary 1.2(a) is equivalent [19] to the following higher-order version: For every ideal $n$ such that $1 \notin n$ , if $m \subseteq n$ , then $m = n$ .

The quotient ring $A / m$ is a residue field in that $1 \neq 0$ and that every element which is not invertible is zero – as with the real or complex numbers in constructive mathematics.4
⁴
Residue fields have many of the basic properties of the fields from classical mathematics. For instance, minimal generating families of vector spaces over residue fields are linearly independent, finitely generated vector spaces do (up to $\neg \neg$ ) have a finite basis, monic polynomials possess splitting fields and Noether normalization is available (the proofs in [84] can be suitably adapted). The constructively rarer geometric fields – those kinds of fields for which every element is either invertible or zero – are required to ensure, for instance, that kernels of matrices are finite dimensional and that bilinear forms are diagonalizable.

Each of the latter is in fact a Heyting field, a residue field which also is a local ring: if a finite sum is invertible then one of the summands is. Example 1.4.
If we enumerate $Z$ by $0, 1, - 1, 2, - 2, \dots$ , the ideal $m$ coincides with the ideal $(2)$ . If the enumeration starts with a prime p, the ideal $m$ coincides with $(p)$ . More generally, if A is a countable Bézout ring and the enumeration starts with an irreducible element p, then $m$ coincides with $(p)$ .
Example 1.5.
Let $A = Z / a$ , where $a = ({6} \cup {2 | P} \cup {3 | Q})$ and P and Q are incompatible propositions, be enumerated by 0, 1, 5, 2, 3, 4. Then $m = {0} \cup {2 | \neg Q} \cup {4 | \neg Q} \cup {3 | \neg \neg Q \land \neg P}$ . It is instructive to check, with this description, that the maximality condition of Corollary 1.2(a) is satisfied. As is to be expected, the construction of $m$ neither discloses nor requires information about the status of P and Q. Even though A is a Bézout ring, the ideal $m$ can fail to be finitely generated and hence can fail to be a principal ideal.
Example 1.6.
If A is a local ring with group of units $A^{\times}$ , then $m = A ∖ A^{\times}$ .
Example 1.7.
We can also use an arbitrary ideal $a$ as $m_{0}$ instead of the zero ideal. All results in this section remain valid once “not φ” is redefined as “ $φ \Rightarrow 1 \in a$ ”; the resulting ideal $m$ is then a maximal ideal above $a$ ; it is proper in the sense that $1 \in m \Rightarrow 1 \in a$ , so “equiconsistent with $a$ ”.

The resulting ideal $m$ can also be obtained by applying the original version of the construction in the quotient ring $A / a$ (which is again countable) and taking the inverse image of the resulting ideal along the canonical projection $A \to A / a$ .

1.1. Recovering the original construction

If we can decide whether a finitely generated ideal contains the unit or not, we can improve on Corollary 1.2(a). For instance this is the case for strongly discrete rings such as the ring $Z$ , more generally for the ring of integers of every number field, and for polynomial rings over discrete fields [84, Theorem VIII.1.5].

Proposition 1.8.
Assume that for every finitely generated ideal $a \subseteq A$ we have $1 \notin a$ or $\neg (1 \notin a)$ . Then:
Each ideal $m_{n}$ is finitely generated.

The ideal $m$ is detachable.
If even $1 \in a$ or $1 \notin a$ for every finitely generated ideal $a \subseteq A$ , then:
The ideal $m$ is maximal in the strong sense that for every element $x \in A$ , $x \in m$ or $1 \in m + (x)$ , which is to say that the quotient ring $A / m$ is a geometric field (every element is zero or invertible).5
⁵
This notion of a maximal ideal, together with the corresponding one of a complete theory in propositional logic, has been generalized to the concept of a complete coalition [125,127] for an abstract inconsistency predicate.

Proof.
We verify claim (a) by induction over n. The case $n = 0$ is clear. Let $n > 0$ . By the induction hypothesis, the ideal $m_{n - 1}$ is finitely generated, hence so is $m_{n - 1} + (x_{n - 1})$ . By assumption, $1 \notin m_{n - 1} + (x_{n - 1})$ or $\neg (1 \notin m_{n - 1} + (x_{n - 1}))$ . In the first case $m_{n} = m_{n - 1} + (x_{n - 1})$ . In the second case $m_{n} = m_{n - 1}$ . In both cases the ideal $m_{n}$ is finitely generated.

To verify claim (b), let an element $x_{n} \in A$ be given. By assumption, $1 \notin m_{n} + (x_{n})$ or $\neg (1 \notin m_{n} + (x_{n}))$ . Hence $x_{n} \in m$ or $x_{n} \notin m$ by Lemma 1.1(c).

For claim (c), let an element $x_{n} \in A$ be given. If $1 \in m_{n} + (x_{n})$ , then also $1 \in m + (x_{n})$ . If $1 \notin m_{n} + (x_{n})$ , then $x_{n} \in m$ by Lemma 1.1(c). □

Remarkably, under the assumption of Proposition 1.8, the ideal $m$ is detachable even though in general it fails to be finitely generated. Usually in constructive mathematics, ideals which are not finitely generated are seldom detachable. For instance the ideal ${x \in Z | x = 0 \lor φ} \subseteq Z$ is detachable if and only if $φ \lor \neg φ$ .

A consequence of Proposition 1.8(a) is that the original procedure displayed as Equation (⋆) on page 263 is constructively feasible, and that it coincides with the construction of the maximal ideal $m$ .
1.2. A more economical description using generators

There is an equivalent description of the maximal ideal $m$ which uses sets $G_{n}$ of generators as proxies for the intermediate ideals $m_{n}$ (⊛): $\begin{aligned} G_{0} : = \emptyset \\ G_{n + 1} : = G_{n} \cup {x_{n} | 1 \notin (G_{n} \cup {x_{n}})} \end{aligned}$ An induction establishes the relation $(G_{n}) = m_{n}$ ; setting $G : = ⋃_{n \in N} G_{n}$ , there is the following analogue of Lemma 1.1(c).

Lemma 1.9 (⊛).

For every number $n \in N$ , the following are equivalent:

$x_{n} \in G_{n + 1}$ .

$x_{n} \in G$ .

$1 \notin (G) + (x_{n})$ .

$1 \notin (G_{n}) + (x_{n})$ .

In particular, not only do we have that $(G) = m$ , but G itself is already an ideal. This description of $m$ is in a sense more “economical” as the intermediate stages $G_{n}$ are smaller (not yet being ideals), enabling arithmetization in Section 3.

1.3. Generalization to the subcountable case

All results in Section 1 carry over mutatis mutandis if A is only assumed to be subcountable, that is, if we are only given a partially defined surjection $N ⇀ ⇀ A$ .

In this case, we are given an enumeration $x_{0}, x_{1}, \dots$ where some $x_{i}$ might not be defined; we then define $m_{n + 1} : = m_{n} + ({x_{n} | x_{n} is defined \land 1 \notin m_{n} + (x_{n})})$ .

The generalization to the subcountable case is particularly useful in the Russian tradition of constructive mathematics as exhibited by the effective topos [13,66,99,142], where many rings of interest are subcountable, including uncountable ones such as the real numbers [66, Prop. 7.2].

The generalization is also useful for localizations of rings at multiplicative subsets which might not be detachable, such as, in algebraic geometry, the structure sheaf of a spectrum. This sheaf is the localization of (the constant sheaf associated to) a given ring at its generic filter [25, Section 3.3].

1.4. Interaction with Noetherian hypotheses

In classical mathematics, a ring is Noetherian if and only if every infinite ascending sequence $\begin{matrix} a_{0} \subseteq a_{1} \subseteq a_{2} \subseteq \dots \end{matrix}$ of ideals stabilizes in that there is an index n such that $a_{n} = a_{n + 1} = \dots$ . In particular, the construction of a maximal ideal as the ascending union of the approximations $m_{n}$ already levels off at a finite stage. Constructively, we can reproduce a small fragment of this finiteness property.

More precisely, in constructive mathematics, the notion of Noetherian ring splinters into several inequivalent notions [36,41,68,84,94–96,109,129,132,139]. Common to most of them is that firstly they refer only to finitely generated ideals and that secondly stabilization is weakened to stalling: For instance, the Richman–Seidenberg condition [84, Section III.2] states that every infinite ascending chain $a_{0} \subseteq a_{1} \subseteq \dots$ of finitely generated ideals stalls in that there is an index n such that $a_{n} = a_{n + 1}$ . Related conditions allow for different kinds of collections of ideals, for instance trees [109], processes [22, Section 3.9] or sheaves of sequences [27,36,41]; but all of these keep the two restrictions, for without them not even the field with two elements would be provably Noetherian.

Since the approximations $m_{n}$ can fail to be finitely generated, these Noetherian conditions do not apply to the construction of a maximal ideal. However, even with a properness test as in Proposition 1.8 which ensures that they are, their effect of guaranteeing stalling is not of much use: In typical situations, it is common that $m_{n} = m_{n + 1}$ without $m_{n}$ coinciding with the limit $⋃_{k} m_{k}$ .

We could “speed up” the construction, skipping steps which do not add a new generator. It is somewhat remarkable that we can do so constructively, even without a properness test, by setting $\begin{aligned} m_{0}^{'} : = {0} \\ m_{n + 1}^{'} : = m_{n}^{'} + ({x_{k} | k \in I_{n} \land (\forall ℓ \in I_{n} . k ⩽ ℓ)}), \\ where I_{n} : = {k \in N | x_{k} \notin m_{n}^{'} \land 1 \notin m_{n}^{'} + (x_{k})} . \end{aligned}$ The modified sequence $m_{0}^{'} \subseteq m_{1}^{'} \subseteq \dots$ stalls only when it stabilizes. However, even with a properness test, by speeding up we lose finite generation of the approximations as we cannot determine whether $I_{n}$ is empty or inhabited. Hence the classical finiteness property is not reproduced in a strong sense.

For the peculiar anonymous Noetherian condition [22, Definition 3.27], postulating that every ideal is not not finitely generated, there is the following result; in the language of Veldman and Bezem, a “ghost from the lost classical paradise” [143, Section 5.1].

Proposition 1.10.
If the ring A is anonymously Noetherian, it is not not the case that there exists a number $n \in N$ such that $m = m_{n}$ .
Proof.
If the ideal $m$ is finitely generated, then clearly such a number n exists. The claim follows from the double contrapositive of this implication. □

The scope of Proposition 1.10 includes the structure sheaf of the spectrum of countable reduced rings [25, Proposition 34].

That said, for processly Noetherian rings, there is an alternative construction of a maximal ideal which sidesteps all of these issues and does not even require countability, if instead an oracle for maximality is available. Given a finitely generated ideal $a$ , such an oracle advises us whether there is a element $x \notin a$ such that the extension $a + (x)$ is still proper or whether all elements x such that $a + (x)$ is proper are already contained in $a$ . A maximal ideal can then be constructed by iteratively adding generators as suggested by the oracle, similar to the construction of minimal prime ideals above a given finitely generated ideal in the setting of Lasker–Noether rings [94, Theorem E].
1.5. An application: Construction of algebraic closures

Assume that A is a residue field. Let $f \in A [X]$ be a nonconstant monic polynomial. Since f is nonconstant monic, it is not invertible; thus Example 1.7 shows that there is a maximal ideal $m$ above $(f)$ . Hence $A [X] / m$ is a residue field in which f has a zero, namely the equivalence class of X.

Iterating this Kronecker construction, we obtain a splitting field of f. No assumption regarding decidability of reducibility has to be made, but in return the resulting field is only a residue field. Alternatively, a splitting residue field of f can be obtained in a single step as the quotient of the universal splitting algebra ([80, Section III.4], [101, Section 2.1], [110]) of f by a maximal ideal.

Using either of these constructions, we can obtain an algebraic closure of A: Let $f_{0}, f_{1}, \dots$ be an enumeration of all nonconstant monic polynomials over A; successively apply Kronecker or universal splitting algebra steps; and take the direct limit to obtain a residue field $K_{0}$ . Over this field, all the polynomials with coefficients in A split into linear factors; but $K_{0}$ acquires new polynomials which are not present over A. If g is a nonconstant monic polynomial over $K_{0}$ , it will not not have a zero in $K_{0}$ ,6

⁶
There is a splitting field $K_{0}^{'}$ of g over $K_{0}$ in which g has a zero α. Since the coefficients of g are all algebraic over A, by a standard lemma [84, Corollary VI.1.5] also α is a root of a nonconstant monic polynomial $f_{i}$ over A. This polynomial already splits into linear factors over $K_{0}$ , and if $K_{0}^{'}$ was an integral domain in that at least one factor of a vanishing product is already zero, one of these roots would coincide with α. Hence, by injectivity of the canonical map $K_{0} \to K_{0}^{'}$ , the polynomial g would already have a zero in $K_{0}$ . However, constructively, we cannot suppose the integral domain condition. Constructively it is only not not true that α is one of the zeros of $f_{i}$ . This issue is not visible in the account of Mines, Richman and Ruitenburg [84, Theorem VI.3.5], as they work over discrete fields, an assumption we do not make.

so classically

K_{0}

is the desired algebraic closure.

This closure construction, now fairly standard, is due to Gilmer [35,55,110]. Constructively however, it can fail that $K_{0}$ is algebraically closed. In this case the older approach from before Gilmer’s innovation can be applied: We repeat this construction with an enumeration of all nonconstant monic polynomials over $K_{0}$ , to obtain a field $K_{1}$ ; then $K_{2}$ ; and so on. The direct limit $K_{ω}$ of these fields is the desired algebraic closure – if g is a nonconstant monic polynomial over $K_{ω}$ , its coefficients will already be elements of some $K_{n}$ so that g will have a zero in $K_{n + 1}$ .

Using the technique reviewed in Section 4, the scope of this closure construction can be generalized from countable residue fields to arbitrary residue fields, delivering sheaf models of algebraic closures. This generalization is also useful in the case of countable residue fields, as it allows us to make do without potentially noncanonical enumerations of the field elements, thereby addressing a concern of Coquand [38, p. 37]. We leave a detailed comparison to the sheaf models of Mannaa and Coquand [83] as further work.

1.6. Computational content?

“Non-informative”, judged Berardi and Valentini who also studied the iterative maximal ideal construction [19, Section 4.2]. They continue: “Membership to [the maximal ideal] is a negated predicate. […] We proved no more than the maximal ideal M exists, and that we can use it in constructive reasoning. From the statement $x \in M$ we will get no witness.” Negativity is our Lemma 1.1(c). “A bad joke”, suggested another expert on constructive algebra.

Indeed, no computation at all is required for carrying out the iterative maximal ideal construction; the construction is purely formal and membership to the resulting ideal is in general not decidable. That said, we argue that there is still computational value in the construction.

Firstly, that realizers for statements “ $x \in m$ ” are non-informative is only true in case negation is defined as implication to ⊥, whereas we have defined as implication to $1 = 0$ . While ⊥ does not have any realizers at all, depending on the ring, the statement “ $1 = 0$ ” might well admit meaningful realizers. For instance, a ring of the form $B [f^{- 1}]$ is trivial if and only if f is nilpotent, and the ring $Z / (X)$ where X is the subsingleton set ${1 | φ} \subseteq Z$ associated to a truth value φ is trivial if and only if φ holds.

Secondly and more fundamentally, there is computational value in the construction in that it enables us to write and structure proofs in the style of classical mathematics, maintaining the fiction that somehow a maximal ideal has oracularly partitioned the ring elements into those which are zero modulo $m$ and those which are invertible modulo $m$ ; while in fact, no such partition has been computed and all the actual computational work is carried out by the proofs themselves. We illustrate this point with several case studies in Section 2.

As further spelled out in Section 4.4, the construction is closely related to the dynamical approach to maximal ideals. The central premise of that approach is that we may blithely assume that a given element $x \in A$ is zero modulo the maximal ideal if we are also prepared to backtrack and continue computing in case this assumption later turns out to be inconsistent and x is actually invertible modulo the maximal ideal.

This idea is precisely codified by the iterative maximal ideal construction in that we have the residue field property $\begin{matrix} (†) & x \in m ⟺ \neg (1 \in m + (x)) \end{matrix}$ by Lemma 1.1(c): The elements of $m$ are exactly those ring elements for which there is a way to transform the contrary assumption $1 \in m + (x)$ to the conclusion $1 = 0$ . The equivalence (†) expresses the essence of the maximal ideal construction – only that it cannot serve as a definition because of its evident circularity. The construction resolves this circularity by stratification along a given enumeration. Section 4 explains how set-theoretic forcing facilitates a second resolution which does not require an enumeration.

2. On the intersection of all prime ideals

Classically, Krull’s lemma states that the intersection of all prime ideals is the nilradical, the ideal $\sqrt{(0)}$ of all nilpotent elements. In our setup, we have the following substitute concerning complements: $\begin{matrix} {\sqrt{(0)}}^{c} = ⋃_{\begin{array}{c} p \subseteq A \\ p prime \\ p \neg \neg -stable \end{array}} p^{c} = ⋃_{\begin{array}{c} p \subseteq A \\ p prime \\ p radical \end{array}} p^{c} . \end{matrix}$

Lemma 2.1.
Let $x \in A$ . Then there is an ideal $p \subseteq A$ which is
“x-prime” in the sense that $1 \in p \Rightarrow x \in \sqrt{(0)}$ and $a b \in p \land (b \in p \Rightarrow x \in \sqrt{(0)}) ⟹ a \in p$ , that is, prime if the negations occurring in the definition of “prime ideal” are understood as “ $φ \Rightarrow x \in \sqrt{(0)}$ ”,

“x-stable” in the sense that $((a \in p \Rightarrow x \in \sqrt{(0)}) \Rightarrow x \in \sqrt{(0)}) \Rightarrow a \in p$ ,

radical,

and such that $x \in p$ if and only if x is nilpotent.

Proof.
The localization $A [x^{- 1}]$ is again countable, hence the construction of Section 1 can be carried out to obtain a maximal (and hence prime) ideal $m \subseteq A [x^{- 1}]$ . Every negation occurring in the terms “maximal ideal” and “prime ideal” refers to $1 = 0$ in $A [x^{- 1}]$ , which is equivalent to x being nilpotent.

The preimage of $m$ under the localization homomorphism $A \to A [x^{- 1}]$ is the desired x-prime ideal. □
Corollary 2.2 (Krull [78]).

Let $x \in A$ be an element which is not nilpotent. Then there is a (radical and $\neg \neg$ -stable) prime ideal $p \subseteq A$ such that $x \notin p$ .

Proof.
Because x is not nilpotent, the notions of an x-prime ideal and an ordinary prime ideal coincide. Hence the claim follows from Lemma 2.1. □
Theorem 2.3 (Krull’s separation lemma).

Let $S \subseteq A$ be a multiplicatively closed subset which does not contain zero. Then there is a (radical and $\neg \neg$ -stable) prime ideal $p \subseteq A$ such that $S \cap p = \emptyset$ .

Proof.
As in the proof of Corollary 2.2, the desired prime ideal is the preimage under the localization morphism $A \to A [S^{- 1}]$ of a maximal ideal constructed in $A [S^{- 1}]$ . If S is not a detachable subset of A, the localization $A [S^{- 1}]$ can fail to be countable; however, in any case, it is subcountable so that the iterative maximal ideal construction can still be carried out (Section 1.3). □

The general case of Krull’s separation lemma for arbitrary commutative rings is, over zf, equivalent to the Boolean prime ideal theorem [9].

An essential part of constructive algebra is to devise tools to import proofs from classical commutative algebra into the constructive setting.7
⁷
Forms of Zorn’s Lemma similar to Krull’s Lemma feature prominently in algebra; to wit, in ordered algebra there are the Artin–Schreier theorem for fields, Levi’s theorem for abelian groups and Ribenboim’s extension to modules. Dynamical algebra aside, to which we come back later, these statements have recently gained attention from the angle of proof theory at large; see, for example, [30,103,111–113,123,149,150].

The following two statements are established test cases exploring the power of such tools [10,40,43,97,104,108,121,122,124,128].
Proposition 2.4.
Let $f \in A [X]$ be a polynomial.
If f is nilpotent in $A [X]$ , then all coefficients of f are nilpotent in A.

If f is invertible in $A [X]$ , then all nonconstant coefficients of f are nilpotent.

These facts have abstract classical proofs employing Krull’s lemma as follows.
Proof of (a). Simple induction over the formal degree of f if A is reduced; the general case reduces to this one: For every prime ideal $p$ , the coefficients of f vanish over the reduced ring $A / p$ . Hence they are contained in all prime ideals and are thereby nilpotent. □

Proof of (b). Simple induction if A is an integral domain; the general case reduces to this one: For every prime ideal $p$ , the nonconstant coefficients of f vanish over the integral domain $A / p$ . Hence they are contained in all prime ideals and are thereby nilpotent. □

Both statements admit direct computational proofs which do not refer to prime ideals; the challenge is not to find such proofs, but rather to imitate the two classical proofs above constructively, staying as close as possible to the original. It is remarkable that the construction of Section 1 meets this challenge at all, outlined as follows, despite its fundamental reliance on nondetachable subsets.

We continue assuming that A is countable: Section 4 indicates how this assumption can be dropped in quite general situations, while for the purposes of specific challenges such as Proposition 2.4 we could also simply pass to the countable subring generated by the polynomial coefficients or employ the method of indeterminate coefficients – the special instance of Proposition 2.4(a) for the countable ring $A = Z [A_{0}, \dots, A_{n}] / (\dots)$ , where we mod out the equations expressing that the indeterminate polynomial $\sum_{i = 0}^{n} A_{i} X^{i}$ is nilpotent of index at most m, implies all other such instances, and similarly for Proposition 2.4(b).
Proof of Proposition 2.4.
The first claim follows from a simple induction if A is a reduced ring. In the general case, write $f = a_{n} X^{n} + a_{n - 1} X^{n - 1} + \dots + a_{0}$ . Let $p$ be a radical $a_{n}$ -prime ideal as in Lemma 2.1. Since $A / p$ is reduced, the nilpotent coefficient $a_{n}$ vanishes over $A / p$ . Thus $a_{n} \in p$ , hence $a_{n}$ is nilpotent. Since the polynomial $f - a_{n} X^{n}$ is again nilpotent, we can continue by induction.

The second claim follows by a simple inductive argument if A is an integral domain with double negation stable equality. In the general case, write $f = a_{n} X^{n} + \dots + a_{0}$ and assume $n ⩾ 1$ . To reduce to the integral situation, let $p$ be an $a_{n}$ -prime ideal as in Lemma 2.1. With negation “ $\neg φ$ ” understood as “ $φ \Rightarrow a_{n} \in \sqrt{(0)}$ ”, the quotient ring $A / p$ is an integral domain with double negation stable equality. Hence $a_{n} = 0$ in $A / p$ , so $a_{n} \in p$ whereby $a_{n}$ is nilpotent. The polynomial $f - a_{n} X^{n}$ is again invertible in $A [X]$ (since the group of units is closed under adding nilpotent elements) so that we can continue by induction. □

Just as Corollary 2.2 is a constructive substitute for the recognition of the intersection of all prime ideals as the nilradical, the following proposition is a substitute for the classical fact that the intersection of all maximal ideals is the Jacobson radical. As is customary in constructive algebra [80, Section IX.1], by Jacobson radical we mean the ideal ${x \in A | \forall y \in A . 1 - x y \in A^{\times}}$ .
Proposition 2.5.
Let $x \in A$ . If x is apart from the Jacobson radical (that is, $1 - x y \notin A^{\times}$ for some element y), then there is a maximal ideal $m$ such that $x \notin m$ .
Proof.
The standard proof as in [80, Lemma IX.1.1] applies: There is an element y such that $1 - x y$ is not invertible. By Example 1.7, there is an ideal $m$ above $a : = (1 - x y)$ which is maximal not only as an ideal of $A / a$ (where “ $\neg φ$ ” means “ $φ \Rightarrow 1 \in a$ ”) but also as an ideal of A (where “ $\neg φ$ ” means “ $φ \Rightarrow 1 = 0$ ”). If $x \in m$ , then $1 = (1 - x y) + x y \in m$ ; hence $x \notin m$ . □

The two test cases presented in Proposition 2.4 only concern prime ideals. In contrast, the following example crucially rests on the maximality of the ideal $m$ .
Proposition 2.6 (⊛).

Let $M \in A^{n \times m}$ be a matrix with more rows than columns. Assume that the induced linear map $A^{m} \to A^{n}$ is surjective. Then $1 = 0$ .

Proof.
By passing to the quotient $A / m$ , we may assume that A is a residue field. In this case the claim is standard linear algebra:

If any of the matrix entries is invertible, the matrix could be transformed by elementary row and column operations to a matrix of the form $(\begin{array}{cc} 1 & 0 \\ 0 & M^{'} \end{array})$ , where the induced linear map of the submatrix $M^{'}$ is again surjective. Thus $1 = 0$ by induction.

Hence by the residue field property all matrix entries are zero. But the vector $(1, 0, \dots, 0) \in A^{n}$ still belongs to the range of $M = 0$ , hence $1 = 0$ by $n > 0$ . □

After removing the countability assumption by the technique of Section 4, we display an unrolled version of this proof of Proposition 2.6 on page 285.

A more significant case study is Suslin’s lemma, the fundamental and originally non-constructive ingredient in his second solution of Serre’s problem [136]. The classical proof, concisely recalled in Yengui’s constructive account [152], reduces modulo maximal ideals. The construction of Section 1 offers a constructive substitute. However, since gcd computations are required in the quotient rings, it is not enough that they are residue fields; they need to be geometric fields. Hence our approach has to be combined with the technique variously known as Friedman’s trick, nontrivial exit continuation or baby version of Barr’s theorem in order to yield a constructive proof [11,25,52,88]. We have chosen to not undertake a formalization of this approach; but we nevertheless believe that, after removing the countability assumption using the technique of Section 4 and unwinding all auxiliary definitions, we recover Yengui’s proof.

Although not the focus of this text, we have also analyzed classical proofs making use of minimal prime ideals; see Remark 4.27 below.
3. Formalization in weaker foundations

The construction presented in Section 1 crucially rests on the flexibility of nondetachable subsets: In absence of additional assumptions as in Proposition 1.8, we cannot give the ideals $m_{n}$ by decidable predicates $A \to {0, 1}$ – without additional hypotheses on A, membership of the ideals $m_{n}$ is not decidable. As such, the construction is naturally formalized in intuitionistic set theories such as czf or izf, which natively support such flexible subsets.

In this section, we explain how with some more care, the construction can also be carried out in much weaker foundations such as Heyting arithmetic ha. While formulation in classical Peano arithmetic pa is routine, the development in ha crucially rests on a specific feature of the construction, namely that the condition for membership is a negative condition.

To set the stage, we specify what we mean by a ring in the context of arithmetic. One option would be to decree that an arithmetized ring should be a single natural number coding a finite set of ring elements and the graphs of the corresponding ring operations; however, this perspective is too narrow, as we also want to work with infinite rings.

Instead, an arithmetized ring should be given by a “formulaic setoid with ring structure”, that is: by a formula $A (n)$ with free variable n, singling out which natural numbers constitute representatives of the ring elements; by a formula $E (n, m)$ describing which representatives are deemed equivalent; by a formula $Z (n)$ singling out representatives of the zero element; by a formula $P (n, m, s)$ singling out representatives s of sums; and so on with the remaining data constituting a ring; such that axioms such as $\begin{aligned} \forall n . Z (n) \Rightarrow A (n) “every zero representative belongs to the ring” \\ \exists n . Z (n) “there is a zero representative” \\ \forall n, m . Z (n) \land Z (m) ⟹ E (n, m) “every two zero representatives are equivalent” \\ \forall z, n . Z (z) \land A (n) ⟹ P (z, n, n) “zero is neutral with respect to addition” \end{aligned}$ hold. This conception of arithmetized rings deviates from the usual definition in reverse mathematics [133, Definition III.5.1] to support quotients even when ha cannot verify the existence of canonical representatives of equivalence classes. It is related to the notion of ring objects in the initial arithmetic universe obtained as the exact completion of an appropriate Skolem theory [82,146]. A similar, but more specialized, notion has been considered by Perdry [95, Section 2].

Although first-order arithmetic cannot quantify over ideals of arithmetized rings, specific ideals can be given by formulas $I (n)$ such that axioms such as $\begin{aligned} \forall n . I (n) \Rightarrow A (n) “ I \subseteq A ” \\ \exists n . Z (n) \land I (n) “ 0 \in I ” \end{aligned}$ hold. It is in this sense that we are striving to adapt the construction of Section 1 to describe a maximal ideal.

In this context, we can arithmetically imitate any set-theoretic description of a single ideal as a subset cut out by an explicit first-order formula. However, for recursively defined families of ideals, we require a suitable recursion theorem: If we are given (individual formulas $M_{n} (x)$ indexed by numerals representing) ideals $m_{0}, m_{1}, m_{2}, \dots$ , we cannot generally form $⋃_{n \in N} m_{n}$ , as the naive formula “ $⋁_{n \in N} M_{n} (x)$ ” representing their union would have infinite length. We can take the union only if the family is uniformly represented by a single formula $M (n, x)$ (expressing that x represents an element of $m_{n}$ ).

This restriction is a blocking issue for arithmetizing the construction of the chain $m_{0} \subseteq m_{1} \subseteq \dots$ of Section 1. Because $m_{n}$ occurs in the definition of $m_{n + 1}$ in negative position, naive arithmetization results in formulas of unbounded logical complexity, suggesting that a uniform definition might not be possible.

This issue has a counterpart in type-theoretic foundations of mathematics, where the family ${(m_{n})}_{n \in N}$ cannot be given as an inductive family (failing the positivity check), and is also noted, though not resolved, in related work [63, p. 11]. The issue does not arise in the context of pa, where the law of excluded middle allows us to bound the logical complexity: We can blithely define the joint indicator function $g (n, i)$ for the sets $G_{n}$ (such that $G_{n} = {x_{i} | i \in N, g (n, i) = 1}$ ) of Lemma 1.9 by the recursion $\begin{aligned} g (0, i) = 0 \\ g (n + 1, i) = \{\begin{array}{ll} 1, & if g (n, i) = 1 \lor (i = n \land 1 \notin (g (n, 0) x_{0}, \dots, g (n, n - 1) x_{n - 1}, x_{n})) \\ 0, & else. \end{array} \end{aligned}$ This recursion can be carried out within pa since the recursive step only references the finitely many values $g (n, 0), \dots, g (n, i)$ . Heyting arithmetic, however, does not support this case distinction. The formalization of the construction in ha is only unlocked by the following direct characterization.

Lemma 3.1 (In the setting of Section 1.2.).

For every finite binary sequence $v = v_{0} \dots v_{n - 1}$ , let $a_{v}$ be the ideal $(v_{0} x_{0}, \dots, v_{n - 1} x_{n - 1}, x_{n})$ . Then:

For every such sequence $v = v_{0} \dots v_{n - 1}$ , if $⋀_{i = 0}^{n - 1} (v_{i} = 1 \Leftrightarrow 1 \notin a_{v_{0} \dots v_{i - 1}})$ , then $a_{v} = (G_{n}) + (x_{n})$ . In particular, in this case $x_{n} \in G$ if and only if $1 \notin a_{v}$ .

For every natural number $n \in N$ , $\begin{matrix} x_{n} \in G ⟺ \neg \exists v \in {0, 1}^{n} . 1 \in a_{v} \land ⋀_{i = 0}^{n - 1} (v_{i} = 1 \Leftrightarrow 1 \notin a_{v_{0} \dots v_{i - 1}}) . \end{matrix}$

Proof.
The first part is by induction, employing the equivalences of Lemma 1.9. The second rests on the tautology $\neg α ⟺ \neg (α \land (φ \lor \neg φ))$ : $\begin{aligned} x_{n} \in G & ⟺ \neg (1 \in (G_{n}) + (x_{n})) ⟺ \neg (1 \in (G_{n}) + (x_{n}) \land ⋀_{i = 0}^{n - 1} (x_{i} \in G \lor x_{i} \notin G)) \\ ⟺ \neg \exists v \in {0, 1}^{n} . (1 \in (G_{n}) + (x_{n}) \land ⋀_{i = 0}^{n - 1} (v_{i} = 1 \Leftrightarrow x_{i} \in G)) \\ ⟺ \neg \exists v \in {0, 1}^{n} . (1 \in a_{v} \land ⋀_{i = 0}^{n - 1} (v_{i} = 1 \Leftrightarrow 1 \notin a_{v_{0} \dots v_{i - 1}})) \end{aligned}$ □

Condition (b) is manifestly formalizable in arithmetic, uniformly in n.
4. Expanding the scope to general rings

The iterative construction presented in Section 1 can be employed to constructively recast suitable classical proofs in commutative algebra which rely on maximal ideals. However, the construction requires an enumeration $N ↠ A$ of the ring elements. This section deals with the case that no such enumeration exists or is available.

As a first observation, we notice that without much difficulty, the same technique can be used in situations where the maximality condition “ $1 \notin m + (x)$ implies $x \in m$ ” is required only for a finite number $x_{0}, \dots, x_{n - 1}$ of ring elements fixed beforehand. In this case we can apply the construction of Section 1 to this finite enumeration and use the resulting ideal $m_{n}$ as a partial substitute for an intangible maximal ideal.

We propose to employ tools from pointfree topology to widen the applicability of this partial substitute to cases where the inspected ring elements are not fixed beforehand. The idea is to dynamically grow a partial enumeration as needed: When following a given proof, we initially approximate the unavailable complete enumeration $N ↠ A$ by the nowhere-defined partial function $f : N ⇀ A$ . When the proof requires that some particular element $x_{0} \in A$ is contained in the image of f, we grow f to the more-defined partial function $f^{'}$ mapping 0 to $x_{0}$ . When the proof requires some further element $x_{1} \in A$ to be part of the enumeration, we further refine $f^{'}$ to the partial function $f^{″}$ with $f^{″} (0) = x_{0}$ , $f^{″} (1) = x_{1}$ . As the proof runs its course, we pass to better and better approximations on an on-demand basis.

To make this informal idea precise, we employ constructive forcing to pass from the base universe V to a suitably enlarged universe $V^{\nabla}$ . In this larger universe, the multitude of better and better finite approximations to a hypothetical enumeration of A is reified as a single coherent entity, the generic enumeration of A. On the one hand, the existence of this enumeration exhibits $V^{\nabla}$ as a better (more well-adapted) universe to work in than the base V. On the other hand, the extended universe is still close to V in that the two universes validate the same bounded first-order statements. We can hence work in $V^{\nabla}$ to deduce results about V. Even in case that V validates classical logic – an assumption we do not make – the enlarged universe typically only validates intuitionistic logic.

Constructive forcing is usually described in the language of sheaves and toposes [21,59,91,115,118,135,140,151] and closely linked to pointfree topology. For surveys of these topics, we refer to [17,25,71–73,144,145]. The objective of this section is to give a purely syntactical account, not employing categorical language, having the requirements of predicative mathematics [44,82,146] in mind and focusing on computational content. Related work includes [6, Section 2.4], [37], [106, Section 2.3] and [117].

We circumvent the actual construction of $V^{\nabla}$ , which would require sheaves, by instead directly giving a translation $φ \mapsto φ^{\nabla}$ of formulas in such a way that a sentence φ holds in $V^{\nabla}$ iff $φ^{\nabla}$ holds in V. This translation is a parametric generalization of the venerable double negation translation. In fact, depending on the forcing notion used, we recover

the standard double negation translation, where existential quantification is translated to impossibility of a counterexample (“ $\exists \mapsto \neg \forall \neg$ ”);

the refined translation sometimes known as Friedman’s nontrivial continuation trick, as used in one of the proofs of Barr’s theorem; and

the topological translation, where existential quantification is translated to local existence.8

⁸
For more on the topological translation, see [26, Section 4.3] or [25, Section 2.4]. For instance, the translation of the (not constructively provable) claim “every real symmetric matrix has an eigenvector” is the (refutable) statement “for every continuous family of real symmetric matrices, eigenvectors can locally be picked in a continuous fashion”, while the translation of the (constructively provable) claim “every real symmetric matrix does not not have an eigenvector” is the (constructively provable) statement “for every continuous family of real symmetric matrices, on an open dense set of parameter values, eigenvectors can locally picked in a continuous fashion”. In one direction, the topological translation enables quick nonprovability results, while in the other it enables continuous globalizations.

The translation of formulas is accompanied by a translation of proofs (with just a polynomial increase in length), ensuring that if a set of axioms entails a certain conclusion, the set of translated axioms entails the translated conclusion. Translated proofs admit a direct computational interpretation, as programs running in a general eventually monad described below. Specific versions of the eventually monad have been studied in the reactive programing community [33,92].

4.1. Forcing notions

The particular flavor of forcing is determined by its notion of forcing. This is a preorder $(L, ≼)$ equipped with a covering system (Definition 4.1 below). The elements of L are called forcing conditions and are regarded as partial approximations to (perhaps fictitious) ideal objects. The relation $τ ≼ σ$ expresses that τ is a refinement of σ, that is that τ contains more information than σ and hence restricts the fictitious ideal objects approximated by τ more strongly than σ does, just as $[3.14, 3.15]$ is a smaller interval than $[3.1, 3.2]$ .

The associated covering system specifies which kinds of refinements we are prepared to make. In the following definition, the expression $↓ σ$ denotes the set ${τ \in L | τ ≼ σ}$ of all refinements of σ and the expression $↓ R$ denotes the downward closure of a subset $R \subseteq L$ , that is the set ${τ \in L | \exists σ \in R . τ ≼ σ} = ⋃_{σ \in R} ↓ σ$ . For a set M, we denote its powerset (or powerclass) by $P (M)$ .

Definition 4.1 ([75, p. 24], ⊛).

A covering system on a poset L consists of a set $Cov (σ) \subseteq P (↓ σ)$ of coverings for each element $σ \in L$ subject only to the following stability condition: If $τ ≼ σ$ and $R \in Cov (σ)$ , there should be a covering $S \in Cov (τ)$ such that $S \subseteq ↓ R$ .

Definition 4.2 (⊛).

A filter of a forcing notion $(L, Cov)$ is a subset $F \subseteq L$ such that

F is upward-closed (“closed under coarser elements”): if $τ ≼ σ$ and if $τ \in F$ , then $σ \in F$ ;

F is downward-directed: F is inhabited, and if $α, β \in F$ , then there is a common refinement $σ ≼ α$ , β such that $σ \in F$ ; and

F splits the covering system: if $σ \in F$ and $R \in Cov (σ)$ , then $τ \in F$ for some $τ \in R$ .

It can well happen that a forcing notion does not admit any filters; the purpose of a forcing notion is to give rise to a forcing extension of the universe in which a filter can always be found. The canonical filter living in the extended universe is called the generic filter.

Example 4.3 (⊛).

To force the existence of an enumeration of the elements of a (perhaps uncountable) set X, let $L : = X^{*}$ be the set of finite lists of elements of X. We picture a list $x_{0} \dots x_{n - 1}$ as code for the partial enumeration $f : N ⇀ X$ given by $f (i) = x_{i}$ for $i = 0, \dots, n - 1$ , and declare $τ ≼ σ$ iff σ is a prefix of τ, expressing that the partial enumeration coded by τ refines the one coded by σ.

For each list $σ \in L$ , we decree that its coverings are the set ${σ y | y \in X}$ and, for each element $a \in X$ , the set ${σ σ^{'} | σ^{'} \in L, a \in σ σ^{'}}$ . (By $σ y$ , we mean the enlarged list with y as an added element at the end. By $σ σ^{'}$ , we mean the concatenation of the lists σ and $σ^{'}$ . We write $a \in ν$ if and only if the list ν has a among its terms.) The first kind of covering expresses that we are prepared to grow a partial enumeration in order to make it more defined, the second to ensure that any given element a is enumerated.

The filters of this forcing notion are in canonical one-to-one correspondence with surjections $N ↠ X$ , by mapping a filter F to the gluing of the partial enumerations coded by the lists in F. These partial enumerations indeed agree on their common domain of definition by the directedness condition; and because F splits the covering system, the gluing of the partial enumerations is total and surjective. Conversely, a surjection corresponds to the filter of its finite prefixes. In case that X is uncountable, there are no filters, and this direct correspondence degenerates to the unique bijection between empty sets.

Example 4.4.
We can also directly force the existence of a maximal ideal, instead of first forcing the existence of an enumeration and then applying the Krivine construction in the enlarged universe. (The relation of these two ways of acquiring a maximal ideal is explored in Proposition 4.26.) To this end, let L be the poset of finitely generated ideals of A ordered by reverse inclusion, and for each element $a \in L$ , let its collection of coverings be $\begin{matrix} Cov (a) : = {{a + (x)} \cup {a + (u) | u \in A, \exists v \in A . u + v x = 1} | x \in A} \cup {{a | 1 = 0} | 1 \in a} . \end{matrix}$ The first kind of covering expresses that we are prepared to grow partial approximations exactly as the strong maximality condition “ $x \in m$ or $1 \in m + (x)$ ” would suggest: An approximation $a$ can grow to $a^{'} = a + (x)$ (ensuring $x \in a^{'}$ ), or to $a^{'} = a + (u)$ where $u \in A$ is such that $u + v x = 1$ for some $v \in A$ (ensuring $1 \in a^{'} + (x)$ ). The second kind of covering implements the objective “ $1 \in m \Rightarrow 1 = 0$ ”.

The filters of this forcing notion are in canonical one-to-one correspondence with those ideals $m$ of A which are maximal in the strong sense that $\begin{matrix} 1 \in m ⟹ 1 = 0 and x \in m \lor 1 \in m + (x) . \end{matrix}$ The correspondence is by mapping a filter F to the ideal $\cup F$ and conversely by mapping a maximal ideal $m$ to the filter of finitely generated ideals contained in $m$ .
Example 4.5.
To recover the double negation translation, let L be the trivial poset containing just a single element ⋆ and decree $\begin{matrix} Cov (⋆) : = {{⋆ | φ} \cup {⋆ | \neg φ} | φ \in Ω} (where Ω is the set of truth values). \end{matrix}$ This definition expresses that we are prepared, for every truth value $φ \in Ω$ , to assume φ or to assume $\neg φ$ .

This forcing notion has at most one filter, the set L itself. This set is a filter if and only if the law of excluded middle holds.
Example 4.6.
Let $T$ be a coherent (or geometric) propositional theory [74, Definition D1.1.3], such as the theory of prime ideals of a given ring, and let L be its Lindenbaum algebra, the set of formulas in the language of $T$ modulo provable equivalence, endowed with the ordering where $[φ] ≼ [ψ]$ if and only if $φ ⊢ ψ$ modulo $T$ . In the coherent case, we decree $\begin{matrix} Cov ([φ]) : = {{[ψ_{1}], \dots, [ψ_{n}]} | n ⩾ 0, φ ⊣ ⊢ (ψ_{1} \lor \dots \lor ψ_{n}) modulo T}; \end{matrix}$ in the geometric case, we decree $\begin{matrix} Cov ([φ]) : = {M \in P (↓ [φ]) | φ ⊢ (⋁_{K \in M} ⋁_{ψ \in K} ψ) modulo T} . \end{matrix}$ The filters of this forcing notion are in canonical one-to-one correspondence with models of the theory $T$ ; an element $[φ] \in L$ is read as partial knowledge about a (perhaps fictitious) model of $T$ . For instance, if $T$ is the theory of strong prime ideals of a given ring A, with propositional symbols $P_{x}$ (interpreted as “x is contained in the prime ideal”), we are prepared to refine $[P_{x y}]$ to $[P_{x}]$ and to $[P_{y}]$ (expressing the objective “ $x y \in p \Rightarrow x \in p \lor y \in p$ ”).

To accommodate non-propositional theories with sorts, such as the theory of rings or of local rings, the concept of forcing notion is not sufficiently flexible. To handle this case, we need to generalize from posets equipped with covering systems to sites, categories equipped with Grothendieck coverages.
Example 4.7.
Let $(⊢)$ be a finitary multi-conclusion entailment relation [34,81,89,113,114,131] or a geometric entailment relation ([126, Section 3], [148]) on a set S. We equip the set $L : = P_{ω} (S)$ of finitely enumerable (Kuratowski-finite) subsets of S with the following ordering: $A ≼ B$ iff $A ⊢ b$ for every element $b \in B$ . For each pair $(A, B)$ such that $A ⊢ B$ , we declare that the set ${A \cup {b} | b \in B}$ should be a covering of $A$ .

For this forcing notion, there is a canonical one-to-one correspondence between the filters of L and the ideals of the entailment relation: If $F \subseteq L$ is a filter, then $⋃ F$ is an ideal. If $ν \subseteq S$ is an ideal, then ${A \in P_{ω} (S) | A \subseteq ν}$ is a filter.

For suitable choices of the entailment relation $(⊢)$ , we recover the forcing notions of several of the earlier examples. For instance, up to inessential details (“Morita equivalence”), the forcing notion of Example 4.6 is the special case where S is the set of atomic propositions and where $A ⊢ B$ iff $⋀_{φ \in A} φ ⊢ ⋁_{ψ \in B} ψ$ modulo $T$ . The forcing notion of Example 4.4 is the special case where the entailment relation is that of [126, p. 87].
Example 4.8.
Let $(P, ⩽)$ be a complete lattice and let $Inc$ be a Scott-open predicate on P as in [85]. Then the opposite lattice of P becomes a forcing notion with coverings given by $\begin{matrix} Cov (σ) : = {\emptyset | Inc σ} \cup {{σ \lor ν} \cup {σ \lor ν^{'} | ν^{'} \in \overline{ν}} | ν \in P}, \end{matrix}$ where the joins are computed in P and $\overline{ν}$ denotes the pseudo-complement of ν as in [85, Equation (6)], that is the set of those elements $ν^{'} \in L$ such that $Inc (ν \lor ν^{'})$ .

The filters of this forcing notion are in canonical one-to-one correspondence with the proper $Inc$ -complete elements of P, that is those elements α with $\neg Inc α$ for which the disjunction $\begin{matrix} ν ⩽ α or Inc (α \lor ν) \end{matrix}$ holds for all elements $ν \in P$ . The correspondence is by mapping a filter F to its join $⋁ F \in P$ and conversely by mapping a proper $Inc$ -maximal element α to the filter $↓ α$ .

If P is algebraic, that is if every element is the join of the compact elements below it, we can restrict this covering system to the poset $KP$ of compact elements of P: $\begin{matrix} {Cov}_{KP} (σ) : = {\emptyset | Inc σ} \cup {{σ \lor ν} \cup {σ \lor ν^{'} | ν^{'} \in \overline{ν} \cap KP} | ν \in KP} . \end{matrix}$ The one-to-one correspondence from above then restricts to a correspondence between the filters of $({(KP)}^{op}, {Cov}_{KP})$ and those proper elements α of P for which the disjunction “ $ν ⩽ α \lor Inc (α \lor ν)$ ” holds for all elements $ν \in KP$ . In this way we can recover several other examples for forcing notions. For instance, Example 4.4 is the special case where P is the complete lattice of all ideals of A and $Inc a$ denotes $1 \in a$ .
Remark 4.9.
Classical set-theoretic forcing does without an explicit specification of coverings because implicitly the double negation topology is used: $\begin{matrix} Cov (σ) : = {M \in P (↓ σ) | \forall τ ≼ σ . \neg \neg \exists ν ≼ τ . ν \in M} . \end{matrix}$ Up to the double negation which disappears in a classical metatheory, sets M as displayed are called dense (in $↓ σ$ ) in the literature on classical set-theoretic forcing, and upward-closed downward-directed subsets of F which meet all dense sets are called generic filters, in line (but more restrictive) than our terminology for arbitrary forcing notions.

If the poset L of forcing conditions is atomless (that is, for every condition $σ \in L$ there are conditions α, $β ≼ σ$ without a common refinement), as in commonly the case in classical set-theoretic forcing [119, Lemma 1.33], then no such generic filter exists in V. In contrast, coarser covering systems on atomless posets may allow filters to exist already in V, as the examples above demonstrate.

A forcing notion is not only a template for a forcing extension of the universe and for a suitable formula translation, but also for a space in the sense of pointfree topology. The forcing conditions constitute the basic opens of the induced space while the covering system specifies generating coverings of those opens. The points of this space are in canonical bijection with the filters of the forcing notion.

For the purposes of forcing, the most important use case is when the forcing notion is nontrivial but no filters exist in the base universe. In this case the induced space is nontrivial and without points, highlighting that a pointfree approach to topology is required to make sense of this space.

Conversely, every space in pointfree topology gives rise to a forcing notion such that its filters are in canonical one-to-one correspondence with the points of the space. For instance, let a space be given by a frame L as in locale theory [100]. Then a covering system is defined by $Cov (σ) : = {M \in P (L) | σ = ⋁ M}$ .
4.2. The eventually monad

Let L be a forcing notion. A predicate P on L is called monotone iff $τ ≼ σ$ implies $P σ \Rightarrow P τ$ . Such predicates express positive observations which are stable under refinement of approximations. For instance, in the case of the forcing notion of Example 4.3, the proposition $P σ$ could express that a particular element $x_{0} \in X$ is among the terms of σ.

For a monotone predicate P, we introduce a derived predicate denoted “ $P | σ$ ” (pronounced “P bars σ”) expressing that no matter how an approximation σ evolves to a better approximation τ, eventually $P τ$ will hold. Similar to Coquand and Persson’s approach to well quasi-orders [42, Definition 6] and Coquand and Lombardi’s approach to Noetherian rings [36,41], we define this predicate in a direct inductive fashion, by the following generating clauses (⊛):

If $P σ$ , then $P | σ$ .

If $P | τ$ for all $τ \in R$ , where R is some covering of σ, then $P | σ$ .

Hence, to witness

P | σ

, we may directly witness

P σ

or first ask for a refinement of σ as envisaged by the covering system.9

⁹
The induction principle [1,3,4,105] corresponding to the definition of the bar predicate is this: For every predicate Q on L, if
for every element $σ \in L$ , $P σ \Rightarrow Q σ$ , and if

for every element $σ \in L$ and every covering $R \in Cov (σ)$ , $(\forall τ \in R . Q τ) \Rightarrow Q σ$ ,
then $P | σ \Rightarrow Q σ$ for every element $σ \in L$ .

Lemma 4.10 (⊛).

The relaxation of P is again monotone, that is $P | σ \Rightarrow P | τ$ if $τ ≼ σ$ .

Proof.
By induction on the given witness of $P | σ$ :
If $P σ$ , then also $P τ$ and hence $P | τ$ by monotonicity of P.

If $P | σ^{'}$ for all $σ^{'} \in R$ , where R is a covering of σ, then by the stability condition of Definition 4.1 there is a covering $S \in Cov (τ)$ such that $S \subseteq ↓ R$ . Hence for every element $τ^{'} \in S$ , there is an element $σ^{'} \in R$ such that $τ^{'} ≼ σ^{'}$ . By the induction hypothesis, we have $P | τ^{'}$ for all such elements $τ^{'}$ , and hence $P | τ$ .
□

The functor mapping a predicate P to its induced relaxation $P | \cdot$ is a monad on the category of monotone predicates, dubbed the eventually monad. In computer science parlance, this monad is the (parametrized) freer monad [5,76] on Cov, that is the free monad [137, Section 6] on the free functor on Cov. The following two basic results on “escaping the monad” shed light on the meaning of $P | σ$ and are crucial for the forcing extension and the base universe to satisfy the same first-order statements.
Proposition 4.11 (⊛).

Let L be a forcing notion. Let P be a monotone predicate on L. If $P | σ$ , then every filter F which contains σ also contains a refinement $τ ≼ σ$ with $P τ$ .

Proof.
By induction on the given witness of $P | σ$ , as guided by a given filter F:
If $P σ$ , we conclude with setting $τ : = σ$ .

If $P | τ$ for all $τ \in R$ , where R is some covering of σ, then by the splitting property the filter F contains a refinement $τ_{0} ≼ σ$ with $τ_{0} \in R$ . By the induction hypothesis, there is a further refinement $τ ≼ τ_{0}$ contained in F such that $P τ$ .
□

The converse of Proposition 4.11 can only hold in the case that the formal space presented by the forcing notion has enough points. A case in which the converse emphatically fails is in the situation of Example 4.3 when the set X is uncountable, for in this case there are no filters at all. Illuminating is also the case of forcing a generic sequence $N \to N$ (which is just Example 4.3 in the special case $X : = N$ , but without the second kind of covering): In this case the converse of Proposition 4.11 is equivalent to the principle of monotonic bar induction.

We think of “ $P | σ$ ” as an inductive paraphrasing, not directly referring to filters and indeed even being nontrivial in case there are no filters at all in the base universe, of the statement that every filter containing σ also contains a refinement $τ ≼ σ$ with $P τ$ . While the latter statement refers to filters – ideal, completed objects – the former has a more finitary character.
Lemma 4.12 ([75, Proposition V.3.2], ⊛).

Let L be a forcing notion such that every covering is inhabited. Let P be a constant predicate on L. Then $P | σ$ implies $P σ$ .

Proof.
By induction. In computational terms, we inspect a given witness of $P | σ$ and descend into it, using the assumption that every covering is inhabited in order to pick out branches. □
Example 4.13 (⊛).

In the situation of Example 4.3, let the set X be inhabited by an element $x_{0}$ . Then the criterion of Proposition 4.12 is satisfied: Coverings of the first kind are inhabited by $σ x_{0}$ and coverings of the second kind are inhabited by $σ a$ . In computational terms, if a program in the eventually monad asks for the current approximation σ to be more defined or to include a specific element a, we just append $x_{0}$ respectively a to σ.

Example 4.14.
In the situation of Example 4.5, for every monotone predicate P we have $P | ⋆$ if and only if $\neg \neg (P ⋆)$ . That is, the eventually monad coincides with the double negation or continuation monad. In particular, we can generally escape from the monad only in presence of the law of excluded middle.
Example 4.15.
In the situation of Example 4.8, let $σ_{0} \in L$ be a fixed element. Let $P σ : \Leftrightarrow (σ_{0} ⩽ σ)$ . Then $P | σ$ if and only if $σ_{0} ⊑ σ$ in the sense of the inductively generated relation of [85, Definition 18].

It is prudent to introduce the quantifier-like notation “ $\nabla σ . P σ$ ”, pronounced “eventually it is the case that $P σ$ holds”, for $P | σ$ . For instance, in the situation of Example 4.3, we have $\begin{matrix} \forall x \in X . \nabla σ . x \in σ (meaning \forall x \in X . ((x \in \cdot) | σ)), \end{matrix}$ expressing that for every element $x \in X$ it will eventually be the case that it is enumerated; but typically we do not have $\begin{matrix} \nabla σ . \forall x \in X . x \in σ (meaning (\forall x \in X . x \in \cdot) | σ), \end{matrix}$ expressing that eventually it will be the case that all elements are enumerated. Remark 4.16.
The “localization” $P | \cdot$ of a monotone predicate P has a close connection to sheaf theory. A monotone predicate P gives rise to a presheaf on the thin category induced from L, more precisely a subpresheaf of the terminal presheaf, by mapping an element $σ \in L$ to the truth value of $P σ$ . The presheaf mapping σ to the truth value of $P | σ$ is then the sheafification with respect to the Grothendieck coverage induced from the covering system attached to L.

4.3. The translation

Let L be a forcing notion. The purpose of this section is to describe, purely in terms of the base universe V, when a bounded first-order statement holds in the forcing extension $V^{\nabla}$ generated by L. We consider statements over the (large) first-order signature Σ which has (⊛)

one sort $\underline{X}$ for each set X in the base universe,

one n-ary function symbol $\underline{f} : \underline{X_{1}} \times \dots \times \underline{X_{n}} \to \underline{Y}$ for each map $f : X_{1} \times \dots \times X_{n} \to Y$ ,

one n-ary relation symbol $\underline{R} ↪ \underline{X_{1}} \times \dots \times \underline{X_{n}}$ for each relation $R \subseteq X_{1} \times \dots \times X_{n}$ , and

an additional unary relation symbol $G ↪ \underline{L}$ (to be interpreted as the generic filter of L).

As usual, substitution

φ [\underline{x_{0}} / x]

of a constant (nullary function symbol) for a free variable and interpretation brackets

⟦ \dots ⟧

are defined; for instance

⟦ \underline{f} (\underline{x}) ⟧ = f (x)

. Recursively in the structure of a formula φ over this signature, and similar to Kripke or Beth semantics, we define what it means that “φ is forced by a condition

σ \in L

”, symbolically denoted as “

σ ⊨ φ

” (⊛):

Finally, when we say that some first-order statement φ “holds in the forcing extension $V^{\nabla}$ ”, we mean $\begin{matrix} \forall σ . σ ⊨ φ, symbolically also written as: φ^{\nabla} . \end{matrix}$ In this way, every statement about the forcing extension is actually a statement about the base universe V. Because of the well-established nature of the eventually monad, these statements have clear computational content; which content exactly, depends on the forcing condition.

In effect, these definitions describe a formula translation $φ \mapsto φ^{\nabla}$ akin to the double negation translation – more precisely, the variant called Gödel–Gentzen translation in [48,49]. There are two differences to this revered translation: Firstly, in place of $\neg \neg$ , a different modality (local operator, see [58, Section 14.5], [57,98]) is used, namely the eventually monad ∇ induced from the forcing notion L, as in the “J-” or “T-translation” [2,47]. Secondly, this modality depends on a parameter, the current forcing condition σ. In the case of the forcing notion of Example 4.5, the translation described here indeed specializes to precisely the double negation translation.

Lemma 4.17 (⊛).

For every first-order formula φ, the interpretation is …

monotone: If $σ ⊨ φ$ and if $τ ≼ φ$ , then also $τ ⊨ φ$ .

local: If $\nabla σ . σ ⊨ φ$ , then $σ ⊨ φ$ .

Proof.
Routine induction on the structure of the formula φ; see, for instance, [134, p. 98]. The fundamental properties of the eventually monad ∇ required for the verification are the “nucleus axioms” (“local operator axioms” [58, Section 14.5], [57]):
$P σ \Rightarrow (\nabla σ . P σ)$

$(\nabla σ . \nabla σ . P σ) \Rightarrow (\nabla σ . P σ)$

$(\nabla σ . P σ \land Q σ) \Leftrightarrow (\nabla σ . P σ) \land (\nabla σ . Q σ)$
□
Theorem 4.18.
The interpretation is sound with respect to intuitionistic first-order logic: If a formula φ is intuitionistically provable, then φ holds in $V^{\nabla}$ .
Proof.
Routine induction on the structure of intuitionistic derivations, see [31, Sections 6.7, 6.8]. For instance, in view of the rule $\begin{matrix} \frac{φ ⊢_{\vec{x}} χ ψ ⊢_{\vec{x}} χ}{φ \lor ψ ⊢_{\vec{x}} χ} \end{matrix}$ of intuitionistic sequent calculus we need to verify that $\begin{matrix} if σ ⊨ \forall \vec{x} : \vec{X} . (φ \Rightarrow χ) and if σ ⊨ \forall \vec{x} : \vec{X} . (ψ \Rightarrow χ), then σ ⊨ \forall \vec{x} : \vec{X} . (φ \lor ψ \Rightarrow χ); \end{matrix}$ this particular verification rests on Lemma 4.17(b). □

It is by Theorem 4.18 that we may “reason in the forcing extension”: If we have established that some statement α holds in $V^{\nabla}$ (for instance, by direct verification of the translated statement $α^{\nabla}$ ) and if we have an intuitionistic proof that α entails some further statement β, then we may conclude that β holds in $V^{\nabla}$ . Just as proofs give rise to programs, translated proofs give rise to programs “with side effects in the eventually monad”.

As an actual construction of $V^{\nabla}$ (as the category of sheaves over the Grothendieck site induced from the forcing notion) is avoided and it is only explained what it means for a statement to hold in $V^{\nabla}$ , our approach is related to the naturalist account of forcing in classical set theory [60, Theorem 2], [93, Section 4], [12]. Both the translation itself as well as Lemma 4.17 and Theorem 4.18 can be extended to the higher-order setting [74, Section D4.1], making it possible to work in the forcing extension much in the same way as in the base universe.
Proposition 4.19.
The forcing extension $V^{\nabla}$ contains a filter of $\underline{L}$ , namely G, in the precise sense that the following statements hold in $V^{\nabla}$ :
$\forall σ : \underline{L} . \forall τ : \underline{L} . (τ \underline{≼} σ \land G τ) \Rightarrow G σ$ .

$\exists σ : \underline{L} . G σ$ .

$\forall α : \underline{L} . \forall β : \underline{L} . (G α \land G β) \Rightarrow \exists σ : \underline{L} . σ \underline{≼} α \land σ \underline{≼} β \land G σ$ .

$\forall σ : \underline{L} . \forall R : \underline{P (L)} . (R \underline{\in} \underline{Cov} (σ) \land G σ) \Rightarrow \exists τ : \underline{L} . G τ \land τ \underline{\in} R$ .

Proof.
Straightforward verification. □
Example 4.20.
For the forcing notion of Example 4.3, the forcing extension contains an enumeration f of $\underline{X}$ in the following sense: Defining “ $f (n) = x$ ” to be an abbreviation for “ $\exists σ : \underline{L} . G σ \land σ \underline{[} n \underline{]} = x$ ”, in the forcing extension we have that
“f is everywhere-defined”: $\forall n : \underline{N} . \exists x : \underline{X} . f (n) = x$ ,

“f is single-valued”: $\forall n : \underline{N} . \forall x : \underline{X} . \forall y : \underline{X} . (f (n) = x \land f (n) = y) \Rightarrow x = y$ , and

“f is surjective”: $\forall x : \underline{X} . \exists n : \underline{N} . f (n) = x$ .
In case X carries a ring structure, we can further define “ $x \in m$ ” to be an abbreviation for “ $\exists n : \underline{N} . (f (n) = x \land x \in m_{n + 1})$ ”, where $m_{n + 1}$ morally refers to the ideal constructed in Section 1 applied to the generic enumeration f, but which formally has to be read along the lines of Lemma 3.1(b). In the forcing extension, we then have that
“ $m$ is an ideal”:

“ $m$ contains the zero element”: $\underline{0} \in m$

“ $m$ is closed under addition”: $\forall x : \underline{A} . \forall y : \underline{A} . (x \in m \land y \in m) \Rightarrow x \underline{+} y \in m$

“ $m$ has the magnet property”: $\forall x : \underline{A} . \forall r : \underline{A} . x \in m \Rightarrow r x \in m$

“ $m$ is maximal in the weak sense”:

“ $m$ is proper”: $\underline{1} \in m \Rightarrow \underline{1} = \underline{0}$

$\forall x : \underline{A} . ((\exists u : \underline{A} . \exists v : \underline{A} . \underline{1} = u \underline{+} v x \land u \in m) \Rightarrow \underline{1} = \underline{0}) \Rightarrow x \in m$

Example 4.21.
For the forcing notion of Example 4.4, the forcing extension contains a strong maximal ideal $n$ of $\underline{A}$ in the following sense: Defining “ $x \in n$ ” to be an abbreviation for “ $\exists a : \underline{L} . G a \land x \underline{\in} a$ ”, in the forcing extension we have that
“ $n$ is an ideal” as in Example 4.20(4), and

“ $n$ is maximal in the strong sense”:

“ $n$ is proper”: $\underline{1} \in n \Rightarrow \underline{1} = \underline{0}$

$\forall x : \underline{A} . x \in n \lor (\exists u : \underline{A} . \exists v : \underline{A} . \underline{1} = u \underline{+} v x \land u \in n)$

Theorem 4.22 (⊛).

Assume that L is inhabited and that every covering is inhabited. Let φ be a bounded first-order formula not containing the unary relation symbol G. Then the following statements are equivalent:

φ holds in V.

φ holds in $V^{\nabla}$ .

Proof.
Routine induction on the structure of φ employing Lemma 4.12. □

Both directions of Theorem 4.22 are central for putting the forcing extension to good use. By the direction “(a) ⇒ (b)”, we may retain everything already known about the base universe when passing to the forcing extension – as long as the facts we would like to import can be phrased as first-order formulas. In the other direction, every result obtained in the forcing extension descends to the base universe – as long as the result can be phrased as a first-order formula and does not mention the generic filter. For classical set-theoretic forcing, this strategy is commented on for instance in [60, Theorem 2].

The assumption of Theorem 4.22 on L is for instance satisfied for the forcing notion of Example 4.3. However, it fails for the forcing notion of Example 4.4. A variant of Theorem 4.22 can do without the requirement that all coverings are inhabited, at the expense of a restricted scope on the interpreted formulas: Theorem 4.23 (⊛).

Assume that L contains a top element 1, and that all iterated coverings of the top element are inhabited (so that $P | 1$ implies P for constant predicates P). Let φ be a coherent implication (a bounded first-order formula of the form $\forall \dots \forall . (\dots \Rightarrow \dots)$ , where antecedent and succedent do not contain “∀” and “⇒”) not containing the unary relation symbol G. Then the following statements are equivalent:

φ holds in V.

φ holds in $V^{\nabla}$ .

Proof.
Omitted. In the language of toposes, the assumption on L ensures that the canonical geometric morphism $V^{\nabla} \to V$ is surjective. Pullback along surjective morphisms preserves and reflects the interpretation of coherent implications. □

4.4. The connection to dynamical algebra

Having provided the required background on constructive forcing in Sections 4.1–4.3, we are now in the position to harvest the fruits of this machinery. Let A be an arbitrary ring, not presumed to be countable. Let P be an informal argument about A making use of a maximal ideal of A. Under which circumstances can we provide a constructive reading of P?

“If the considered proof is sufficiently uniform (experience shows that it is always the case), the computation obtained as a whole is finite and ends in the desired conclusion”, explain Lombardi and Quitté the scope of the dynamical algebra toolbox for this kind of situation [80, Section XV.6, p. 876]. Using the notion of forcing extensions, we can provide a formal rendition of this important informal insight.

Let $Σ^{'}$ be the signature Σ of Section 4.3, but without the unary relation symbol G and instead with an unary relation symbol $M ↪ \underline{A}$ (to be used as a stand-in for a maximal ideal).

Theorem 4.24.
Let P be a proof
formulated in intuitionistic (perhaps higher-order) logic

over the signature $Σ^{'}$

of a first-order claim not referring to M

making use of the weak maximal ideal condition of Example 4.20 (4,5)
Then the claim asserted by P holds in V.
Proof.
Let $V^{\nabla}$ be the forcing extension generated from the forcing notion of Example 4.3, so that $V^{\nabla}$ contains the generic enumeration of the elements of A. Since A is countable in $V^{\nabla}$ , the iterative maximal ideal construction of Section 1 applies there, resulting in a maximal ideal $m$ of A (or more precisely, $\underline{A}$ ) in $V^{\nabla}$ (⊛). Interpreting P in $V^{\nabla}$ , with the unary relation symbol M interpreted as membership in $m$ , we conclude that the proven claim holds in $V^{\nabla}$ . By Theorem 4.22, it also holds in V. □

The central workhorse of the dynamical algebra approach to maximal ideals is systematic folding of branches obtained by case distinctions along the maximal ideal condition, propagating information from leaves to the root, as reviewed on page 266 or in more detail in [80, Section XV.6]. We regard the maximal ideal $m$ constructed in the proof of Theorem 4.24 as a reification of the dynamical algebra toolbox to maximal ideals – while the latter is a heuristic explanation how to reread proofs involving maximal ideals, the former is an actual maximal ideal (living in a forcing extension). Unwinding all definitions, the central idea of the dynamical approach is recovered as the computational content of the proof of Lemma 1.1(b).

For instance, Theorem 4.24 can be followed in order to generalize the test case analyzed in Proposition 2.6 from countable rings to arbitrary rings. We formalized this approach in Agda (⊛); unwinding the forcing machinery, we roughly obtain the following proof: Proof.
We show, by induction on the number of rows and the number of formal zero entries: For every matrix M over a ring A, if M has more rows than columns and if the induced linear map $A^{m} \to A^{n}$ is surjective, then $1 = 0$ in A.

Let a matrix M with more rows than columns over a ring A be given. If all entries of M are known to be zero (formal zeros), then $1 = 0$ in A because the vector $(1, 0, \dots, 0)$ still belongs to the range of $M = 0$ .

Else let $a_{i j}$ be the first entry not known to be zero. It becomes a formal zero over the quotient ring $A / (a_{i j})$ . Since the matrix M is still surjective over the quotient, the induction hypothesis (applied to the quotient ring) implies $1 = 0$ in $A / (a_{i j})$ . Hence $a_{i j}$ is invertible in A.

By elementary row and column operations, the matrix can be transformed to the form $(\begin{array}{cc} 1 & 0 \\ 0 & M^{'} \end{array})$ , where the induced linear map of the submatrix $M^{'}$ is again surjective. Hence $1 = 0$ by the induction hypothesis (applied to A). □
Notably, this unrolled proof is not the same as the determinant-based proofs of Richman [108, Theorem 1] or Lombardi–Quitté [80, Proposition II-5.2]. Instead, it is more in spirit of the proofs of [108, Theorems 2–4] or of [23], but using auxiliary computations over quotient rings instead of localized rings. This feature is to be expected – localized rings typically appear when unwinding proofs which make use of the generic localization [25, Section 3] as opposed to proofs making use of the iterative maximal ideal construction applied to generic enumeration.

Theorem 4.24 is not the only way to reify the dynamical approach to maximal ideals. Instead of employing the forcing extension containing the generic enumeration, we can also employ the forcing extension of Example 4.4 containing a generic maximal ideal in the strong sense. Since for this alternative forcing notion the assumption for going back and forth – Theorem 4.22 – is not satisfied, its scope is restricted:
Theorem 4.25.
Let P be a proof
formulated in intuitionistic (perhaps higher-order) logic

over the signature $Σ^{'}$

of a first-order claim not referring to M which moreover is a coherent implication

making use of the strong maximal ideal condition of Example 4.21 .
Then the claim asserted by P holds in V.
Proof.
The claim holds in the forcing extension generated by the forcing notion of Example 4.4, with the predicate M interpreted as described in Example 4.21, and passes down to V by Theorem 4.23. □

The restriction in Theorem 4.25 to coherent implications is reminiscient of the same kind of restriction in Barr’s theorem on transforming classical proofs to intuitionistic proofs. Indeed, while the forcing extension generated by Example 4.4 does not yet satisfy the full law of excluded middle, it does have a certain amount of classicality built into it – its maximal ideal satisfies the strong maximal ideal condition.

The ideal $m$ obtained by applying the construction of Section 1 to the generic enumeration of A and the ideal $n$ obtained by directly forcing a strong maximal ideal serve similar purposes. Because they live in different universes, it is not meaningful to ask whether they are equal. However, we may ask whether they satisfy the same first-order statements. They do not: Proposition 4.26.
With the terminology of Proposition 2.5 , Example 4.20 and Example 4.21 , an element $x \in A$ is …
contained in the Jacobson radical if and only if $x \underline{\in} n$ holds in the forcing extension containing the generic maximal ideal.

not apart from the Jacobson radical if and only if $x \underline{\in} m$ holds in the forcing extension containing the generic enumeration.

Proof.
The first statement has been analyzed before, in the language of entailment relations [126, Corollary 2]. One proves by induction that if $\nabla a . x \in a$ , then $x \in Jac (a)$ .

For the “only if” direction of the second claim, arguing in the forcing extension, we assume (as we may) for the sake of contradiction that $1 \in m + (x)$ . Then there is an element $y \in A$ such that $1 - x y$ is an element of $m$ and hence is not invertible. This is a contradiction to x not being apart from the Jacobson radical.

For the “if” direction, let $u \in A$ be arbitrary and assume that $1 - u x$ is not invertible. Then $[1 - u x] ⊧ 1 - u x \underline{i n} m$ . By assumption, $[] ⊧ x \underline{\in} m$ and hence also $[1 - u x] ⊧ x \underline{\in} m$ . Thus $[1 - u x] ⊧ 1 \underline{\in} m$ , a contradiction. □
Remark 4.27.
In addition to maximal ideals, minimal prime ideals are important ingredients for some reduction techniques in classical commutative algebra. For instance, the stalk of a reduced ring at a minimal prime ideal enjoys the good property of being a field. Can the iterative construction of Section 1 be adapted to build a minimal prime ideal, or (equivalently in classical mathematics) a maximal prime filter (a saturated multiplicative subset such that $x + y \in p$ implies $x \in p \lor y \in p$ and such that $0 \in p \Rightarrow 1 = 0$ )?

Given any sequence $p_{0}, p_{1}, \dots$ of prime filters of A, we can indeed explicitly construct a prime filter $q$ which is maximal among the given prime filters, that is which satisfies $q \subseteq p_{n} \Rightarrow q = p_{n}$ , as follows: $\begin{aligned} q : = ⋃ (⋃_{n} S_{n}), \\ where S_{0} : = \emptyset, \\ S_{n + 1} : = S_{n} \cup {p_{n} | S_{n} \cup {p_{n}} is a chain} \end{aligned}$ (A chain is a subset such that for any two elements $p$ and $p^{'}$ , $p \subseteq p^{'}$ or $p^{'} \subseteq p$ .) As the set P of all prime filters of A might not be countable, it is tempting to apply this construction to the generic enumeration of all prime filters of A, in the forcing extension where P is forced to be countable. However, while the passage from the base universe to the forcing extension preserves and reflects first-order logic, the two universes typically differ in their stock of subsets: In the forcing extension, the ring A can catch new prime filters which did not exist in the base universe; the prime filter $q$ will only be maximal with respect to the old prime filters.

That said, if we relax the primality condition in a classically equivalent way, a different iterative procedure can be used to construct a maximal prime filter; see Example 5.3 below. With this construction, we can aspire to decrypt classical proofs in commutative algebra employing minimal prime ideals. Indeed, in this way we reify the dynamical approach to minimal prime ideals [80, Section XV.7]. For instance, the classical proofs of the analog of Proposition 2.6 for injective linear maps and of McCoy’s theorem (for every injective linear map $A^{m} \to A^{n}$ , the ideal of its m-minors is regular) reproduced in [25, Section 3.5] can be interpreted in this framework. Unwinding the resulting constructive proof for the analog of Proposition 2.6, we recover Richman’s proof [108, Theorem 2]; unwinding the resulting constructive proof of McCoy’s theorem, we recover the proof reproduced at [25, p. 174] (but not the Cramer-style proofs of [29], [80, Theorem 5.22] or [79, Exercise 5.23A(3)]).

A substantially different approach to constructivizing minimal prime ideals, directly forcing the existence of the generic maximal prime filter instead of iteratively constructing one after forcing the existence of the generic enumeration, has been explored by Coquand and Lombardi [40, Section 6].

4.5. Further connections

Noetherian conditions. Over the last 30 years, there has been a gradual evolution of Noetherian conditions in the constructive algebra community. Building on early pioneering work of Tennenbaum [139], Richman and Seidenberg proposed the ascending chain condition, referring to ascending sequences of finitely generated ideals [107,132]. There is a variant of Hilbert’s basis theorem for this flavor of Noetherian rings; however, its utility is limited because constructively, such ascending sequences can be rare – for a particularly sequence-poor ring, see [20, Example 2]. The ascending tree condition [109] is an attempt to fix this deficiency; knowing that a ring satisfies this stronger condition gives much more information than the ascending chain condition, and a version of Hilbert’s basis theorem shows that there is still an ample supply of important rings satisfying this condition. There is a further condition which in many cases of interest is even stronger, a wellfoundedness condition attributed to Martin-Löf [68].

Common to all these conditions is that for their corresponding version of Hilbert’s basis theorem, membership in finitely generated ideals needs to be decidable, the ring needs to be coherent, or both. Is there a Noetherian flavor which does not require either of these assumptions?

There is; the inductive condition used by Coquand, Lombardi and Persson [41,42] fits the bill. Appreciating the obstacles which the proofs of Hilbert’s basis theorem for the earlier flavors of Noetherianity had to overcome, the clean proof [42, Corollary 16] for the inductive condition has an almost magical quality to it.

Forcing technology allows us to recognize that with this condition, we have actually come full circle – back to the venerable ascending chain condition:

Theorem 4.28.
A ring is inductively Noetherian [ 36 , 41 , 42 ] if and only if a very particular ascending sequence of finitely generated ideals stalls, namely the generic one.
Proof.
See the forthcoming paper [27]. □

The mystery of nongeometric sequents. Every forcing extension is specifically tailored to support a generic filter of the corresponding forcing notion. Hence it may come as a surprise that, despite not being designed in that way, generic filters tend to have more, and indeed rather peculiar, properties than would be expected just by virtue of being a filter. For instance:

The generic surjection f is not only everywhere-defined, single-valued and surjective as expected, but also has the property that, up to a double negation, every desired finite pattern occurs among its values: In the forcing extension it holds that for every finite list $σ = x_{0} \dots x_{k - 1}$ , it is not not the case that there is a number $n \in N$ such that the values $f (n), f (n + 1), \dots, f (n + k)$ agree with σ.

Localizing a ring at its generic prime filter not only yields a local ring, as expected when localizing at a prime filter, but in fact a ring which is almost a field in the sense that nonunits are nilpotent.

The generic ideal of a given ring is not only an ideal as expected, but also maximal in the sense that nonzero elements of the quotient are already invertible. As far as we know, this observation has not yet been explored at all.

This phenomenon is the mystery of nongeometric sequents. The survey [25, Section 3] presents a range of applications of these unexpected properties, while the paper [24] attempts to explain their origin.
5. Generalization to abstract inconsistency predicates on well-orders

This section generalizes the construction of Section 1 from countable rings to arbitrary countable sets equipped with an abstract inconsistency predicate on their powerset. Abstract inconsistency predicates are a common generalization of predicates such as “the given ideal is improper”, “the given set of vectors is linearly dependent” and “the given set of first-order formulas is inconsistent”; they help to present the central aspects of the construction of Section 1 more tidily. In a second step, we relax the countability assumption to a more general well-foundedness requirement.

5.1. Abstract inconsistency predicates

The notion of inconsistency predicates can be defined in the quite general context of directed-complete lattices as monotone predicates which split directed joins [127]. For our purposes, the level of generality displayed in the following definition is sufficient.

Definition 5.1.
Let X be a set. An inconsistency predicate on X is a predicate $Inc$ on $P (X)$ which
is monotone: if $U \subseteq V$ and $Inc U$ , then $Inc V$ , and

splits directed joins: if $U \subseteq P (X)$ is a directed subset and $Inc (\cup U)$ , then $Inc V$ for some $V \in U$ .

An important example of a directed join is the union of an ascending sequence of subsets: For an inconsistency predicate $Inc$ , if $Inc (⋃_{n \in N} U_{n})$ , then there is a number n such that $Inc U_{n}$ . However, we will also employ directed subsets of the form ${U} \cup {X | φ}$ where φ is a proposition which might not be decidable.10
¹⁰
Directed subsets of this kind, classically trivial but constructively relevant, have also played a role in [127, Lemma 1] and [86, Example I.1.7(2)].

Example 5.2.
Let A be a ring. For any subset $M \subseteq A$ , let $Inc M$ state that $1 \in (M)$ , where $(M)$ is the ideal generated by M. Then $Inc$ is an inconsistency predicate.
Example 5.3.
Let A be a ring. For any subset $M \subseteq A$ , let $Inc M$ state that the multiplicative set generated by M contains 0, that is that some (perhaps empty) product $m_{1} \dots m_{n}$ of elements of M (with repetitions allowed) is zero. Then $Inc$ is an inconsistency predicate.
Example 5.4.
Let M be a module over a ring. For any subset $U \subseteq M$ , let $Inc U$ denote that $(U) = M$ , where $(U)$ is the submodule generated by U. Then $Inc$ is an inconsistency predicate if and only if M is finitely generated.
Example 5.5.
Let X be the set of sentences over some first-order signature. Let $α \in X$ be a fixed sentence. Let $Inc M$ state that M entails α in (minimal, intuitionistic or classical) first-order logic. Then $Inc$ is an inconsistency predicate.
Remark 5.6.
The inconsistency predicates of Examples 5.2, 5.3, 5.4 and 5.5 are all induced by algebraic closure operators as reviewed in [85, Example 1]; in these cases, $Inc U$ is actually defined in terms of the closure of the subset U.

5.2. Maximal consistent extensions

For countable sets equipped with an inconsistency predicate, we have the following generalization of the construction in Section 1.

Construction 5.7.
Let X be a countable set equipped with an inconsistency predicate $Inc$ . Let $x_{0}, x_{1}, \dots$ be an enumeration of X. Let $A_{0} \subseteq X$ be an arbitrary subset. Let “ $\neg φ$ ” mean “ $φ \Rightarrow Inc A_{0}$ ”. Without appealing to any form of choice, we recursively define $\begin{matrix} A_{n + 1} : = A_{n} \cup {x_{n} | \neg Inc (A_{n} \cup {x_{n}})} \end{matrix}$ and set $A : = ⋃_{n \in N} A_{n}$ .
Lemma 5.8 (In the situation of Construction 5.7.).

The set A is equiconsistent with $A_{0}$ : If $Inc A$ , then also $Inc A_{0}$ .

For every number n, the following are equivalent:

(1) $x_{n} \in A_{n + 1}$ . (2) $x_{n} \in A$ . (3) $\neg Inc (A \cup {x_{n}})$ . (4) $\neg Inc (A_{n} \cup {x_{n}})$ .

Proof.
For claim (a), we verify by induction on $n \in N$ that $\neg Inc A_{n}$ . The result then follows because $Inc$ splits the directed join $⋃_{n} A_{n}$ .

The case $n = 0$ is trivial. For the induction step $n \to n + 1$ , assume $Inc A_{n + 1}$ . Since $A_{n + 1} \subseteq A_{n} \cup {x_{n}}$ , we have $Inc (A_{n} \cup {x_{n}})$ by monotonicity. Hence $A_{n + 1} = A_{n} \cup {x_{n} | Inc A_{0}}$ .11
¹¹
If the principle of explosion for $Inc A_{0}$ was available, then this identity would entail $A_{n + 1} = A_{n}$ and thus enable a quick conclusion of the proof.

This identity can be rewritten to render its directed nature more apparent: $\begin{matrix} A_{n + 1} \subseteq ⋃ ({A_{n}} \cup {X | Inc A_{0}}) . \end{matrix}$ As $Inc$ splits direct joins, we obtain $Inc A_{n}$ (and hence $Inc A_{0}$ by the induction hypothesis $\neg Inc A_{n}$ ) or we obtain $Inc A_{0}$ directly.

For claim (b), it is clear that $(3) \Rightarrow (4) \Rightarrow (1) \Rightarrow (2)$ . For $(2) \Rightarrow (3)$ , let $x_{n} \in A$ . If $Inc (A \cup {x_{n}})$ , then $Inc A$ because $A \cup {x_{n}} = A$ and hence $Inc A_{0}$ by part (a). □
Theorem 5.9.
Let X be a countable set equipped with an inconsistency predicate. Then every subset $A_{0}$ of X has an extension $A \supseteq A_{0}$ which is maximal equiconsistent in that for every subset B of X: $\begin{matrix} A \subseteq B \land \neg Inc B ⟹ A = B . \end{matrix}$
Proof.
We verify that A as in Construction 5.7 is as desired. Let $x \in B$ . Then $\neg Inc (A \cup {x})$ , as $Inc (A \cup {x})$ would imply $Inc B$ by monotonicity. Hence $x \in A$ by Lemma 5.8(b). □
Remark 5.10.
If an inconsistency predicate is induced by an algebraic closure operator (Remark 5.6), then every subset is equiconsistent with its closure; whence the maximal equiconsistent extensions provided by Theorem 5.9 are automatically closed under the given operator. For instance, maximal equiconsistent extensions with respect to the inconsistency predicate of Example 5.2 are automatically ideals and extensions with respect to the predicate of Example 5.5 are automatically deductively closed.

Extending the empty subset by Theorem 5.9 has a number of corollaries, such as:
Every countable ring has a maximal ideal (Example 5.2).

Every countable ring has a maximal multiplicatively closed subset not containing zero (Example 5.3). Such a subset S is multiplicatively saturated (closed under divisors) and a prime filter in the weak sense that $x + y \in S$ and $x \notin S$ implies $y \in S$ (where negation means implication to $1 = 0$ as in Section 1). The ring of fractions $A [S^{- 1}]$ has the property that elements which are not nilpotent are invertible. In the case that A is reduced, this ring of fractions is a field in the sense that nonzero elements are invertible. The complement of S is a (certain weak kind of) a minimal prime ideal; in classical reverse mathematics, this iterative construction of a minimal prime ideal is due to Hatzikiriakou [61, Lemma 3.1].

Every finitely generated module over a countable ring has a maximal proper submodule (Example 5.4).

Every countable vector space over a residue field has a maximal linearly independent set (using the inconsistency predicate and the notion of linear independence of [85, Section 6]). Such a set is anonymously spanning in that every vector is not not contained in its span. In this sense countable vector spaces “almost” have a basis.
By extending a given subset instead of the empty one, all these results also admit relative versions. For instance, every submodule U of a finitely generated module over a countable ring can be extended to a maximal submodule $U^{'}$ such that $U^{'} = M \Rightarrow U = M$ . Some corollaries of Theorem 5.9 are usually only stated in their relative form:
Every set of sentences over a countable signature can be completed to a maximal equiconsistent set (Example 5.5); this result is a central ingredient in constructive proofs of Gödel’s completeness theorem [50,63,77].

5.3. The well-founded case

Fundamental to Construction 5.7 is its step-by-step nature, requiring that the elements are presented in a single infinite sequence. If a single such sequence does not suffice to exhaust all elements, it is conceivable to take a limit step and continue sequentially from then on.

Let I be a well-ordering, that is a set equipped with a relation $(<)$ such that constructions by transfinite recursion and proofs by induction are possible. Further assume that I itself and that for every $n \in I$ the set ${k \in I | k < n}$ is conditionally directed: For every two elements of the set, an upper bound is also contained in the set. This requirement is for instance met in case that $(<)$ is a linear order.

Construction 5.11.
Let X be a set equipped with an inconsistency predicate $Inc$ . Let X be an image of I, writing $X = {x_{n} | n \in I}$ . Let “ $\neg φ$ ” mean “ $φ \Rightarrow Inc \emptyset$ ”. Without appealing to any form of choice, we define by transfinite recursion $\begin{matrix} A_{n} : = A_{< n} \cup {x_{n} | \neg Inc (A_{< n} \cup {x_{n}})}, \end{matrix}$ where $A_{< n} : = ⋃_{k < n} A_{k}$ , and set $A : = ⋃_{n \in I} A_{n}$ .
Lemma 5.12 (In the situation of Construction 5.11.).

The set A is consistent: $\neg Inc A$ .

For every index $n \in I$ , the following are equivalent:

(1) $x_{n} \in A_{n}$ . (2) $x_{n} \in A$ . (3) $\neg Inc (A \cup {x_{n}})$ . (4) $\neg Inc (A_{< n} \cup {x_{n}})$ .

Proof.

The proof of Lemma 5.8 carries over almost verbatim. The only part which requires some adaptation is the verification that $\neg Inc A_{n}$ for every index $n \in I$ . This verification now proceeds by transfinite induction.

Assuming that $\neg Inc A_{k}$ for all $k < n$ , we verify that $\neg Inc A_{n}$ . So assume $Inc A_{n}$ . Since $A_{n} \subseteq A_{< n} \cup {x_{n}}$ , we have $Inc (A_{< n} \cup {x_{n}})$ by monotonicity. Thus $A_{n} = A_{< n} \cup {x_{n} | Inc \emptyset}$ and hence $\begin{matrix} A_{n} \subseteq ⋃ ({\emptyset} \cup {A_{k} | k < n} \cup {X | Inc \emptyset}) . \end{matrix}$ Because $Inc$ splits directed joins, we obtain $Inc \emptyset$ (in which case we are done); or $Inc A_{k}$ for some $k < n$ (in which case we are done by the induction hypothesis); or $Inc X$ together with the information that $Inc \emptyset$ (so we are done as well). □

Theorem 5.13.

Let X be a set equipped with an inconsistency predicate. Assume that X is an image of I. Then X contains a maximal consistent subset.

Proof.

As the proof of Theorem 5.9. □

Footnotes

Acknowledgements

The present study was carried out within the project “Reducing complexity in algebra, logic, combinatorics – REDCOM” belonging to the program “Ricerca Scientifica di Eccellenza 2018” of the Fondazione Cariverona and GNSAGA of the INdAM.12

¹²

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

Important steps towards this paper were made during the Dagstuhl Seminar 21472 “Geometric Logic, Constructivisation, and Automated Theorem Proving” in November 2021. This paper would not have come to existence without the authors’ numerous discussions with Daniel Misseleck-Wessel, and greatly benefited from astute comments of Adrian Antz, Karim Becher, Nicolas Daans, Kathrin Gimmi, Matthias Hutzler, Tadeusz Litak, Christian Sattler, Noah Schweber, Lukas Stoll, the three anonymous reviewers of the abridged precursor text to this article [

] and the two reviewers of the present text.

References

Aczel, An introduction to inductive definitions, in: Handbook of Mathematical Logic,

Barwise, ed., Stud. Logic Found. Math., Vol. 90, North-Holland, 1977, pp. 739–782. doi:10.1016/S0049-237X(08)71120-0.

Aczel, The Russell–Prawitz modality, Math. Structures Comput. Sci11(4) (2001), 541–554. doi:10.1017/S0960129501003309.

Aczel and

Rathjen, Constructive Set Theory, 2010, book draft.

Aczel and

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

Apfelmus, The operational monad tutorial, The Monad. Reader15 (2010), 37–56.

Avigad, Forcing in proof theory, Bull. Symbolic Logic10(3) (2004), 305–333. doi:10.2178/bsl/1102022660.

Banaschewski, The power of the ultrafilter theorem, J. London Math. Soc.27(2) (1983), 193–202. doi:10.1112/jlms/s2-27.2.193.

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

Banaschewski and

Erné, On Krull’s separation lemma, Order10 (1993), 253–260. doi:10.1007/BF01110546.

10.

Banaschewski and

Vermeulen, Polynomials and radical ideals, J. Pure Appl. Algebra113(3) (1996), 219–227. doi:10.1016/0022-4049(95)00149-2.

11.

Barr, Toposes without points, J. Pure Appl. Algebra5(3) (1974), 265–280. doi:10.1016/0022-4049(74)90037-1.

12.

Barton, Forcing and the universe of sets: Must we lose insight?, J. Philos. Logic49 (2020), 575–612. doi:10.1007/s10992-019-09530-y.

13.

Bauer, Realizability as the connection between computable and constructive mathematics, 2005, http://math.andrej.com/asset/data/c2c.pdf.

14.

Bauer, Intuitionistic mathematics and realizability in the physical world, in: A Computable Universe,

Zenil, ed., World Scientific Pub Co, 2012.

15.

Bauer, Five stages of accepting constructive mathematics, Bull. AMS54 (2017), 481–498. doi:10.1090/bull/1556.

16.

Becher, Splitting fields of central simple algebras of exponent two, J. Pure Appl. Algebra220 (2016), 3450–3453. doi:10.1016/j.jpaa.2016.04.009.

17.

Bélanger and

J.-P.

Marquis, Menger and Nöbeling on pointless topology, Logic Log. Philos.22(2) (2013), 145–165.

18.

Bell, Set Theory. Boolean-Valued Models and Independence Proofs, Oxford Logic Guides, Oxford University Press, 2005.

19.

Berardi and

Valentini, Krivine’s intuitionistic proof of classical completeness (for countable languages), Ann. Pure Appl. Log.129(1–3) (2004), 93–106. doi:10.1016/j.apal.2004.01.002.

20.

Blass, Well-ordering and induction in intuitionistic logic and topoi, in: Mathematical Logic and Theoretical Computer Science,

Kueker,

Lopez-Escobar and

Smith, eds, Lect. Notes Pure Appl. Math., Vol. 106, 1986, pp. 29–48.

21.

Blass and

Ščedrov, Classifying topoi and finite forcing, J. Pure Appl. Algebra28(2) (1983), 111–140. doi:10.1016/0022-4049(83)90085-3.

22.

Blechschmidt, Using the internal language of toposes in algebraic geometry, PhD thesis, University of Augsburg, 2017.

23.

Blechschmidt, An elementary and constructive proof of Grothendieck’s generic freeness lemma, 2018, https://arxiv.org/abs/1807.01231.

24.

Blechschmidt, A general Nullstellensatz for generalized spaces, 2020, https://rawgit.com/iblech/internal-methods/master/paper-qcoh.pdf.

25.

Blechschmidt, Generalized spaces for constructive algebra, in: Proof and Computation II,

Mainzer,

Schuster and

Schwichtenberg, eds, World Scientific, 2021, pp. 99–187. doi:10.1142/9789811236488_0004.

26.

Blechschmidt, Exploring mathematical objects from custom-tailored mathematical universes, in: Objects, Structures, and Logics: FilMat Studies in the Philosophy of Mathematics,

Oliveri,

Ternullo and

Boscolo, eds, Springer, 2022.

27.

Blechschmidt and

Oldenziel, The topos-theoretic multiverse: A modal approach for computation, 2023.

28.

Blechschmidt and

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

Berger and

Franklin, eds, Lect. Notes Comput. Sci., Springer, 2022, Proceedings, CiE 2022, Swansea, Wales, July 11–15, 2022.

29.

Błocki, An elementary proof of the McCoy theorem, Univ. Iagel. Acta Math.30 (1993), 215–218.

30.

Bonacina and

Wessel, Ribenboim’s order extension theorem from a constructive point of view, Algebra Universalis81(5) (2020).

31.

Borceux, Handbook of Categorical Algebra: Volume 3, Sheaf Theory, Encyclopedia Math. Appl., Cambridge University Press, 1994.

32.

Bridges and

Palmgren, Constructive mathematics, in: The Stanford Encyclopedia of Philosophy,

Zalta, ed., Metaphysics Research Lab, 2018.

33.

Cave,

Ferreira,

Panangaden and

Pientka, Fair reactive programming, in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, 2014, pp. 361–372.

34.

Cederquist and

Coquand, Entailment relations and distributive lattices, in: Logic Colloquium ’98. Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Prague, Czech Republic, August 9–15, 1998,

Buss,

Hájek and

Pudlák, eds, Lect. Notes Logic, Vol. 13, A. K. Peters, 2000, pp. 127–139.

35.

Conrad, Constructing Algebraic Closures, 2021, https://kconrad.math.uconn.edu/blurbs/galoistheory/algclosureshorter.pdf .

36.

Coquand, Notions invariant by change of basis, 2001, https://www.cse.chalmers.se/~coquand/base.ps.

37.

Coquand, About Goodman’s theorem, Ann. Pure Appl. Logic164(4) (2013), 437–442. doi:10.1016/j.apal.2012.10.007.

38.

Coquand, Point-free topology and sheaf models. Slides for the workshop on critical views on infinity, organized by Laura Crosilla, 2021, https://www.cse.chalmers.se/~coquand/potential.pdf.

39.

Coquand and

Lombardi, Hidden constructions in abstract algebra: Krull dimension of distributive lattices and commutative rings, in: Commutative Ring Theory and Applications,

Fontana,

S.-E.

Kabbaj and

Wiegand, eds, Lect Notes Pure Appl. Math., Vol. 231, Addison-Wesley, 2002, pp. 477–499.

40.

Coquand and

Lombardi, A logical approach to abstract algebra, Math. Structures Comput. Sci16(5) (2006), 885–900. doi:10.1017/S0960129506005627.

41.

Coquand and

Lombardi, Krull’s principal ideal theorem, Technical report, 30, Institut Mittag-Leffler, 2000/2001.

42.

Coquand and

Persson, Gröbner bases in type theory, in: TYPES 1998: Types for Proofs and Programs,

Altenkirch,

Reus and

Naraschewski, eds, Lecture Notes in Comput. Sci., Vol. 1657, Springer, 1999, pp. 33–46.

43.

Coste,

Lombardi and

M.-F.

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

44.

Crosilla, Exploring predicativity, in: Proof and Computation,

Mainzer,

Schuster and

Schwichtenberg, eds, World Scientific, 2018, pp. 83–108. doi:10.1142/9789813270947_0003.

45.

Dora,

Dicrescenzo and

Duval, About a new method for computing in algebraic number fields, in: Europ. Conference on Computer Algebra (2), 1985, pp. 289–290.

46.

Erné, A primrose path from Krull to Zorn, Comment. Math. Univ. Carolin.36(1) (1995), 123–126.

47.

Escardó and

Oliva, The Peirce translation and the double negation shift, in: Programs, Proofs, Processes,

Ferreira,

Löwe,

Mayordomo and

Mendes Gomes, eds, Lecture Notes in Comput. Sci., Vol. 6158, Springer, 2010, pp. 151–161. doi:10.1007/978-3-642-13962-8_17.

48.

Ferreira and

Oliva, On various negative translations, in: Proceedings Third International Workshop on Classical Logic and Computation, CL&C 2010, Brno, Czech Republic, 21–22 August 2010,

van Bakel,

Berardi and

Berger, eds, EPTCS, Vol. 47, 2010, pp. 21–33.

49.

Ferreira and

Oliva, On the relation between various negative translations, in: Logic, Construction, Computation,

Berger,

Diener,

Schuster and

Seisenberger, eds, Ontos Math. Log., Vol. 3, De Gruyter, 2012, pp. 227–258.

50.

Forster,

Kirst and

Wehr, Completeness theorems for first-order logic analysed in constructive type theory: Extended version, J. Logic Comput.31 (2021), 112–151. doi:10.1093/logcom/exaa073.

51.

Friedman, The consistency of classical set theory relative to a set theory with intuitionistic logic, J. Symbolic Logic38 (1973), 315–319. doi:10.2307/2272068.

52.

Friedman, Classical and intuitionistically provably recursive functions, in: Higher Set Theory,

Müller and

Scott, eds, LNM, Vol. 669, Springer, 1978, pp. 21–27. doi:10.1007/BFb0103100.

53.

Geschke, Models of Set Theory, 2011, https://www.math.uni-hamburg.de/home/geschke/teaching/ModelsSetTheory.pdf .

54.

Geschke and

Quickert, On Sacks forcing and the Sacks property, in: Classical and New Paradigms of Computation and Their Complexity Hierarchies. Papers of the Conference “Foundations of the Formal Sciences III”,

Löwe,

Piwinger and

Räsch, eds, Trends Log. Stud. Log. Libr., Vol. 23, Springer, 2004, pp. 95–139.

55.

Gilmer, A note on the algebraic closure of a field, Amer. Math. Monthly75(10) (1968), 1101–1102. doi:10.2307/2315743.

56.

Gödel, The consistency of the axiom of choice and of the generalized continuum-hypothesis, Proc. Natl. Acad. Sci. USA24(12) (1938), 556–557. doi:10.1073/pnas.24.12.556.

57.

Goldblatt, Grothendieck topology as geometric modality, MLQ Math. Log. Q.27(31–35) (1981), 495–529. doi:10.1002/malq.19810273104.

58.

Goldblatt, Topoi: The Categorical Analysis of Logic, Stud. Logic Found. Math., Vol. 98, Elsevier, 1984.

59.

Grayson, Forcing in intuitionistic systems without power-set, J. Symbolic Logic48(3) (1983), 670–682. doi:10.2307/2273459.

60.

Hamkins, The set-theoretic multiverse, Rev. Symb. Log.5 (2012), 416–449. doi:10.1017/S1755020311000359.

61.

Hatzikiriakou, Minimal prime ideals and arithmetic comprehension, J. Symbolic Logic56(1) (1991), 67–70. doi:10.2307/2274904.

62.

Henkin, Metamathematical theorems equivalent to the prime ideal theorem for Boolean algebras, Bull. Amer. Math. Soc.60 (1954), 387–388.

63.

Herbelin and

Ilik, An analysis of the constructive content of Henkin’s proof of Gödel’s completeness theorem (draft), 2016.

64.

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

65.

Howard and

Rubin, Consequences of the Axiom of Choice, Math. Surveys Monogr., AMS, 1998.

66.

Hyland, The effective topos, in: The L. E. J. Brouwer Centenary Symposium,

A.S.

Troelstra and

van Dalen, eds, North-Holland, 1982, pp. 165–216.

67.

Ishihara,

Khoussainov and

Nerode, Decidable Kripke models of intuitionistic theories, Ann. Pure Appl. Logic93 (1998), 115–123. doi:10.1016/S0168-0072(97)00057-2.

68.

Jacobsson and

Löfwall, Standard bases for general coefficient rings and a new constructive proof of Hilbert’s basis theorem, J. Symbolic Comput.12(3) (1991), 337–372. doi:10.1016/S0747-7171(08)80154-X.

69.

Jech, Multiple Forcing, Cambridge Tracts in Math., Vol. 88, Oxford University Press, 1987.

70.

Johansson, Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus, Compos. Math.4 (1937), 119–136.

71.

P.T.

Johnstone, Topos Theory, L.M.S. Monographs, Vol. 10, Academic Press, 1977.

72.

P.T.

Johnstone, The point of pointless topology, Bull. AMS8(1) (1983), 41–53. doi:10.1090/S0273-0979-1983-15080-2.

73.

P.T.

Johnstone, The art of pointless thinking: A student’s guide to the category of locales, in: Category Theory at Work (Bremen, 1990), Res. Exp. Math., Heldermann, 1991, pp. 85–107.

74.

P.T.

Johnstone, Sketches of an Elephant: A Topos Theory Compendium, Oxford University Press, 2002.

75.

Joyal and

Tierney, An extension of the Galois theory of Grothendieck, in: Mem. AMS, Vol. 309, AMS, 1984.

76.

Kiselyov and

Ishii, Freer monads, more extensible effects, in: Haskell ’15: Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell, 2015, pp. 94–105. doi:10.1145/2804302.2804319.

77.

J.-L.

Krivine, Une preuve formelle et intuitionniste du théorème de complétude de la logique classique, Bull. Symb. Logic2 (1996), 405–421. doi:10.2307/421172.

78.

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

79.

T.Y.

Lam, Exercises in Modules and Rings, Problem Books in Math., Springer, 2007.

80.

Lombardi and

Quitté, Commutative Algebra: Constructive Methods, Springer, 2015.

81.

Lorenzen, Algebraische und logistische Untersuchungen über freie Verbände, Vol. 16, 1951, pp. 81–106, English translation available [89].

82.

Maietti, Joyal’s arithmetic universes as list-arithmetic pretoposes, Theory Appl. Categ.23(3) (2010), 39–83.

83.

Mannaa and

Coquand, A sheaf model of the algebraic closure, in: Proc. of the Fifth International Workshop on Classical Logic and Computation, 2014.

84.

Mines,

Richman and

Ruitenburg, A Course in Constructive Algebra, Universitext, Springer, 1988.

85.

Misselbeck-Wessel and

Schuster, Radical theory of Scott-open filters, Theoret. Comput. Sci.945 (2023), 113677.

86.

Moerdijk and

Vermeulen, Proper maps of toposes, in: Mem. Amer. Math. Soc., Vol. 705, AMS, 2000.

87.

Moore, The Method of Forcing, 2019, https://arxiv.org/abs/1902.03235 .

88.

Murthy, Classical proofs as programs: How, what and why, in: Constructivity in Comp. Science,

Myers and

O’Donnell, eds, Springer, 1992, pp. 71–88. doi:10.1007/BFb0021084.

89.

Neuwirth, Algebraic and logistic investigations on free lattices, 2017, English translation of [81], https://arxiv.org/abs/1710.08138.

90.

Neuwirth, Lorenzen’s reshaping of Krull’s Fundamentalsatz for integral domains (1938–1953), in: Paul Lorenzen: Mathematician and Logician,

Heinzmann and

Wolters , eds, Log. Epistemol. Unity Sci., Vol. 51, Springer, 2021, pp. 143–183.

91.

Palmgren, Constructive sheaf semantics, Math. Log. Quart.43 (1997), 321–327. doi:10.1002/malq.19970430304.

92.

Paykin,

Krishnaswami and

Zdancewic, The essence of event-driven programming, 2016, https://jpaykin.github.io/papers/pkz_CONCUR_2016.pdf.

93.

Penelope and

Meadows, A reconstruction of Steel’s multiverse project, Bull. Symb. Logic26(2) (2020), 118–169. doi:10.1017/bsl.2020.5.

94.

Perdry, Strongly Noetherian rings and constructive ideal theory, J. Symbolic Comput.37(4) (2004), 511–535. doi:10.1016/j.jsc.2003.02.001.

95.

Perdry, Lazy bases: A minimalist constructive theory of Noetherian rings, MLQ Math. Log. Q.54(1) (2008), 70–82. doi:10.1002/malq.200710042.

96.

Perdry and

Schuster, Noetherian orders, Math. Structures in Comput. Sci.21(1) (2011), 111–124. doi:10.1017/S0960129510000460.

97.

Persson, An application of the constructive spectrum of a ring, in: Type Theory and the Integrated Logic of Programs, Chalmers Univ., Univ. of Gothenburg, 1999.

98.

Pfenning and

Davies, A judgmental reconstruction of modal logic, Math. Structures Comput. Sci.11(4) (2001), 511–540. doi:10.1017/S0960129501003322.

99.

Phoa, An introduction to fibrations, topos theory, the effective topos and modest sets, Technical report, University of Edinburgh, 1992.

100.

Picado and

Pultr, Frames and Locales. Topology Without Points, Front. Math., Birkhäuser, 2012.

101.

Pohst and

Zassenhaus, Algorithmic Algebraic Number Theory, Encyclopedia Math. Appl., Cambridge University Press, 1989.

102.

Poincaré, La logique de l’infini, Rev. méta. et mor.17 (1909), 461–482.

103.

Powell, On the computational content of Zorn’s lemma, in: LICS ’20, ACM, 2020, pp. 768–781. doi:10.1145/3373718.3394745.

104.

Powell,

Schuster and

Wiesnet, A universal algorithm for Krull’s theorem, Information and Computation (2021).

105.

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, 2005, chapter 16.

106.

Renardel de Lavalette, Extended bar induction in applicative theories, Ann. Pure Appl. Logic50(2) (1990), 139–189. doi:10.1016/0168-0072(90)90047-6.

107.

Richman, Constructive aspects of Noetherian rings, Proc. AMS44(2) (1974), 436–441. doi:10.1090/S0002-9939-1974-0416874-9.

108.

Richman, Nontrivial uses of trivial rings, Proc. AMS103 (1988), 1012–1014. doi:10.1090/S0002-9939-1988-0954974-5.

109.

Richman, The ascending tree condition: Constructive algebra without choice, Comm. Algebra31(4) (2003), 1993–2002. doi:10.1081/AGB-120018518.

110.

Richman, A theorem of Gilmer and the canonical universal splitting ring, Comm. Alg.6(1) (2014), 101–108.

111.

Rinaldi and

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

112.

Rinaldi,

Schuster and

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

113.

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.

114.

Rinaldi and

Wessel, Cut elimination for entailment relations, Arch. Math. Logic58 (2019), 605–625. doi:10.1007/s00153-018-0653-0.

115.

Roberts, Class forcing and topos theory, Technical report, The University of Adelaide, 2018.

116.

Roitman, The uses of set theory, Math. Intelligencer14(1) (1992), 63–69. doi:10.1007/BF03024144.

117.

Sato, Forcing for hat inductive definitions in arithmetic, Math. Log. Quart.60(4–5) (2004), 314–318.

118.

Ščedrov, Forcing and classifying topoi, in: Mem. Amer. Math. Soc., Vol. 48, AMS, 1985.

119.

Schilhan, Forcing and applications on bounding, splitting and almost disjointness, Bachelor’s thesis, at the Universität Wien, 2016.

120.

Schoenfield, The problem of predicativity, in: Essays on the Foundations of Mathematics,

Bar-Hillel,

Poznanski,

Rabin and

Robinson, eds, Magnes, 1961, pp. 132–139.

121.

Schuster, Induction in algebra: A first case study, in: LICS ’12, ACM, 2012, pp. 581–585.

122.

Schuster, Induction in algebra: A first case study, Log. Methods Comput. Sci.9(3:20) (2013), 1–19.

123.

Schuster and

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

124.

Schuster and

Wessel, Resolving finite indeterminacy: A definitive constructive universal prime ideal theorem, in: LICS ’20, ACM, 2020, pp. 820–830. doi:10.1145/3373718.3394777.

125.

Schuster and

Wessel, The computational significance of Hausdorff’s maximal chain principle, in: CiE ’20, Lecture Notes in Comput. Sci., 2020.

126.

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, 2021, pp. 77–102.

127.

Schuster and

Wessel, The Jacobson radical for an inconsistency predicate, Computability11(2) (2022), 147–162. doi:10.3233/COM-210365.

128.

Schuster,

Wessel and

Yengui, Dynamic evaluation of integrity and the computational content of Krull’s lemma, J. Pure Appl. Algebra226(1) (2022).

129.

Schuster and

Zappe, Do Noetherian rings have Noetherian basis functions? in: Logical Approaches to Computational Barriers. Second Conference on Computability in Europe, CiE 2006, Swansea, UK, July 2006,

Beckmann,

Berger,

Löwe and

Tucker, eds, Lect. Notes Comput. Sci., Vol. 3988, Springer, 2006, pp. 481–489.

130.

Scott, Prime ideal theorems for rings, lattices, and Boolean algebras, Bull. Amer. Math. Soc.60(4) (1954), 390.

131.

Scott, Completeness and axiomatizability in many-valued logic, in: Proceedings of the Tarski Symposium (Proc. Sympos. Pure Math., Vol. XXV, Univ. California, Berkeley, Calif., 1971),

Henkin,

Addison,

Chang,

Craig,

Scott and

Vaught, eds, AMS, 1974, pp. 411–435. doi:10.1090/pspum/025/0363802.

132.

Seidenberg, What is Noetherian?, Rend. Sem. Mat. Fis. Milano44 (1974), 55–61. doi:10.1007/BF02925651.

133.

Simpson, Subsystems of Second Order Arithmetic, Springer, 1999.

134.

Streicher, Introduction to Category Theory and Categorical Logic, 2004, https://www.mathematik.tu-darmstadt.de/~streicher/CTCL.pdf .

135.

Streicher, Forcing for IZF in sheaf toposes, Georgian Math. J.16(1) (2009), 203–209. doi:10.1515/GMJ.2009.203.

136.

Suslin, On the structure of the special linear group over polynomial rings, Izv. Akad. Nauk SSSR Ser. Mat.41 (1977), 235–252.

137.

Swierstra, Data types à la carte, J. Funct. Programming18 (2008), 423–436. doi:10.1017/S0956796808006758.

138.

Tarski, Fundamentale Begriffe der Methodologie der deduktiven Wissenschaften. I, Monatsh. Math. Phys.37 (1930), 361–404. doi:10.1007/BF01696782.

139.

Tennenbaum, A constructive version of Hilbert’s basis theorem, PhD thesis, University of California, 1973.

140.

Tierney, Forcing topologies and classifying topoi, in: Algebra, Topology, and Category Theory,

Heller and

Tierney, eds, Academic Press, 1976, pp. 211–219. doi:10.1016/B978-0-12-339050-9.50021-3.

141.

van Dalen, Logic and Structure, Universitext, Springer, 2004.

142.

van Oosten, Realizability: An Introduction to Its Categorical Side, Stud. Logic Found. Math., Vol. 152, Elsevier, 2008.

143.

Veldman and

Bezem, Ramsey’s theorem and the pigeonhole principle in intuitionistic mathematics, J. Lond. Math. Soc. (2)47 (1993), 193–211. doi:10.1112/jlms/s2-47.2.193.

144.

Vickers, Locales and toposes as spaces, in: Handbook of Spatial Logics,

Aiello,

Pratt-Hartmann and

van Benthem, eds, Springer, 2007, pp. 429–496. doi:10.1007/978-1-4020-5587-4_8.

145.

Vickers, Continuity and geometric logic, J. Appl. Log.12(1) (2014), 14–27. doi:10.1016/j.jal.2013.07.004.

146.

Vickers, Sketches for arithmetic universes, J. Log. Anal.11(FT4) (2016), 1–56.

147.

Weaver, Forcing for Mathematicians, World Scientific, 2014.

148.

Wessel, Points, ideals, and geometric sequents, Technical report, University of Verona, 2018.

149.

Wessel, Ordering groups constructively, Comm. Alg.47(12) (2019), 4853–4873. doi:10.1080/00927872.2018.1477947.

150.

Wessel, A note on connected reduced rings, J. Comm. Alg.13(4) (2021), 583–588.

151.

Yamamoto, Toposes from forcing for intuitionistic ZF with atoms, 2017, https://arxiv.org/abs/1702.03399.

152.

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

153.

Yengui, Constructive Commutative Algebra. Projective Modules over Polynomial Rings and Dynamical Gröbner Bases, LNM, Vol. 2138, Springer, 2015.

Reifying dynamical algebra: Maximal ideals in countable rings,constructively

Abstract

Keywords

0.1. Extraction of computational content

1. An iterative construction of maximal ideals

Lemma 1.1 (⊛).

Lemma 1.9 (⊛).

1.3. Generalization to the subcountable case

1.4. Interaction with Noetherian hypotheses

2. On the intersection of all prime ideals

Proof. Because x is not nilpotent, the notions of an x-prime ideal and an ordinary prime ideal coincide. Hence the claim follows from Lemma 2.1. □ Theorem 2.3 (Krull’s separation lemma).

Lemma 3.1 (In the setting of Section 1.2.).

Definition 4.1 ([75, p. 24], ⊛).

Definition 4.2 (⊛).

Example 4.3 (⊛).

Proof. By induction. In computational terms, we inspect a given witness of P | σ and descend into it, using the assumption that every covering is inhabited in order to pick out branches. □ Example 4.13 (⊛).

Lemma 4.17 (⊛).

Proof. Omitted. In the language of toposes, the assumption on L ensures that the canonical geometric morphism V ∇ → V is surjective. Pullback along surjective morphisms preserves and reflects the interpretation of coherent implications. □ 4.4. The connection to dynamical algebra

5.1. Abstract inconsistency predicates

Footnotes

Acknowledgements

References

Proof.
Because x is not nilpotent, the notions of an x-prime ideal and an ordinary prime ideal coincide. Hence the claim follows from Lemma 2.1. □
Theorem 2.3 (Krull’s separation lemma).

Proof.
By induction. In computational terms, we inspect a given witness of $P | σ$ and descend into it, using the assumption that every covering is inhabited in order to pick out branches. □
Example 4.13 (⊛).

Proof.
Omitted. In the language of toposes, the assumption on L ensures that the canonical geometric morphism $V^{\nabla} \to V$ is surjective. Pullback along surjective morphisms preserves and reflects the interpretation of coherent implications. □

4.4. The connection to dynamical algebra