# Is it possible to formalize a “universe” of categories as a one-sorted first-order theory with one binary relation and no functions?

This is a modification of a question I asked earlier.

In that question, I hadn't placed any limits on the number of binary relations allowed, so my question had an affirmative answer, but a trivial and uninteresting one. This modification effectively changes the question by making it much less trivial, so this is not a duplicate post.

ZFC set theory is typically formalized as a one-sorted theory without urelements, and with a signature containing one primitive binary relation and no primitive functions.

Is it possible to do the same with category theory or higher category theory, formalizing a universe of categories as a first-order theory with only one type of object, one binary relation, and no functions?

To clarify: what I want is to formulate a first-order theory of an entire "universe" of categories, much like ZFC is a "universe" of sets - not a first-order theory in which the models are individual categories in general. This could be done in several ways: the universe could be a category itself, effectively formalizing Cat in an "Elementary Theory of the Category of Categories." Or, you could perhaps think of it as a theory of the 2-category of 1-categories, or something like that. (The discussion with user18921 in the comments made it clearer to me that there was some confusion on this point.)

If the above is impossible, then as a small concession, I'll allow a single binary function $\circ$ to denote composition, though it would be nice to see if it's possible even without that. I would expect that it is, much in the same way that $\cup$ and $\cap$ don't need to be defined explicitly as function symbols in the signature of ZFC. (You could also probably formalize $circ$ instead as a binary relation, just denoting that the composition of two functions exists.)

As before, I understand that this runs counter to what some feel is the philosophical spirit of category theory, but I'm still curious if it's possible anyway, just as an interesting logical puzzle.

My comments from before are repeated, as they still apply, and are now more pertinent that the trivial solution to the original question no longer applies:

It seems tricky to me at first glance. A "category" has a "set" of "objects" and another set of "morphisms." That's already four sorts of thing - category, set, object, morphism.

However, it's possible to identify an "object" with the identity morphism on that object. So, you could perhaps use this idea to bring you down to only three sorts of thing - category, set, and morphism.

Alternatively, you could say that "object" and "morphism" are both types of the more fundamental n-morphism, and arrive at a three-sorted theory of categories, sets, and n-morphisms.

You could also try to formalize a "set" as a discrete category, and bring you down to only two sorts of thing - category and (n-)morphism.

If you go with n-morphisms, maybe you could try to identify every n-morphism with the (n+1)-identity morphism on it, and see if that simplifies things somehow.

The above are some ideas that I had; I'm not even sure if they'd work. But assuming they do, that still leaves you with only two things - categories and morphisms - and I'm not sure if it's possible to go one step further and get it down to one thing. Thoughts?

• Actually, the link you gave puts it better than that. ETCS defines Set by making reference to a "natural numbers object". Any first-order theory of categories certainly ought to be able to formalize Set in a way that meets those axioms, and hence it also ought to be able to formalize the natural numbers object - no? – Mike Battaglia Aug 29 '13 at 5:43
• Hey no chat for me today, I really need to get some assignments in. If you're trying to formalize a first-order theory of a universe of categories, I think that's a great idea and I think Lawvere was (is?) arguing for the same thing. In that case, yes, you will certainly be able to interpret arithmetic. I think you should edit the question to make clearer what you're looking for. Don't assume people have read the other question !! – goblin Aug 29 '13 at 5:56
• Yeah, I think that's a good way of putting it. I've heard that the appropriate concept is not the class of all categories, nor the category of all categories, but rather the 2-category of all 1-categories. So you're probably looking for an axiomatization of the 2-category of all categories, just like ETCS axiomatizes the 1-category of all 0-categories. – goblin Aug 29 '13 at 6:01
• I don't get the motivation behind the question. Somehow it misses the whole point of category theory. – Martin Brandenburg Aug 29 '13 at 6:53
• The motivation is to come to a better understanding of the difficulties in formalizing a first-order theory of the category of categories, and to understand exactly what distinguishes such a theory from set theory. I thought it a useful conceptual exercise to embrace materialism for just a second, for the sake of figuring out how such a theory might compare to ZFC. – Mike Battaglia Aug 29 '13 at 7:08

The answer to the logical puzzle is "yes". For any finite signature $\Sigma$, there is a sentence $\chi$ in the language of a single binary relation such that models of $\Sigma$ are bi-interpretable with models of $\chi$ (Hodges, Model Theory, Theorem 5.5.1).
• And moreover, the proof of this is quite cute and elementary. Slightly modified from Hodges’ version, for concision: given a (possibly several-sorted) language $L$ with finite signature, first choose for each sort $S$ a natural number $\alpha(S) > 2$, and for each relation symbol $R$ a natural number $\beta(R) > 1$, all distinct. (Assume functions are coded by relations.) Now, given any $L$-structure $M$, produce a graph $G(M)$ as follows: for each element $x \in M_S$, add a vertex $v_x$, connected by one edge to a copy of $K_{\alpha(S)}$ — this “tags” it according to its sort. [cont’d] – Peter LeFanu Lumsdaine Oct 22 '13 at 12:20
• And whenever a relation $R(x_1,\ldots,x_n)$ holds, connect $v_{x_1},\ldots,v_{x_n}$ by an $n$-armed star with arms of length $\beta{R}$. Now, three not-too-difficult claims to verify: (A) you can recover $M$ from $G(M)$, up to isomorphism; (B) you can axiomatise which graphs arise from $L$-structures in this way by a single sentence $\theta_L$ in the language of one binary relation; (C) a formula $\varphi(\vec x)$ of $L$ can be translated into a formula $\hat{\varphi}(\vec x)$ in one binary relation, such that $M \vDash \varphi(\vec x)$ exactly if $G(M) \vDash \hat{\varphi}(\vec v_x)$. – Peter LeFanu Lumsdaine Oct 22 '13 at 12:21
• Yes, it is a cute proof. I think you may need to modify your construction a little so that you can recover the order of the $x_i$ from the star that represents $R(x_1, \ldots, x_n)$. – Rob Arthan Oct 22 '13 at 12:31
• ah, thanks; yes, I tried to simplify it a little too far. Try this: represent $R(x_1,\ldots,x_n)$ by a star with arms of lengths $\beta(R)+1,\ldots, \beta(R)+n$ going to $v_{x_1}, \ldots$ respectively. We can now recover the order of the arguments from the lengths; and using $\beta(R)+1 \geq 2$ for the shortest arm ensures that this doesn’t create any triangles, so we can still pick out the $K_n$ tags and hence recover the original carrier set of the structure. I hope we’re good now? – Peter LeFanu Lumsdaine Oct 22 '13 at 12:38