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$中的等式。