Notation. When I say "ring", I mean "ring with unity" (not necessarily commutative).

Definition. A ring $R$ is said to be left-Artinian if for every sequence $I_0\supseteq I_1\supseteq I_2\supseteq I_3\supseteq ...$ of left ideals of $R$, there exists an $n\in\mathbb N$ such that $I_n=I_{n+1}$.

Definition. A ring $R$ is said to be right-Artinian if for every sequence $I_0\supseteq I_1\supseteq I_2\supseteq I_3\supseteq ...$ of right ideals of $R$, there exists an $n\in\mathbb N$ such that $I_n=I_{n+1}$.

Definition. A ring $R$ is said to be Artinian if it is both left-Artinian and right-Artinian.

Definition. The Jacobson radical $\mathrm{Ra}R$ of a ring $R$ is defined by one of the following equivalent definitions:

$\mathrm{Ra}R = \left\lbrace r\in R\mid \text{for every }s\in R\text{, the element }1-rs\text{ of }R\text{ is invertible}\right\rbrace$;

$\mathrm{Ra}R = \left\lbrace r\in R\mid \text{for every }s\in R\text{, the element }1-sr\text{ of }R\text{ is invertible}\right\rbrace$;

$\mathrm{Ra}R = \left\lbrace r\in R\mid \text{for every }\left(s,t\right)\in R^2\text{, the element }1-srt\text{ of }R\text{ is invertible}\right\rbrace$;

$\mathrm{Ra}R = \left\lbrace r\in R\mid \text{every right ideal }I\text{ of }R\text{ satisfying }I+rR=R\text{ satisfies }I=R\right\rbrace$;

$\mathrm{Ra}R = \left\lbrace r\in R\mid \text{every left ideal }I\text{ of }R\text{ satisfying }I+Rr=R\text{ satisfies }I=R\right\rbrace$;

$\mathrm{Ra}R = \left\lbrace r\in R\mid \text{every f.g. right }R\text{-module }M\text{ satisfying }MrR=M\text{ satisfies }M=0\right\rbrace$;

$\mathrm{Ra}R = \left\lbrace r\in R\mid \text{every f.g. left }R\text{-module }M\text{ satisfying }RrM=M\text{ satisfies }M=0\right\rbrace$

(where "f.g." means "finitely generated"). (Note that the equivalences are constructive; I have written up the proofs in German a while ago (search for "Jacobson-Radikal") and will translate when I have the time.)

Definition. A ring $R$ is said to be von Neumann regular if for every $r\in R$, there exists some $x\in R$ such that $rxr=r$.

Question: Can we constructively prove that every Artinian ring $R$ satisfying $\mathrm{Ra}R=0$ is von Neumann regular? (This is proven classically using the AC in Lam, "A first course in noncommutative rings", Theorem (4.14) + Corollary (4.24).)

Normally, theorems in algebra can be proved constructively if we know a classical proof. There are methods for this (scindage a la Lombardi; dynamic proofs; Gödel-Gentzen etc.). Unfortunately, whenever chain conditions (such as Artinianity) are involved, these methods break down. The constructive Artinian condition is neither easy to use nor easy to satisfy, so I am not completely sure whether the question is the right one to ask - but I don't know of a better one.

While constructive Artinianity is far less useful than classical Artinianity, it can still be applied to chains of ideals such as $R\supseteq rR\supseteq r^2R\supseteq r^3R\supseteq ...$ to conclude that for every $r\in R$ there exists some $n\in\mathbb N$ and some $y\in R$ such that $r^n=r^{n+1}y$. This can then be juggled with (for example, we can conclude that $r^n=r^ayr^b$ for any two nonnegative integers $a$ and $b$ with $a+b=n+1$; here we use $\mathrm{Ra}R=0$). This is, at the moment, my main reason to believe that the Question above has a positive answer (we mainly have to bring the $n$ down to $1$). But, as I said, I am far from sure about this.

Meta-question: What is the (morally) right constructive analogue of the notions "Artinian" and "Noetherian"?