What is the following property of a subtraction operator called?
$a - (b - c) = c - (b - a)$
Having a name for this property is important for algebraic structures defined with a subtraction operator but no addition operator. And these are important for measures such as temperatures that can be subtracted from each other but not added to each other. Physicists call these intensive measures, while statisticians call these intensive variables.
For example, let’s call ordinal a type $\mathfrak{O}$ which terms can be subtracted but not added. The best way to define the subtraction operator for this type is:
$- : \mathfrak{O} \times \mathfrak{O} \longrightarrow \mathfrak{O} \\ a - (b - c) = c - (b - a)$
Interestingly, the codomain of the subtraction operator should actually be an extended type called cardinal that does support addition, with addition defined as:
$+ : \mathfrak{C} \times \mathfrak{C} \longrightarrow \mathfrak{C} \\ a + b = c \Longleftrightarrow c - a = b$
Therefore, the codomain of the subtraction operator should be $\mathfrak{O}$, not $\mathfrak{C}$.
$- : \mathfrak{O} \times \mathfrak{O} \longrightarrow \mathfrak{C}$
But, when the domain of the subtraction operator is $\mathfrak{O} \times \mathfrak{C}$, then its codomain remains $\mathfrak{O}$. In other words, you can subtract a temperature from a temperature, and this gives you a temperature delta. But you can also subtract a temperature delta from a temperature, and this gives you a temperature.
From there, it becomes obvious that you can add a temperature delta to a temperature, which gives you a temperature, while adding two temperature deltas to each other gives a temperature delta. In other words, there is no commutative addition operator for the ordinal type $\mathfrak{O}$, but there is something that comes pretty close (hence the confusion for most people).
If you define the ordinal type $\mathfrak{O}$ as a coinductive type with successor as coinductive operator, an equivalence relation, and a total order relation, you can define a pair of forward and backward operators once you have added the subtraction operator and the cardinal type $\mathfrak{C}$, with $\mathfrak{O} \times \mathfrak{C}$ as domain and $\mathfrak{O}$ as codomain.
The forward operator is equivalent to performing multiple successor operations, while the backward operator is equivalent to performing multiple predecessor operations. And with these, you have operators that let you “add” and “subtract” temperature deltas to and from temperatures, without letting you add two temperatures together.
This line of thinking has some interesting consequences. For example, it suggests a different definition for the arithmetic mean. Indeed, if one defines the arithmetic mean as a sum divided by a count, how does one gets the average of two temperatures since they cannot be summed?
In order to work around this problem, one has to define the subdivision operator on an extension of the cardinal type $\mathfrak{C}$. We will call it the fractional type $\mathfrak{F}$. From there, the arithmetic mean of two ordinal terms (like two temperatures) is defined as:
$a, b : \mathfrak{C} \mid a < b \\ mean(a, b) = forward(a, (b - a) / 2)$
I should also mention that all this should apply to both sets or types, but I do all my work with types instead of sets, just because non-mathematicians are more comfortable with them, and because it lends itself nicely to the approach of building a hierarchy of type whereby an extended type is defined from a primitive type by simply adding an extra relation or operation.
I do not know how far this could go, but I am putting my ideas together on this notebook.
