Is the axiom of universes 'harmless'?
Usually when you start studying category theory you see the usual definition: a category consists of a class $Ob(\mathcal{C})$ of objects, etc.
If you take ZFC to be your system of axioms, then a "class" (a proper one) is something which you can't formally use, since everything in the universe of discourse is a set.
Some people (MacLane? Grothendieck?) were understandably worried about this. Cutting down on the history which I am unqualified to give an accurate account of, there is the definition of Grothendieck universe.
If we add the following axiom of universes to ZFC, then we can get around having to use classes:
Axiom of universes (U): every set is contained in some universe.
Now, it can be proven that the axiom of universes is equivalent to the
Inaccesible cardinal axiom: for every cardinal μ, there is an inaccessible cardinal κ which is strictly larger.
which was proven to be independent of ZFC. Hence we can work in ZFC+U and do category theory with the concern of dealing with proper classes put at rest.
This seems to be now a standard approach to a good foundation of category theory.
My question, to put it informally, is: how innocent is the axiom of universes?
What I mean by this is: how do we know it does not have unexpected consequences which may alter the rest of mathematics? The motivation was to give a good foundation of category theory, but it would be unreasonable to give a great foundation that altered the rest of ordinary mathematics.
To give an example, we now that adding the axiom of choice to ZF has some startling consequences. For example, the Banach-Tarski paradox. How do we know that ZFC+U does not have some equally startling consequences? Why are we at rest with adding this axiom to our foundation of mathematics? Isn't this a rather delicate question? How much do we know about how good is the universe approach? (I would say a foundation for category theory is better than another one if it solves the 'proper classes issue' and it has less impact on the rest of mathematics.)
Solution 1:
What I mean by this is: how do we know it does not have unexpected consequences which may alter the rest of mathematics?
I will give a couple remarks, and also link to these MathOverflow discussions:
Recent claim that inaccessibles are inconsistent with ZF
Reasons to believe Vopenka’s principle/huge cardinals are consistent
(1) In set theory, the study of large cardinals (much "larger" than just inaccessible) has been very fruitful. The existence of many of these large cardinals requires the existence of inaccessibles. So set theorists are interested in these large cardinals because of their useful (perhaps "startling") consequences. If there were no interesting consequences, set theorists would find other things to look at.
(2) From the skeptical POV, we don't know what the consequences might be. It could be that ZFC is consistent but ZFC plus the universe axiom is inconsistent. Many people come to feel that they have some intuition that the existence of universes is not inconsistent with ZFC. This belief often comes from thinking about the way that the cumulative hierarchy works. On the other hand, there is a manuscript by Kiselev (link) in which he claims to prove that the existence of even one inaccessible cardinal is inconsistent with ZFC.
We do know that ZFC cannot prove that there is even one inaccessible cardinal. And we know we cannot prove in ZFC that the existence of an inaccessible is consistent, because of limitations coming from the incompleteness theorems. So any argument that inaccessibles are consistent will have to use methods that cannot be formalized in ZFC.
(3) Temporarily adopt a Platonistic perspective, at least for the sake of argument. From this position, each "axiom" is either true or false, but it cannot alter the properties of mathematical objects, which exist separately from the axioms used to study them. Of course we can prove false statements from false axioms, but we can't actually change the objects themselves.
(4) Now temporarily reject Platonism, and think only about formal proofs. Then it will not make any difference to my conception of mathematics if someone else adopts an axiom that I don't accept. I will simply put a * beside all the theorems that use this axiom, and count them as dubious at best. I might even reprove some of the theorems without the new axiom just so I know they are OK. In this way, my personal conception of mathematics would also be unchanged by other people using different axioms.
I think that (3) and (4) start to indicate the way that philosophical issues will enter in when we ask about the effects of different axioms on "mathematics".
(This answer is marked as community wiki, as I already gave a different answer for this question. Please feel welcome to add more links to the list of links above.)
Solution 2:
I will leave it to another user to discuss the exact strength of the universe axioms in set theory. There is a lot to say about that.
The thing that I want to point out is that, for the actual applications of the category-theoretic methods to number theory, such as Fermat's Last Theorem (FLT), it appears that the use of universes can be eliminated. For example, Colin McLarty published an article (ref, preprint) in the Bulletin of Symbolic Logic in 2010 in which he states:
"This paper aims to explain how and why three facts coexist:
- Universes organize a context for the rather explicit arithmetic calculations proving FLT or other number theory.
- Universes can be eliminated in favor of ZFC by known devices though this is never actually done (and this remains far stronger than PA).
- The great proofs in cohomological number theory, such as Wiles [1995] or Deligne [1974], or Faltings [1983], use universes in fact."
The key claim I want to highlight is (2): many people believe that methods using universes are not needed for concrete results such as Wiles' theorem, and in principle the proofs can be rewritten without them. I am in no position to judge the claim but it seems to be accepted by quite a few people who have looked into the matter. There is an open conjecture that Fermat's Last Theorem can be proved in Peano Arithmetic and even in much weaker theories, and at present we have no reason to suspect that FLT cannot be proved in Peano Arithmetic.
This makes the foundational question of universes more interesting: they are used, clearly, but working number theorists know how to avoid them if desired, which leaves a sort of tension. This is the issue McLarty is getting at in his paper.
McLarty's most recent progress announcement indicates he has made even more progress since his 2010 paper.