We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo

Computer Science > Logic in Computer Science

Title: 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, 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.
Subjects: Logic in Computer Science (cs.LO); Symbolic Computation (cs.SC)
Cite as: arXiv:2405.01733 [cs.LO]
  (or arXiv:2405.01733v1 [cs.LO] for this version)

Submission history

From: John Tucker [view email]
[v1] Thu, 2 May 2024 21:07:00 GMT (50kb)

Link back to: arXiv, form interface, contact.