Basis for the equational identities of the algebraic structure $(\mathbb{R};-,abs)$

Question

Consider the algebraic structure $(\mathbb{R};-,abs)$, where $-$ is the additive inverse unary function, and $abs$ is the absolute value function. What is a basis for the equational identities of that structure? I conjecture that just these three identities are sufficient: $--x=x$, $abs(abs(x))=abs(x)$, and $abs(-x)=abs(x)$. Are those enough, or do we need more?

Answer 1

Any composition $f_1 \circ f_2 \circ … \circ f_n$ where each $f_i$ is either $-x$ (negation) or $|x|$ (absolute value) can be reduced to one of $x, -x, |x|,$ or $-|x|$ using only the three identities (namely, negation is an involution and the absolute value is idempotent and even).

First, since the absolute value is idempotent and even, if any of the $f_i$s are the absolute value, one could get rid of all the following $f_j$s without changing the resulting composite function.

Following that, either all of the $f_i$s are negation or all but the last one are negation and the last one is the absolute value. Using the involution property of negation, one could get rid of each pair of consecutive negations, leaving at most one negation.

In the end, one is left with just $x, -x, |x|,$ or $-|x|$, none of which are equal for all $x$.

So yes, the three given equational identities are enough to generate all equational identities in the structure $(\mathbb{R}, -x, |x|)$.