Ars Mathematica

Daniel Murfat has a nice series of notes on various mathematical topics, mostly algebraic geometry.

I came across this history of loops, a generalization of groups, where I picked up this interesting tidbit: loops are named after the Chicago Loop, the central business district of Chicago. (The elevated trains tracks form a loop that enclose it.)

Classical algebraic structures such as groups and rings can be given entirely in terms of equations, so they don’t require the full expressiveness of Horn clauses.

Directed graphs (with at most one edge between nodes) can be represented by their adjacency relation: for two vertices x and y, the adjacency relation R(x,y) holds if there is an edge from x to y. Undirected graphs can be modeled by requiring that directed edges between two vertices go in both directions: R(x,y) implies R(y,x).

Partially-ordered sets can also be modeled in terms of Horn clauses. The three properties of a partial order are all Horn clauses:

• reflexivity — x ≤ x
• transitivity — x ≤ y and y ≤ z implies x ≤ z.
• asymmetry — x ≤ y and y ≤ x implies x = y.

(Thus preorders, which drop the asymmetry axiom, are also given by Horn clauses.)

Total orders, which impose the requirement x ≤ y or y ≤ x, cannot be given by Horn clauses.

My normal tendency is to write long posts that I never finish. I’ll start off this series with small posts to see if I can break the habit.

The idea of Horn clauses emerged from model theory, so I will begin there. Model theory considers ideas that can expressed in very limited languages. You begin with a small vocabulary of constants, function symbols and relation symbols, known as the signature. For example, you can express the theory of groups in terms of two function symbols and one constant: the group product, the inverse function, and a constant that represents the unit. The theory of directed graphs can be described by a single relation symbol R(x,y) that expresses whether a directed edge begins at x and ends at y.

When coupled with first-order logic, even a very limited language can be very expressive. Set theory itself, for example, can be expressed using a single relation symbol (set membership). Horn clauses are special first-order logical statements that are not nearly as expressive, but still cover very many cases, as we shall see.

I was musing about the foundations of mathematics the other day, when it occurred to me that you could make a pretty good case that the key foundational idea of mathematics is that of Horn clauses (also known as universal Horn sentences). Horn clauses, despite begin obscure outside certain areas, are ubiquitous. Many (perhaps most?) basic mathematical objects can be described by Horn clauses. Fundamental category theoretic notions have Horn clause interpretations. Even first-order logic, which contains Horn clauses as a special case, can be viewed as having inference rules in the form of Horn clauses applied at the level of proofs.

I thought I’d spend a couple of posts describing Horn clauses, and laying out the case for their ubiquity.