I have been trying to formally state the axioms of category in predicate logic. It seems that I will need one-place predicates for objects and arrows, two-place predicates for heads and tails of arrows and a three-place predicate for composition. I am trying to avoid the use of the functional notation found in most definitions of CT, notation which IIUC more properly belongs in the domain of set theory.
EDIT: Predicate logic alone would seem to be completely unworkable as a language to express the axioms of category theory. I don't see any way around starting with 11 universally quantified variables in predicate logic for the axiom of associativity, compared to only 3 when using the '$\circ$' notation for the composition of arrows. (Sigh)