These definitions are largely from pages 92-93 of Ingo's notes. All rings are commutative with 1. I'm interested in understanding the extent to which discussion of Noetherian rings can be carried over into constructive settings. Consider a standard definition of a Noetherian ring:
A ring $R$ is Noetherian if for every ascending chain of ideals stabilizes; given $I_1 \subseteq I_2 \subseteq \dotsi$, there exists $n$ so that $I_n = I_m$ for all $m \ge n$.
This definition is constructively untenable; the claim that $\mathbb Z$ (or even $\mathbb Z / n \mathbb Z$) is Noetherian implies LPO. This definition will also run into problems if dependent choice fails. We can solve the issue with dependent choice by introducing ascending processes.
Let $M = (M,\preceq)$ be a poset. An ascending process $(S_n)$ with values in $M$ is a sequence $S_0,S_1,S_2,\dotsc$ of inhabited subsets of $M$, such that for each $x \in S_i$, there exists $y \in S_{i+1}$ so that $x \preceq y$. $(S_n)$ is said to halt if $S_n \cap S_{n+1}$ is inhabited for some $n$. We say that $M$ satisfies the ascending process condition of every ascending process with values in $M$ halts. We say that $M$ satisfies the weak ascending chain condition if for every every ascending chain $(x_i)$, we have $x_{i+1} \preceq x_i$ for some $i$.
We say that $R$ is Process-Noetherian if the poset of finitely generated ideals in $R$ satisfies the ascending process condition.
Let $R$ be a ring. Let $M \subseteq \mathcal P(R)$ be the poset of ideals, and let $M_F \subseteq M$ be the poset of finitely generated ideals. Assuming dependent choice and excluded middle, the following candidate definitions of Noetherianity are easily shown to be equivalent:
- $M = M_F$
- $M$ satisfies the weak ascending chain condition
- $M_F$ satisfies the weak ascending chain condition
- $M$ satisfies the ascending process condition
- $M_F$ satisfies the ascending process condition ($R$ is process-Noetherian)
- For every sequence $(x_i)_{i \ge 1}$ of elements of $R$, there exists $n \ge 0$ so that $x_{n+1} \in (x_1,\dotsc,x_n)$.
If excluded middle fails, then properties $1,2,4$ all fail when $R = \mathbb Z$, and so are completely hopeless. We have $5 \Rightarrow 3 \Rightarrow 6$ unconditionally, and it doesn't seem reasonable to expect that $3 \Rightarrow 5$ without dependent choice, and so $3$ and $6$ seem unlikely work in the absence of dependent choice.
Question 1: Is the implication $3 \Rightarrow 6$ reversible? What if we assume dependent choice? Question 2: Can we constructively prove the analogue of Hilbert's basis theorem using any of the three not-completely-hopeless definitions? What changes if we assume dependent choice?
