Can we make a theory of small categories?
Welcome to MSE!
While people have studied notions of model theory with partial functions (though in my experience, the universal algebraists tend to be slightly more excited by these things), there are two possibilities for a cleaner approach. For completeness sake, you can find some information about "partial algebras" here, and "free logic" here.
The first cleaner approach is to simply make composition a relation. After all, a partial function is still a relation, and model theory is perfectly well equipped to handle relations with certain axioms!
Then we might formulate a first order notion of a category as a $2$-sorted theory (with a set $\mathsf{Ob}$ of objects and a set $\mathsf{Mor}$ of morphisms) equipped with three function symbols
- $\text{dom} : \mathsf{Mor} \to \mathsf{Ob}$
- $\text{cod} : \mathsf{Mor} \to \mathsf{Ob}$
- $\text{id} : \mathsf{Ob} \to \mathsf{Mor}$
and one relation symbol
- $\text{comp} \subseteq \mathsf{Mor} \times \mathsf{Mor} \times \mathsf{Mor}$
Then one can include axioms like
$$ \forall x : \mathsf{Ob} . \forall f : \mathsf{Mor} . \text{dom}(f) = x \to \text{comp}(f,\text{id}(x),f) $$
This axiom says that, if the domain of $f$ is $x$, then $f \circ \text{id}(x)$ is defined and equals $f$.
You might also want an axiom
$$ \forall f : \mathsf{Mor} . \forall g : \mathsf{Mor} . \text{dom}(f) = \text{cod}(g) \to \exists h : \mathsf{Mor} . \text{comp}(f,g,h) $$
This axiom says that for any two composable morphisms, a composite actually exists.
You can imagine similar axioms asserting composition is associative, etc.
As a (fun?) exercise, you should try to list all the axioms in this way. Keep in mind you'll need to add some silly looking axioms like $\forall x : \mathsf{Ob} . \text{dom}(\text{id}(x)) = x$ and an axiom saying that for noncomposable morphisms, a composite doesn't exist.
The other way to handle a theory of categories is to move to something slightly more expressive than first order logic. This is the approach taken by many categorical logicians, as it lets us talk about a theory of categories "internal" to another category. It's a little bit more complicated, so I won't say much about it, but you can find a good discussion in Awodey's Lecture Notes on Categorical Logic. In particular in catlog2a, section 2.3.1.
The idea is to work with a theory that allows "subtypes". This gives us the power to quantify over definable subsets, which is all we need to handle composition. After all, if we have two basic sorts $\mathsf{Ob}$ and $\mathsf{Mor}$, then we can define a new sort
$$ C \triangleq \{ (f,g) : \mathsf{Mor} \times \mathsf{Mor} ~|~ \text{dom}(f) = \text{cod}(g) \} $$
and a function $\circ : C \to \mathsf{Mor}$ denoting composition.
Again, as a (fun?) exercise, you might try to explicitly write down the axioms with this new power at your disposal.
I hope this helps ^_^
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:
- $h \circ g \not= u$ and $g \circ f \not= u$
- $(h \circ g) \circ f \not= u$
- $h \circ (g \circ f) \not= u$
- $(h \circ g) \circ f \not= u$ and $(h \circ g) \circ f = h \circ (g \circ f)$.
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.