Set of generating equations for subtraction. Consider the algebraic structure $(\mathbb{R}, -)$. Is there a finite generating set of equations for subtraction, and if so, can someone exhibit a list of equations.
 A: I will write down a finite basis for the identities of the structure $\langle \mathbb R; -\rangle$. Each of these identities is meant to be universally quantified. (Instead of writing $x-y$ I will write $s(x,y)$.)

* $s(x,x)=s(y,y)$

* $s(s(x,y),s(u,v))=s(s(x,u),s(y,v))$

* $s(x,s(y,y))=x$

* $s(x,s(x,y))=y$

For an abelian group $\langle A; +, -, 0\rangle$, call $\langle A; -\rangle$
the associated subtraction structure. Since $\langle \mathbb R; +,-,0\rangle$ has free abelian subgroups of all finite ranks,  $\langle \mathbb R; -\rangle$ has free subtraction structures of all ranks. Therefore the equational theory of $\langle \mathbb R; -\rangle$ is the same as the equational theory of all subtraction structures of abelian groups. It is clear that the four axioms I gave hold in this class. Thus it suffices to explain why any structure satisfying the axioms is the subtraction structure of some abelian group.
Let $\langle X; s(x,y)\rangle$ be a set equipped with a binary operation satisfying the four axioms. The second axiom says that $s(x,y)$ commutes with itself. The 3rd and 4rth say that $m(x,y,z)=s(x,s(y,z))$ is a Maltsev operation on $X$. The Maltsev operation must also commute with itself. It is known that a Maltsev operation that commutes with itself on a set $X$ must equal $x-y+z$ for some uniquely determined abelian group structure on $X$. That is, there exist some abelian group structure on $X$, say $\langle X; +, -, 0\rangle$, such that $m(x,y,z)=x-y+z$. But now $s(x,y)=m(x,y,s(z,z))=x-y$, so the given operation $s$ agrees with the subtraction of the abelian group. The argument shows that any $s$ satisfying the four axioms agrees with the subtraction operation of some abelian group, which is all we needed to show.
