Rings with common division, common meadows and their conditional equational theories
<|reference_start|>Rings with common division, common meadows and their conditional equational theories: 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.<|reference_end|>
@article{bergstra2024rings,
    title={Rings with common division, common meadows and their conditional
  equational theories},
    author={Jan A Bergstra, John V Tucker},
    journal={arXiv preprint arXiv:2405.01733},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.01733},
    primaryClass={cs.LO cs.SC}
}