What is category theory?
I have read the page about category theory in wikipedia carefully, but i don't really get what this theory is.
Is category theory a content in ZFC-set theory? (Just like measure theory, group theory etc.) If not, is it just another formal logic system independent from the standard ZFC-set theory?
Following wikipedia, i think it is the latter one.
If category theory is another formal logic system, then is there any theorem that relates category theory and ZFC-set theory? For example, there is a theorem states that "every theorem about sets in NBG is provable in ZFC, assuming consistency of ZFC" even though NBG and ZFC are completely different set theory. Moreover, is there a theorem which tells the relation between consistencies of ZFC and category theory? Also, is the usual independence proof in ZFC no more available in category theory?
Moreover, how does one write a formula in ZFC-set theory in category theory and vise versa? Since there is no undefined notion: set in category theory, i think this is not possible..
That's a question. Well for start as shown in Mac Lane Categories for the working mathematician there are two different way to approach categories, functor and natural transformations:
- you can either regard categories as some family of sets and operation between them (eventually adding some axioms to set theory since you would like to work with large collections like the class of all sets)
- or you can define categories as those structures which satisfy the axioms of the elementary theory of categories, which is a theory in first order (multi sorted) logic.
Of course if you use as meta-theory ZFC (actually at least NBG for the size problems I've mentioned above) then the two definition are essentially the same, and so you can see category theory as a theory developed inside set theory. Nonetheless just because we can interpret the axioms of category theory inside a set theory doesn't mean that we have to do so. Indeed we can interpret category theory axioms in other foundational theories such as dependent type theory.
From another perspective if we add to the axioms of category some other axioms we can get the first order theory of a topos with some other stuff (natural number object, axiom of choice [expressed as the property that every epimorphism is split]...) we get the axioms that characterize a category with enough structure to be almost equivalent to $\mathbf{Set}$, the category of sets and functions between them. In such theory we can develop all the usual constructions of set theory and so this theory (of a special category) can be used as a foundational theory itself.
So we have two ways to look at categories: as structures in set theory and as theories of structures, some of which can be used to rebuild mathematics.
This second way to look at category theory is really interesting in particular in connection with the study of constructive mathematics, since the theory of particular categories allows one to build constructive foundational theories, and category theory gives also the means to compare and study these theories.
I could say more but I don't want to be too long. Here are some references:
the two definitions of category (axiomatic vs set-theoretic) can be found in Mac Lane's Categories for the working mathematician
for the use of category theories as a foundational theories I suggest you take a look to this short post of Leinster and his related paper on arxiv.
For more about the interaction between category theory and set theory you can also google a little bit, some keywords for the research could be categorical logic, topos theory, foundation of category theory, category theory as foundational theory.
Hope this helps.
A useful resource is http://plato.stanford.edu/entries/category-theory/ which aims to explain something of the role and nature of category theory at an introductory but not merely arm-waving level.