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 $\operatorname{Ra}R$ of a ring $R$ is defined by one of the following equivalent definitions:
$\operatorname{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$;
$\operatorname{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$;
$\operatorname{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$;
$\operatorname{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$;
$\operatorname{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$;
$\operatorname{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$;
$\operatorname{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 $\operatorname{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 $\operatorname{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"? Given the definition of "Artinian" above, I am not sure if $\mathbb F_2$ is Artinian, because I could take a sequence $S_0,S_1,S_2,...$ of independent statements which are independent of each other too (is this possible?) and then let $I_n$ be the ideal containing $1$ if $S_0, S_1, ..., S_{n-1}$ hold. So let me pose a different question, which is actually interesting without relying on constructivity:
Concrete question. Let $R$ be a ring with $\operatorname{Ra} R = 0$. Assume that, for every $r \in R$, there exists an $n \in \mathbb{N}$ and a $y \in R$ such that $r^n = r^{n+1} y$. Also assume that, for every $r \in R$, there exists an $n \in \mathbb{N}$ and a $y \in R$ such that $r^n = y r^{n+1}$. Must $R$ then be von Neumann regular?
Notice that this is NOT a constructive translation of the classical theorem. It is a stronger conjecture which has the advantage of not requiring a constructive translation to begin with.
