What primitive notions and system of logic are used in Category Theory?

Question

I can formally study many subjects in mathematics (e.g. real analysis, group theory, linear algebra) using only ZFC which itself is an axiomatic system in first-order predicate logic with only a few primitive notions like equality, membership etc. but since category theory seems to involve an extension of ZFC by using things called "categories" (they behave kind of like classes) among other notions. I am curious to know what exact logic and primitives are needed to develop the theory of categories? Is it still just first order logic (since I know you can develop a theory of classes using first order logic and primitive notions of class)? Is it second order logic? Something else entirely?

Answer 1

ZFC is fine for small categories. A small category is an algebraic object in almost exactly the same way a group is except that it's two-sorted instead of one-sorted: it's a pair of sets (the objects and the morphisms) together with some maps (source, target, composition) satisfying some equational axioms. It is, if you like, a cross between a graph and a monoid. You talk about small categories in ZFC in exactly the same way you talk about graphs or groups or whatever other "ordinary" mathematical structures.

A large category is almost the same sort of thing except you need to use proper classes. This gets a little funky when you want to state theorems about large categories since you need to be able to quantify over proper classes to say things like "every functor between categories which is a left adjoint preserves colimits" and strictly speaking you cannot do this in ZFC; you need to work in a theory like NBG that explicitly axiomatizes proper classes and quantification over them.

Honestly, this doesn't seem to matter much in practice; you can learn and successfully apply tons of category theory without learning the details of any particular foundational theory that actually lets you quantify over proper classes (I still don't know the details of any such theory!), beyond just remembering that there is a difference between sets and proper classes.

You can check out Mike Shulman's Set theory for category theory for some actual details. The discussion of large categories and proper classes begins in section 6 on page 10.