What makes the pairs of operators $(-, +)$ and $(÷, ×)$ so similar?

What you're talking about is called a Field.

A Field is a set (say rational number $\mathbb{Q}$, real numbers $\mathbb{R}$, complex numbers $\mathbb{C}$, etc...) together with two operations $(+,\times)$ such that the following axioms holds:

The operations are associative: $a + (b + c) = (a + b) + c$ and $a \cdot (b \cdot c) = (a \cdot b) $

The operations are commutative: $a+b=b+a$ and $a\cdot b=b\cdot a$

Each of the operations has it's own identity element $(0,1)$. Formally, there exist two different elements $0$ and $1$ such that $a + 0 = a$ and $a · 1 = a$.

And each of the operations admits an "inverse" (i.e. we have $(-,/)$). That is,

For every $a$, there exists an element denoted $−a$, such that $a + (−a) = 0$. Similarly for every $a\not = 0$ there exists an element, often denoted by $a^{-1}$ or $1/a$ such that $a\cdot a^{-1}=1$.

Finally there is one more axiom which associate between the additive and multiplicative notion. It's called the distributivity and it says that $a \cdot (b + c) = (a \cdot b) + (a \cdot c)$.

We have many fields some of them are finite and some are infinite. In my opinion the best example for a finite field would be $\mathbb{F}_p$ - the field of $p$-elements with addition and multiplication modulo $p$, you can read about it and more finite fields here. The most useful infinite fields (Again in my opinion) are the rational numbers, the real numbers and the complex numbers with the usual addition and multiplication. The important part however is that and every field satisfies all of the properties that you mentioned in your question.

Note that I removed quantifiers from the definitions to make them simpler, for the complete and correct axioms of a field please click the link in the first line.


Since you're interested in type theory and say that you therefore want an element free perspective, I'll give you the categorical perspective.

In category theory, we can define group objects in a category $C$ with finite products (including the terminal object, $*$) as an object $G$ with $\mu : G\times G \to G$ (a binary operator), $e: * \to G$ (a nullary operator), and $i : G\to G$ (a unary operator) satisfying the following relations, where $\Delta_G : G\to G\times G$ is the diagonal map and $\tau_G : G\to *$ is the map to the terminal object:

Associativity: $$\mu\circ (\mu\times \newcommand\id{\operatorname{id}}\id) = \mu\circ (\id\times \mu) :G\times G\times G \to G$$ Identity: $$\mu\circ (\id\times e)=\mu\circ (e \times \id)=\id : G\times G$$ Inverses: $$\mu\circ (\id\times i) \circ \Delta_G = \mu\circ (i\times \id) \circ \Delta_G = e\circ \tau_G : G\to G$$

Now this axiomatization is equivalent to the axiomatization you've given in your question, except that instead of inversion, you've given division as the primitive operation.

To get your data, we define division as $d=\mu \circ (\id \times i)$.

Conversely, given division $d: G\times G\to G$, we define $i$ by $i=d\circ (e\times \id)$.

