An "almost" metric via a generalized definition of absolute values

Question

I tried to analyse the properties of $\mathbb R$ that allow us to define the absolute valuation on it, namely $$x\mapsto |x|\text.$$

I realised that the only relevant properties of $\mathbb R$ here are that it is an ordered abelian group, by which I mean an abelian group $(G, +)$ such that $x < y\implies x + z < y + z$. On such a $G$, I can define $|\cdot|$ in the exactly same manner: $$ |x| := \begin{cases} x, & x\ge 0\\ -x, & x < 0 \end{cases}\text. $$

Then the standard properties of $|\cdot|$ are easily proven:

1. Positive definiteness
2. Preservation under negation
3. Triangle inequality.

Now we can define $$ d(x, y) := |x - y|\text.$$

Then it just "begs" to be considered as a metric—the only thing being violated being the requirement that $d(x, y)\in[0, 1)_\mathbb R$.

This motivated me that $[0, +\infty)_G$ (the set of all non-negatives of $G$) could as well be used in place of the usual $[0, \infty)_\mathbb R$ in the definition of metric on sets, and possibly many other places.

Is there a part of math that addresses this kind of questions? Is there something interesting that has been done in this direction?

---

PS: Is MathOverflow better suited for such a question?

Answer 1

If you stare at the metric space axioms carefully you can see exactly what is being used about $[0, \infty)$ that allows us to state them: all we need is the operation $+$ and the order $\le$. So we can actually state the metric space axioms for a metric taking values in a partially ordered monoid; there is actually no need to require the operation to be commutative, nor is there a need to require that the order be total, nor is there a need to require that the monoid be embeddable in a group; see e.g. quantales and quantale-valued metric spaces.

If you keep taking this perspective further you'll arrive at Lawvere's insight that metric spaces are a type of enriched category, and the partially ordered monoid can be further generalized to a monoidal category or even more generally than this.

I am not really aware of any useful applications of this point of view to analysis, though. The most general thing that looks like this that I know of is valuation rings, which use a totally ordered abelian group.