Rings with common division, common meadows and their conditional equational theories

TL;DR

This paper investigates totalized division operations in commutative rings, introduces common divisions and common meadows, and establishes completeness theorems for their conditional equational theories.

Contribution

It introduces the concept of common division and common meadows, and proves completeness theorems for their conditional equational theories, extending the understanding of division in algebraic structures.

Findings

Equational axioms are complete for rings with inverse-based common division.

Direct division satisfies axioms under eager equality despite failing in standard form.

The paper establishes a new congruence for partial terms to prove completeness.

Abstract

We examine the consequences of having a total division operation $\frac{x}{y}$ on commutative rings. We consider two forms of binary division, one derived from a unary inverse, the other defined directly as a general operation; each are made total by setting $1/0$ equal to an error value $\bot$, which is added to the ring. Such totalised divisions we call common divisions. In a field the two forms are equivalent and we have a finite equational axiomatisation $E$ that is complete for the equational theory of fields equipped with common division, called common meadows. These equational axioms $E$ turn out to be true of commutative rings with common division but only when defined via inverses. We explore these axioms $E$ and their role in seeking a completeness theorem for the conditional equational theory of common meadows. We prove they are complete for the conditional equational theory of commutative rings with inverse based common division. By adding a new proof rule, we can prove a completeness theorem for the conditional equational theory of common meadows. Although, the equational axioms $E$ fail with common division defined directly, we observe that the direct division does satisfies the equations in $E$ under a new congruence for partial terms called eager equality.