How to state the Axioms of Category Theory in Predicate Logic? 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)
 A: You can actually make do with a smaller language: one ternary relation (composition $Comp$), and two unary functions (source $s$ and target $t$). We conflate objects with identity arrows, so we don't need a separate sort for objects at all.
The axioms now are straightforward:


*

*"Compositions behave correctly." For every pair of arrows $\alpha,\beta$, there is at most one arrow $\gamma$ such that $Comp(\alpha,\beta,\gamma)$; and such a $\gamma$ exists iff $s(\beta)=t(\alpha)$.

*"The source and target of an identity arrow are itself." $t(t(\alpha))=s(t(\alpha))\wedge t(s(\alpha))=s(s(\alpha))$.

*"Compositions are associative." This is a bit long. For instance, to write $(\alpha\beta)\delta=\alpha(\beta\delta)$, we'd write $Comp(\alpha, \beta,\gamma)\wedge Comp(\gamma, \delta, \epsilon)\wedge Comp(\beta, \delta,\theta)\implies Comp(\alpha, \theta, \epsilon).$ But it's totally doable.

*"Identities are identities." $Comp(\alpha, \beta,\gamma)\wedge s(\alpha)=\alpha\implies \beta=\gamma$, and similarly for composition on the right.

*"Identities are their own source and target." $t(\alpha)=\alpha\iff s(\alpha)=\alpha$.
And that's it!

This is not due to me; I read about it in Goldblatt's book Topoi. I forget who he attributed it to.
