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.
翻译:我们考察在交换环上定义全除法运算 $\frac{x}{y}$ 的数学后果。我们考虑两种形式的二元除法:一种源于一元逆运算,另一种直接定义为一般运算;每种形式都通过设定 $1/0$ 等于错误值 $\bot$(该值被添加到环中)而成为全函数。此类全化除法我们称之为公共除法。在域中,两种形式等价,并且我们获得了有限等式公理集 $E$,该公理集对于配备公共除法的域的等式理论(称为公共草地)是完备的。这些等式公理 $E$ 在具有公共除法的交换环中同样成立,但仅当除法通过逆运算定义时才成立。我们探究这些公理 $E$ 及其在寻求公共草地条件等式理论的完备性定理中的作用。我们证明它们对于基于逆运算的公共除法交换环的条件等式理论是完备的。通过添加新的证明规则,我们可以证明公共草地条件等式理论的完备性定理。尽管直接定义的公共除法不满足等式公理 $E$,但我们观察到在一种称为急切相等性的部分项新同余关系下,直接除法确实满足 $E$ 中的等式。