RINGS WITH COMMON DIVISION, COMMON MEADOWS AND THEIR CONDITIONAL EQUATIONAL THEORIES

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, which are 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 satisfy the equations in E under a new congruence for partial terms called eager equality .