I'm starting Model Theory: An Introduction by David Marker. After reading about an $\mathcal{L}$-theory for a language $\mathcal{L}$, I wanted to try to make a theory of small categories. Can this be done?
My instinct for an approach is to start with a set $X$ of objects and actually create a theory for the morphisms of the category. So I want some "partial operation" $\circ$, which I was going to do by adding a constant symbol $u$, for undefined, and create rules for when I can compose morphisms. I think I could figure that out, but I also really want an axiom like $\forall f \:\exists x\in X\: f\circ 1_x = f$. But of course, I am not allowed to quantify over this random set $X$. Even if I put constants $1_x$ in my language, I also cannot quantify over subsets of the universe. Thoughts?
Giving a theory of the morphisms is a good idea. One way to see this is that you want the structure-preserving maps between categories to be functors, and a functor is a functional relationship on objects and morphisms. But notice that a functor $F : \mathcal{C} \to \mathcal{D}$ has to satisfy $1_{F(x)} = F(1_{x})$ for all $x \in \mathcal{C}$, so really you only have to specify how a structure-preserving map between categories acts on arrows: if you want to know how it acts on an object $x$, you just have to look at how it acts on $1_{x}$. Moreover, the category axioms imply that there is a bijection between objects and identity morphisms.
So one thing we could do is to forget about the objects entirely, and cook up a theory whose domain $M$ is intended to be the set of morphisms in a category. We want to give a partially-defined composition relation and impose some axioms on it. Let's use your suggestion, and introduce a constant $u$ representing the "undefined morphism" and a function symbol $\circ : M \times M \to M$. I guess you will have to give some axioms involving $u$, like $\forall f\, (f \circ u = u)$ and such. Alternatively, you could introduce a relation $C \subseteq M \times M$ and make the signature of your function symbol $\circ : C \to M$.
For the identity axiom, we want to make sure there is an identity morphism for every object in the category. But we want to avoid talking about objects directly. But objects are just the things that serve as domains and codomains for morphisms. And (co)domains are used to say which morphisms are composable. The identity axiom says that for every morphism $f : x \to y$ there is a morphism $1_{x} : x \to x$ that's composable with $f$ and such that $f \circ 1_{x} = f$. So we can just say that: $$ \forall f\, \exists e\, (\{f \circ e = f\} \land \forall g\, \{[(g \circ e \not= u) \to (g \circ e = g)] \land [(e \circ g \not= u) \to (e \circ g = g)]\}) $$ and a similar axiom involving things like $e \circ -$. Informally, this says that for every $f$ there is an $e$ that acts like the identity of the domain of $f$. There's no reason to quantify over objects here, because what we're really after is the identity morphism, and that's just a morphism that acts as a unit. Then all that's left is associativity. You can formalize this as the statement that the following are equivalent:
Of course, there's always more than one way to give a theory of some mathematical object. For example, you could have a theory with a predicate $O$ that applies to objects and a predicate $M$ that applies to arrows, and ensure identity arrows with a function symbol $1 : O \to M$, or something like this. There are lots of options.