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 $\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.
 A: The question has been changed, so I'm submitting a second answer.
The answer to the new concrete question is no.  Your question boils down to whether there exists a semi-primitive strongly $\pi$-regular ring which is not von Neumann regular.  The answer is yes.  For instance, you can use the subring of $\prod_{\omega}\mathbb{M}_2(\mathbb{F}_2)$ consisting of sequences of matrices which are eventually stable (meaning the matrices stop changing after some point) and eventually upper-triangular.
By the way, suppose we revert back to the original question of whether it is possible to find a constructive proof that left/right artinian and semiprimitivity implies v.N. regularity, and we also assume that semiprimitivity gives us an oracle such that for every element $r\in R$ it gives us $s\in S$ such that $1-rs$ is not invertible.  Using a construction similar to this one, I believe I can show that we cannot prove v.N. regularity (essentially because of the example above).
A: I'm not as familiar with constructive proofs, so this "answer" is really just a couple questions.
Consider the ring $R=\mathbb{M}_2(\mathbb{F}_2)$, and the element $r=\begin{pmatrix} 0 & 1\\ 0 & 0\end{pmatrix}$.  Let's treat $r$ as the input in our algorithm.  Without appealing to the semiprimitivity or artinian conditions, the only constructable elements are integer polynomials in $r$.  (Is this correct?)  Thus, we have access to $0,1,r,1+r$, and nothing else (since $2=0$ and $r^2=0$; although we do know these two equalities).
The left ideals generated by these elements are $(0)\subsetneq Rr\subsetneq R$, and the right ideals are $(0)\subsetneq rR\subsetneq R$ (and these containments are provable with what we constructively know).  Thus, appealing the the left and right artinian conditions will not yield anything.
The element $r$ is nilpotent.  Since the Jacobson radical is zero, we know that some multiple of $r$ must not be nilpotent.  But do we have access to any constructible element $s$ such that $rs$ is not nilpotent?  What kind of elements does a zero Jacobson radical hypothesis allow us claim existence for?
