A finite axiomatization of the universal theory of rings in the signature $(+,*,0,1)$ Let $T$ be the theory of rings in the signature $(+,*,0,1)$, and let $T_\forall$ be the $\forall$-theory of rings in the signature $(+,*,0,1)$. My question is, is $T_\forall$ finitely axiomatizable? And if so, can someone exhibit a finite set of axioms?
 A: $T_\forall$ is the theory of cancellative semirings. This theory is axiomatized by:

*

*The commutative monoid axioms for $+$ and $0$.

*The monoid axioms for $*$ and $1$.

*The left and right distributive laws.

*$0$ is absorptive: $\forall x\, (x*0 = 0 = 0*x)$.

*Cancellativity: $\forall x,y,z\,(x+z = y+z\rightarrow x = y)$.

Note that 4 is redundant: $0 + x*0 = x*(0+0) = x*0 + x*0$, so $0 = x*0$, and similarly for $0 = 0*x$. But I've included 4 because 1-4 axiomatize the class of semirings,  and 4 is not redundant if we don't assume cancellativity (see here).
These universal axioms are true of rings, so every substructure of a ring in the signature $(+,*,0,1)$ is a cancellative semiring. Conversely, if $R$ is a semiring, there is a natural additive monoid homomorphism $h\colon R\to G(R)$, where $G(R)$ is the Grothendieck group of the monoid $(R,+,0)$. The multiplication on $R$ extends to $G(R)$, turning $G(R)$ into a ring and $h$ into a semiring homomorphism. If $R$ is cancellative, then $h$ is an embedding. So every cancellative semiring is a substructure of a ring.
