# Horn Clause Example: Rings

I thought I would give a series of examples in increasing exoticness, starting with rings.

A ring has a signature that consists of two binary operations, + and ., one unary operation (-), and two constants (or nullary operations), 0 and 1. The axioms for a ring consist of the associative law for both + and ., the commutative law for +, and the appropriate axioms for -, 0, and 1. Since these all consist of equations, these are all Horn clauses.

Commutative rings are also axiomitizable by adding the commutative law for multiplication. Commutativity is just one of a large family of additional equations that can imposed on the theory of a ring. The whole topic is well-studied, and goes by the name of polynomial identity rings.

In the usual axiomatization of rings, unary minus is not explicitly included. Instead, the existence of an additive inverse is postulated, and uniqueness is proven. This axiom is not a Horn clause, but since the element is unique, you can reformulate it by introducing a new function for the additive inverse.

This trick is not universally applicable. The axioms for division rings, where every nonzero element has a multiplicative inverse, cannot be given in terms of Horn clauses, even by introducing a new function symbol for inverses. One immediate problem is that the inverse is only a partial function, since zero does not have an inverse. This problem can be finessed by extending the notion of Horn clauses to partially-defined functions (something that I will address in a later post). A more serious problem is that there is no way to express the notion that an element is either zero, or has an inverse.

Integral domains also cannot be axiomatized by Horn clauses: the notion that ab = 0 implies that a = 0 or b = 0 is inexpressible. Horn clauses can express the idea that a ring has a zero nilradical, by introducing infinitely many axioms of the form an = 0 implies a = 0, one for each n.

Previous post here. Next post here.