4
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Do you have any objection to using relation symbols instead of function symbols for basic operations? $\endgroup$ – Eric Wofsey Oct 8 '16 at 0:09
  • 3
    $\begingroup$ Multi-sorted signatures with a finite number of sorts can be reduced to one-sorted signatures. We add a new unary predicate for each of the sorts, and an axiom saying that each element satisfies exactly one of these predicates. We then use these predicates in the one-sorted signature to tell which of the original sorts each element belongs to, and in this way each model of the multi-sorted theory can be transformed into a model of the one-sorted theory, and vice-versa. $\endgroup$ – Carl Mummert Oct 8 '16 at 0:14
  • 1
    $\begingroup$ Categories just aren't a theory of the kind you want-you need relations, as mentioned, or else a category structure on the sorts themselves to express that the object of composable arrows is a certain pullback. $\endgroup$ – Kevin Carlson Oct 8 '16 at 0:16
8
$\begingroup$

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).

$\endgroup$
3
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

Demonstrating that Eric Wofsey's directions above can truly be executed, William Hatcher published some axioms whose every model will always be "a (small) category", and whose signature contains only 3 things: a pair of term-constructor-functions (for the source and target of every arrow, or the domain and codomain of every morphism), and a single (ternary) predicate for composition. As the original question noted, we can't make composition a term-constructor because the usual framework for a first-order language doesn't allow those to be partial, but composition needs to be. Hatcher's axiomatization (courtesy of Roger Bishop Jones) uses $d(.)$ for source ("domain"), $c(.)$ for target ("codomain"), and $K(ar1,ar2,result)$ for composition.

A notable feature of this first-order treatment is that it is mono-sortal: every individual thing in the whole domain of discourse -- including objects! -- is an arrow here. Objects are the "identity" arrows and and every arrow goes from an id-arrow to an id-arrow. Every "object" is an arrow going from itself to itself.

Groups actually can be described in this one-sorted framework. It would model a group as a category with 1 ojbect, which is identified with the identity-element of the group; the other arrows are the other elements of the group; and arrow-composition plays the role of the group operator. Any pair of these "loop" arrows composes to another loop -- they all have the sole object (the identity arrow) as both source and target. Composition is associative (as group operators need to be) already.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.