How to state the Axioms of Category Theory in Predicate Logic?

Solution 1:

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.