4 changed tags
3 spelling

CategorialCategorical foundations without set theory

2 highlighted a concern that first order axiomatiztion is not enough to say categories can be formulated independently of sets

J Williams in his answer below noted that via metacategories, we can have a first order axiomatization of categories. However, this does not provide a foundations of mathematics using only category theory, since set theory permeates the formulation of first order logic. In first order logic, structures are sets together with constants, functions and relations. Here constants, functions and relations are also sets. So even if we say that categories are first order axiomatizable, at the very end, categories are still defined in terms of sets.

I admit in wanting foundations totally in terms of categories, then there will be some kind of recursiveness. However, this recursiveness should not be seen as a problem since as described above, first order axiomatization of sets like ZFC, are written in the language of first order logic which (at least in a meta-level) are sets themselves. In fact, this recursiveness is very much a feature of symbolic logic and is partially responsible for the successful that a single primitve concept of set/set-membership can describe so much (or all?) of mathematics.

I'm aware also in certain proofs of equivalence of categories in mainstream math, like GAGA theorems by Serre, there is a need to use categories where the objects are of classes of different levels, like the NBG set theory. In the end, the reasons provided for why the argument of using classes can be pushed down to essentially small category, this in the end invokes NBG set theory.

So precisely, here is my question. Can a category be defined without saying that the objects and morphisms are classes or sets? By asking this, I admit there will be some kind of recursiveness in the answer, in some way, these objects and morphisms must then be categories themselves, but possibly of a simple kind.

This recursiveness should not be seen as a problem since in the orthodox symbolic logic of today, a set theory like ZFC is defined in term of first order axioms, which themselves need at least a minimum of PA or some of kind coutable choice even to set up the framework of first order logic.

1