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 aⁿ = 0 implies a = 0, one for each n.

Previous post here. Next post here.

Chad Orzel announced he’s giving up reading blogs for Lent. The Catholic custom is to give up something enjoyable over the time between Ash Wednesday and Easter. (My father’s mother was Catholic, and once when I was a kid suggested I give up something for Easter. My offer to give up peas was not well-received.)

I was thinking that for any blogger less prolific than Chad, the ultimate Lenten sacrifice would be to give up not blogging. Few blogging-related activities in life are more pleasurable than putting off finishing a post because it’s not quite perfect.

I’m not making any promises, though.

Now to the actual definition of Horn clause. First, some standard logical terminology. A term is simply an expression built out of variables and function symbols. For example, x y^-1 z is a term in the language of groups. An atomic formula is a formula that consists of relation symbols (including equality) applied to terms. So xy = yx is an example of an atomic formula in the language of groups. What makes an atomic formula atomic is that it’s not built out of smaller logical formulas.

A Horn clause is built out of atomic formulas in a particular way. Let A_1, … A_n and B
be atomic formulas. Then a Horn clause is a logical formula of the form

A_1 and … and A_n implies B.

As a degenerate special case, the left-hand side of the implication can be empty, which is the same as asserting formula B holds unconditionally.

Previous post here. Next post here.