Is the equational theory of commutative vN regular rings decidable? I wanted to check whether $A(x,y):=\frac{xy}{x+y}$ is an associative operation in every commutative vN regular ring. Now $A(-1,A(1,1))=A(-1,\frac{1}{2})=1\neq 0 =A(0,1)=A(A(-1,1),1)$. On the other hand, $\frac{xy}{x+y}=\frac{1}{1/x+1/y}$, hence $A(x,A(y,z))=\frac{1}{1/x+1/y+1/z}=A(A(x,y),z)$. I soon realized that $\frac{xy}{x+y}=\frac{1}{(y/y)/x+(x/x)/y}\neq\frac{1}{1/x+1/y}$.
This made me wonder whether equality is decidable in principle for this sort of term expressions. So I browsed a list information about classes of mathematical structures for a summary of the properties of commutative regular rings, but the equational theory field was left empty for this structure. (I guess the reason is that the generalized inverse operation $^{-1}$ should have been part of the signature, otherwise the meaning of this field is ambiguous.) Because this structure is a variety (=equational class, here I assume that $^{-1}$ is part of the signature), if two terms are equal, then this can be proved by term rewriting. If two terms are not equal, then this should be provable by substituting specific values from a specific commutative vN regular ring, for which the two terms evaluate to different values. It is easy to see that this commutative ring can always be chosen to be a field. If a finite field would always be enough, then the equational theory of commutative vN regular rings should be decidable.

Is there any reason why a finite field should not be enough for proving inequality?
  Is there any "much simpler" way to see that the equational theory is decidable?


Edit There was some confusion regarding the generalized inverse operation $^{-1}$ in the comments. Similar to groups, neither $1$ nor $^{-1}$ are needed in the signature to define commutative vN regular rings by first-order axioms. But when talking about the equational theory, it certainly makes a difference whether they are included or not. Both groups and commutative vN regular rings can be treated as varieties, because suitable signatures and defining equations are well known and easy to prove. (For commutative vN regular rings, the ring is an inverse semigroup under multiplication, hence adding $^{-1}$ to the signature and $xx^{-1}x=x$ and $x^{-1}xx^{-1}=x^{-1}$ to the equations of commutative rings is enough.) But to make things confusing, (non-commutative) vN regular rings cannot be treated as varieties, because the inverse element need not be unique, and hence the identity $xx^{-1}y^{-1}y=y^{-1}yxx^{-1}$ may fail (this identity would hold if all inverse elements were unique).
 A: Emil Jeřábek's comment explains how to prove that the equational theory of commutative vN regular rings decidable:

I know nothing about von Neumann regular rings, however such an identity (or any quantifier-free formula for that matter) fails in a field iff it fails in an algebraically closed field (by embedding in algebraic closure) iff it fails in an a.c.f. of finite characteristic (due to the compactness theorem) iff it fails in some $\tilde{\mathbb F}_p$ (as all a.c.f. of the same characteristic are elementarily equivalent) iff it fails in a finite field (as every finitely generated subfield of $\tilde{\mathbb F}_p$ is finite). You only need the first step anyway as the theory of a.c.f. is decidable.

Jan Bergstra (see "meadows", also mentioned by Emil Jeřábek in a comment) told me that Komori in "Free algebras over all fields and pseudo-fields" and Ono in "Equational theories and universal theories of fields" proved that the equational theory of commutative regular rings is decidable. This is theorem 4.3 in Ono (which uses similar ideas as in Emil's comment). I haven't accessed Komori's paper, but Ono's paper confirms that Komori's paper also contains a proof of this fact.

Regarding the confusion about the inverse operation $^{-1}$ and treating commutative regular rings as a variety (equational class), I collected some (related) elementary facts together with complete proofs in a pdf document and a related blog-post Algebraic characterizations of inverse semigroups and strongly regular rings.