Your axiomatization gives associativity and identity for free, plus also commutativity (so you're technically axiomatizing abelian groups).

Then your "dual identity" can be phrased $$\mu\circ (d\times \id) \circ (\id \times \Delta_G) = d\circ (\mu \times \id)\circ (\id \times \Delta_G) = \id \times \tau_G : G\times G\to G $$

Composing with $e\times \id$ we get the identity $$\mu\circ (d\times \id) \circ (\id\times \Delta_G) \circ (e\times \id) = \mu\circ (d\times \id)\circ (e\times \id\times \id)\circ \Delta_G = \mu\circ (i\times \id)\circ \Delta_G=e\times \tau_G,$$ which is half of the inverses identity, and the other half we get is: $$d\circ (\mu\times \id) \circ (\id\times \Delta_G) \circ (e\times \id) = d\circ (\mu\times \id)\circ (e\times \id\times \id)\circ \Delta_G = d\circ \Delta_G=e\circ \tau_G,$$ so we just need to check $d = \mu\circ (\id \times i)$, and this follows from your double reverse and dual substitution identities. (We get $\alpha + (-\beta) = \alpha - (-(-\beta)) = \alpha - \beta$).

Conclusion

All of the properties you've listed follow from the fact that the operations you've chosen define abelian groups.

Thus the reason the triples of operators (don't forget the identity) are so similar is that they each define abelian groups.

Edit:

It's now a bit more clear to me what you're asking about. You also are interested in the relationship between these pairs/triples of operators, and how to possibly add another pair/triple.

In which case I feel the need to point out that fields don't come with two pairs of operations.

It's actually a bit easier to see this in the case of (commutative) rings.

For a general commutative ring $R$ define $a/b = a\cdot b^{-1}$ when $b$ is invertible.

Then the collection of all invertible elements of $R$, denoted $R^\times$ forms a group, and it has identity $1$, the usual multiplication as multiplication, and the division just defined gives the division operation.

Now $R^\times=R$, as sets only when $R=0$, the zero ring, since otherwise $0$ is never invertible. Thus the triple of operations $(1,*,/)$ is never actually a triple of operations on $R$, but rather a triple of operations on the related object $R^\times$.

In the very special case of fields, $R^\times = R\setminus\{0\}$, but for say the integers, we have $\Bbb{Z}^\times = \{1,-1\}$.

Also there is an additional axiom relating the operations $+$ and $*$, the distributive law.

Thus it's not clear what you mean by adding another triple of operations.

The two triples of operations already discussed aren't defined on the same set/type to begin with, so it's not quite clear how you'd be adding a third.

Also even if you did construct a related type on which to define a third operation, this third operation should relate to the previous two in some way.

In mathematics, there are examples of rings with additional operations (though none that I can think of that form an abelian group), such as differential graded algebras, but the third operation always relates to the prior two in some way.


Update: A more detailed answer is available on this mathoverflow post.

Following @Henry’s suggestion, a recursive structure of abelian groups can be constructed by using commutative hyperoperations:

$p_{n+1}(a, b) = \exp(p_n(\ln(a), \ln(b)))$

$p_0(a, b) = \ln\left(e^a + e^b\right)$

$p_1(a, b) = a + b$

$p_2(a, b) = a\cdot b = e^{\ln(a) + \ln(b)}$

$p_3(a, b) = a^{\ln(b)} = e^{\ln(a)\ln(b)}$

$p_4(a, b) = e^{e^{\ln(\ln(a))\ln(\ln(b))}}$

These functions give us the sequence of $(+, ×, ...)$ operations, while their inverse functions give us the sequence of $(-, ÷, ...)$ dual operations. The sequence of identity terms is $(0, 1, e, ...)$. With this, $T_1$ (Type Level 1) is isomorphic to a group, $T_2$ is isormorphic to a field, and successive types give you more and more complex objects.

The identity terms are:

$i_n = e \upuparrows (n - 2).$

$i_1 = 0.$

$i_2 = 1.$

$i_3 = e.$

$i_3 = e ^ e.$

$i_4 = e ^ {e ^ e}.$

While I cannot yet fathom what $T_4$ And successive types can be used for, I have to believe that $T_3$ is interesting, because it brings exponentiation to the table in a very natural manner. Therefore, stopping at the level of fields feels quite shortsighted.

Also, $T_1$ is isomorphic to $\mathbb{Z}$ and $T_2$ is isomorphic to $\mathbb{Q}$, but $T_3$ is isomorphic to a strict subset of $\mathbb{R}$. This goes to suggest that the gap between $\mathbb{Q}$ and $\mathbb{R}$ is pretty large and should be filled incrementally with larger and larger sets. One interesting question is whether $T_n$ “converges” toward a structure that is isomorphic to $\mathbb{R}$ when $n$ increases.


Here is my best attempt at answering this question; but the answer I have is likely to be disappointing.

If $(+, -)$ with 0 as identity element defines a group and $[(+, -), (×, /)]$ with 1 as identity element for $(×, /)$ defines a field, what is defined by $[(+, -), (×, /), (\#, @)]$ with an identity element for $(\#, @)$ other than 0 and 1?

As far as I know, no such thing has been studied any significant amount.

As you've noticed, any field has two corresponding groups: its additive group and its multiplicative group. These two groups have different identity elements.

I'm not aware of any kind of algebraic structure which has three corresponding groups. And nobody is going to study such things, or name them, until someone has found an interesting example of such a thing.


$\log$ turns multiplication and division into addition and subtraction. The precise statement is that $\log: \mathbb R^+ \to \mathbb R$ is a group isomorphism, whose inverse is $\exp$.