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?