mjhjmtu

Update

My original thoughts are better expressed on this mathoverflow post.

Short Version

When defining the $-$, $+$, $÷$, and $×$ operators in a functional manner, one can observe that the $(-, +)$ pair is very similar to the $(÷, ×)$ pair, and the only main differences between them is their identity terms ($0$ and $1$ respectively) and the fact that the divisor cannot be equal to the identity term of the $(-, +)$ pair of operators.

My questions are the following: where can I find some prior work on this topic, and can one define a family of such operator pairs with different identity terms? Is there any theory for such objects?

Set Theory Version

While the arithmetic properties outlined below can be defined for both sets and types, referring to set theory might help clarify the question: 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?

Since $(+, -, 0)$ is used to define $mathbbZ$ and $[(+, -, 0), (×, ÷, 1)]$ is used to define $mathbbQ$, which $(#, @, r)$ could be introduced so that $[(+, -, 0), (×, ÷, 1), (#, @, r)]$ would define $mathbbS$, with $mathbbQ subset mathbbS subseteq mathbbR$?

Intuitively, $#$ should be based on exponentiation, while $@$ should be based on logarithm.

Long Version

One can define the $-$, $+$, $÷$, and $×$ operators in the following fashion:

Minus:

$
small textMinus Identity Term: the minus identity term is equal to 0.normalsize\
i(m) = 0.\
quad\
small textSubtraction Identity: enspace alpha - 0 = alpha.normalsize\
m(alpha, i(m)) = alpha.\
quad\
small textSelf Subtraction: enspace alpha = beta Longleftrightarrow alpha - beta = 0.normalsize\
alpha = beta Longleftrightarrow m(alpha, beta) = i(m).\
quad\
small textSubtraction Affine Identity: enspace alpha - (beta - gamma) = gamma - (beta - alpha).normalsize\
m(alpha, m(beta, gamma)) = m(gamma, m(beta, alpha)).\
$

Plus:

$
small textMultiplication Affine Identity: enspace (alpha + beta) - gamma = alpha - (gamma - beta).normalsize\
m(p(alpha, beta), gamma) = m(alpha, m(gamma, beta)).\
$

Divides:

$
small textDivides Identity Term: the divides identity term is equal to 1. normalsize\
i(d) = 1.\
quad\
small textDivision Identity: enspace fracalpha1 = alpha.normalsize\
d(alpha, i(d)) = alpha.\
quad\
small textSelf Division: enspace fracalphaalpha = 1.normalsize\
alpha = beta Longleftrightarrow d(alpha, beta) = i(d).\
quad\
small textDivision Affine Identity: enspace fracalphafracbetagamma = fracgammafracbetaalpha.normalsize\
d(alpha, d(beta, gamma)) = d(gamma, d(beta, alpha)).\
$

Times:

$
small textMultiplication Affine Identity: enspace fracalpha × betagamma = fracalphafracgammabeta.normalsize\
d(t(alpha, beta), gamma) = d(alpha, d(gamma, beta)).\
$

We observe that the pair of divides and times operators are defined exactly the same way as the pair of minus and plus operators, but with different identity terms, and with a minus identity restriction on the multiplier subdomain of the divides function.

The symmetry established between the pairs of operators $(-, +)$ and $(÷, ×)$ allows the following pairs of properties to be proven for both properties in every pair by proving it for a single property.

The following properties are established for any pair of operator functions $(f, g)$, which corresponds to the pairs $(-, +)$ and $(÷, ×)$. Furthermore, the term reverse is used to refer to the opposite for the $(-, +)$ pair and to the inverse for the $(÷, ×)$ pair.

Proofs for the $(-, +)$ pair can be found on this notebook.

Anticommutativity: $f(alpha, beta) = f(i(f), f(beta, alpha).$

$
alpha - beta = -(beta - alpha).\
quad\
displaystyle fracalphabeta = frac1fracbetaalpha.\
$

Double Reverse Identity: $alpha = f(i(f), f(i(f), alpha)).$

$
alpha = -(-alpha).\
quad\
displaystyle alpha = frac1frac1alpha.\
$

Associative Commutativity: $f(f(alpha, beta), gamma) = f(f(alpha, gamma), beta).$

$
(alpha - beta) - gamma = (alpha - gamma) - beta.\
quad\
displaystyle fracfracalphabetagamma = fracfracalphagammabeta.\
$

Affine Equivalence: $f(alpha, beta) = gamma Longleftrightarrow f(alpha, gamma) = beta.$

$
alpha - beta = gamma Longleftrightarrow alpha - gamma = beta.\
quad\
displaystyle fracalphabeta = gamma Longleftrightarrow fracalphagamma = beta.\
$

Identity Element: $g(alpha, i(f)) = alpha.$

$
alpha + 0 = alpha.\
quad\
alpha × 1 = alpha.\
$

Dual Substitution: $g(alpha, beta) = f(alpha, f(i(f), beta)).$

$
alpha + beta = alpha - (-beta).\
quad\
alpha × beta = fracalphafrac1beta.\
$

Dual Equivalence: $alpha = g(beta, gamma) Longleftrightarrow beta = f(alpha, gamma).$

$
alpha = beta + gamma Longleftrightarrow beta = alpha - gamma.\
quad\
alpha = beta × gamma Longleftrightarrow beta = fracalphagamma.\
$

Commutativity: $g(alpha, beta) = g(beta, alpha).$

$
alpha + beta = beta + alpha.\
quad\
alpha × beta = beta × alpha.\
$

Associativity: $g(g(alpha, beta), gamma) = g(alpha, g(beta, gamma)).$

$
(alpha + beta) + gamma = alpha + (beta + gamma).\
quad\
(alpha × beta) × gamma = alpha × (beta × gamma).\
$

Dual Identity: $(g(f(alpha, beta), beta) = alpha) land (f(g(alpha, beta), beta) = alpha).$

$
((alpha - beta) + beta = alpha) land ((alpha + beta) - beta = alpha).\
quad\
displaystyle (fracalphagamma × beta = alpha) land (fracalpha × betabeta = alpha).\
$

What you're talking about is called a Field.

A Field is a set (say rational number $mathbbQ$, real numbers $mathbbR$, complex numbers $mathbbC$, 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 $acdot b=bcdot 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 $anot = 0$ there exists an element, often denoted by $a^-1$ or $1/a$ such that $acdot 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 $mathbbF_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 : Gtimes G to G$ (a binary operator), $e: * to G$ (a nullary operator), and $i : Gto G$ (a unary operator) satisfying the following relations, where $Delta_G : Gto Gtimes G$ is the diagonal map and $tau_G : Gto *$ is the map to the terminal object:

Associativity:
$$mucirc (mutimes newcommandidoperatornameidid) = mucirc (idtimes mu) :Gtimes Gtimes G to G$$
Identity:
$$mucirc (idtimes e)=mucirc (e times id)=id : Gtimes G$$
Inverses:
$$mucirc (idtimes i) circ Delta_G = mucirc (itimes id) circ Delta_G = ecirc tau_G : Gto 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: Gtimes Gto G$, we define $i$ by $i=dcirc (etimes 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 $$mucirc (dtimes id) circ (id times Delta_G) = dcirc (mu times id)circ (id times Delta_G) = id times tau_G : Gtimes Gto G $$

Composing with $etimes id$ we get the identity
$$mucirc (dtimes id) circ (idtimes Delta_G) circ (etimes id) =
mucirc (dtimes id)circ (etimes idtimes id)circ Delta_G = mucirc (itimes id)circ Delta_G=etimes tau_G,$$
which is half of the inverses identity, and the other half we get is:
$$dcirc (mutimes id) circ (idtimes Delta_G) circ (etimes id) =
dcirc (mutimes id)circ (etimes idtimes id)circ Delta_G = dcirc Delta_G=ecirc tau_G,$$
so we just need to check $d = mucirc (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 = acdot 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 = Rsetminus0$, but for say the integers, we have $BbbZ^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.