Excess axioms in the definition of a metric First, I am aware of how to show the following, my question concerns the reasoning of the standard metric definition.
Traditionally, the axioms defining a metric $\rho:X\times X \rightarrow \mathbb{R}$ where $X$ is a nonempty set, are given as:


*

*$\forall x, y\in X, \rho(x, y) = 0 \iff x = y$,

*$\forall x, y\in X, \rho(x, y) = \rho(y, x)$,

*$\forall x, y, z\in X, \rho(x, y)\leq \rho(z, x) + \rho(z, y)$,

*$\forall x, y\in X, 0 \leq \rho(x, y)$.
It is easy to see that axiom 4 follows from axioms 1 and 3. It is also fairly trivial to show that axiom 2 follows from axioms 1 and 3. It then seems logical to only require the two axioms


*

*$\forall x, y\in X, \rho(x, y) = 0 \iff x = y$,

*$\forall x, y, z\in X, \rho(x, y)\leq \rho(z, x) + \rho(z, y)$,
as a definition for a metric. Is there a good reason that this is not the case, besides historical continuity?
Edit: Thanks to Paul Frost for mentioning my original definition was for pseudometrics... The question has been updated.
Edit 2: As commenters have asked for a proof:
Axioms 1, 3 imply axiom 2: First, consider the triangle inequality for general $x, y, z\in X$. Then, $$\rho(x, y) \leq \rho(z, x) + \rho(z, y),$$ next, set $z = y$ to obtain $$\rho(x, y) \leq \rho(y, x) + \rho(y, y)\Rightarrow \rho(x, y) \leq \rho(y, x)$$ by axiom 1. Similarly, $$\rho(y, x) \leq \rho(z, y) + \rho(z, x),$$ and setting $z=x$ yields $$\rho(y, x) \leq \rho(x, y) + \rho(x, x)\Rightarrow \rho(y, x) \leq \rho(x, y)$$ so $\rho(x, y) = \rho(y, x)$.
We may then show Axioms 1, 2, and 3 imply 4. See this answer. It may be somewhat incorrect to say axioms 1 and 3 imply 4, but I don't see this as a problem, as 1 and 3 imply 2, and 1, 2, 3 imply 4. If I'm incorrect in that assumption, please let me know.
 A: Your statement of the triangle inequality is not quite the same as the usual one, which says $d(x, y) \le d(x, z) + d(z, y)$. The usual definition supports the intuition that $d(x, y)$ measures the time (or cost or work) of getting from $x$ to $y$ with no assumption that getting from $x$ to $y$ involves the same amount of time (or ...) as the return journey.
There are very simple examples of asymmetric metrics: e.g., what you might call the morning rush-hour metric between a city $A$ and a suburb $B$ with $d(A, B) < d(B, A)$ and $d(A, A) = d(B, B) = 0$. See Lee Mosher's comment for many more interesting examples.
The answer to your question necessarily involves a matter of mathematical opinion. The usual axioms for metric spaces clearly separate several concerns. As often happens with axiomatisations, you can find an axiomatisation with fewer axioms or operators by making some clever changes (e.g., axiomatising a group in terms of the operation $(x, y) \mapsto xy^{-1}$) but this will generally make the axiomatisation harder to understand and harder to generalise.
