Short answer: category theorists often elide the extra annotations when employing typical ambiguity or universe polymorphism. Proof theorists demand that these annotations be provided, and study how they behave.
If you want to be pedantic, then you have to annotate all instances of "category of sets" or "category of categories" with the additional word "small". Then the objects of the category of small sets do not form a small set, and the category of small categories is not a small category.
The next step is to replace "small" with an arbitrary natural number, where the objects of the "category of 0-small sets" form a 1-small set. Often, when fully annotated, it turns out that a proof will work for any value of "N" (where all the references to Set or Cat in the proof involve "offsets" from that N, such as "(N+3)-small sets"). Proofs which are parametric in this N (or some sequence N,M,... with inequality constraints between them) are called universe-polymorphic proofs, and are quite similar to a phenomenon in Principia Mathematica called typical ambiguity (although PM asserted a staggeringly powerful axiom about typical ambiguity without any sort of formal justification). You can re-apply these proofs at arbitrary levels in the transfinite hierarchy of universes, and they still hold.
That said, nobody has yet proven that a category of ALL categories (of every "smallness") cannot exist in the way that Russell proved that a set of all sets cannot exist. However, there is some evidence that you would have to omit certain axioms that might seem to be "obvious" at first glance.
No comments:
Post a Comment