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)

  • $\begingroup$ Can you give an example of the functional notation to which you refer? $\endgroup$ – Cameron Buie Dec 29 '15 at 21:13
  • $\begingroup$ Functions or $k$-ary operations can be replaced by $k+1$-ary predicates, with suitable axioms of unique existence to express functional dependence of the "output" argument on the inputs. $\endgroup$ – hardmath Dec 30 '15 at 0:17
  • 1
    $\begingroup$ Note that extending first-order logic to allow partial functions is in some sense a "trivial" extension - you're just adding symbols to stand for first-order expressions. So you can use a partial function symbol for composition, and still retain all the niceness of first-order model theory (e.g. compactness, Lowenheim-Skolem, etc.) as long as you're careful. $\endgroup$ – Noah Schweber Dec 30 '15 at 5:00

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.

  • $\begingroup$ Do we need a unary predicate for "identity arrows"? $\endgroup$ – hardmath Dec 29 '15 at 21:25
  • 3
    $\begingroup$ @hardmath No, an identity arrow is one satisfying $\alpha=s(\alpha)$ (or $\alpha=t(\alpha)$). $\endgroup$ – Noah Schweber Dec 29 '15 at 21:28
  • 2
    $\begingroup$ A variant on this definition (which even avoids including $s$ and $t$ in the language) is used in Freyd's book Abelian Categories, published in 1964. That might be the first place it was written down (it is for a surprising number of ideas in category theory!). $\endgroup$ – Eric Wofsey Dec 30 '15 at 5:06
  • $\begingroup$ Very helpful. Who ever knew that category theory was so simple! $\endgroup$ – Wildcard Aug 15 '16 at 6:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.