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

TL;DR

This work analyzes the totalisation of division in commutative rings by introducing an absorptive error element $\bot$, yielding common divisions and the framework of common meadows. It compares inverse-based and direct division, proving a finite equational base $E_{ftc-cm}$ that axiomatizes common meadows and, for inverse-based division, the equational theory of rings with common division; completeness is achieved for the conditional theory via an additional rule related to AVL. The paper also shows that direct division generally fails to satisfy $E_{ftc-cm}$, unless one adopts eager equality semantics for partial terms, which restores the equations in that setting. It further develops the algebraic structure, conditional reasoning, and completeness results, and discusses extensions with a conditional operator and alternative division definitions, highlighting open problems about finite axiomatisations of conditional theories. The results bridge algebraic theory (rings, fields, meadows) with computing-inspired semantics (partial/total operations, absorbent elements), offering a foundation for reasoning about arithmetic data types in programming and verification contexts.

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.

Theorems & Definitions (113)

• Theorem 1.1
• Theorem 1.2
• Definition 2.1
• Lemma 2.1
• Definition 2.2
• Definition 2.3
• Lemma 2.2
• Theorem 2.1
• Corollary 2.2
• Definition 2.4