Artin Jacobson-semisimple rings are semisimple. Constructively, too?

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"?

-
Not to be nitpicky, but (here begins nitpickiness) in your definition of left and right Artinian, you need $I_n = I_{n+1}$ for all $n \ge M$ for some $M$. –  MTS Mar 8 '11 at 21:26
I'm just curious, by "classical artinianity" do you mean the condition that every set of left ideals has a minimal element? –  Manny Reyes Mar 8 '11 at 21:46
By "classical Artinianity" I mean what MTS has written. Constructively it is a FAR too strong condition (not even the field with two elements is constructively classically Artinian, because this would solve the halting problem). –  darij grinberg Mar 8 '11 at 21:54
So you really want to work with the above definition of artinian, which is not the usual one at first sight? By the way I've deleted the tag "von Neumann algebras" since they are special $C^*$-algebras completely unrelated to von Neumann regular rings. –  Martin Brandenburg Mar 8 '11 at 23:08
Yes, I want to work with my definition of Artinian - unless somebody gives me a better one (which I hope). The usual one is utterly useless in constructive mathematics. –  darij grinberg Mar 8 '11 at 23:15