Model theory: What is the signature of `Category theory`

Question

I'm studying model theory nowadays, and I understand how one-sorted (classical) signatures and structures work. However I am also interested in groupoids, which can not be described as a structure for a one-sorted signature.

Looking up online, I came to the notion of many-sorted signature: nLab, Wikipedia. According to nLab, these can be used to describe, for example, directed (multi-)graphs, which seems easy enough: Take sorts for edges and vertices, and source and range maps from edges to vertices.

However I can't see how can we describe a signature for categories in this language. We need all the ingredients for graphs (edges=arrow, vertices=objects), and at least one function symbol for composition, but since composition is only partially defined, I don't see how this can be done.

Answer 1

Partially defined operations can be represented in first-order logic by relation symbols instead of function symbols. (Actually, so can totally defined operations--you don't actually need function symbols at all, though they are convenient for many purposes.) For instance, instead of writing $\circ$ for a partially defined binary operation, you can define a ternary relation $C(a,b,c)$ which you think of as "$a\circ b=c$". You then just have to add extra axioms stating that there exists a $c$ such that $C(a,b,c)$ iff the codomain of $b$ is the domain of $a$, in which case there exists only one such $c$.

You can use the same trick to avoid needing multiple sorts as well, as long as you only have only finitely many sorts. Just add a unary relation for each sort, and then encode all your functions as partial functions which are only defined when the inputs have the correct sort. You also need to add axioms saying all your relations can only be true if their arguments have the sorts they're supposed to. Finally, you need to add an axiom saying that every element has exactly one sort (this part is why you need to have only finitely many sorts).

Answer 2

Just to give you a name to search for: Categories are models for an essentially algebraic theory. Because they require partially defined functions, essentially algebraic theories don't fit into the standard formalism of model theory.

But, as described in Eric Wofsey's answer, they can be simulated in many-sorted logic using relation symbols for the graphs of the partially defined functions (or in single-sorted logic if the number of sorts is finite, as it is in the case of categories - the usual presentation has one sort for objects and one sort for arrows).

Another option for simulating partially defined functions in standard first-order logic is to add a new constant symbol $*$ and set $f(\overline{a}) = *$ whenever $f(\overline{a})$ is undefined.