Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
@JoelDavidHamkins If you think that it is just a convenient way and that there is a way to stay inside ZFC, I would be curious to know more about this subject. My informal observation comes also from the fact that an assistant proof like MIZAR uses Grothendieck universes. So that made me think that people working on reverse mathematics had proved that Grothendieck universes were necessary for the formal development of some parts of mathematics. It is all I know about this subject.
@JoelDavidHamkins My statement "ZFC alone is not sufficient to develop category theory" was an informal observation. It lies on the fact that one has to deal sometimes with "big" objects and "superbig" objects in the proofs. Maybe there is a way to avoid this big and superbig objects. The book "Homotopy Limit Functors on Model Categories and Homotopical Categories" from Dwyer, Hirscchhorn, Kan and Smith is another example of use of universes.
Do you mean the characterization of accessible categories by the categories of models of a basic theory ? You want to consider the category of all sets or of all groups, whatever the universes they belong to. That is not possible in ZFC: the set of all sets leads to a contradiction. And that is not necessary for mathematicians. So where is the issue ?
@Tom I think that nobody understands what you mean, just because there is no issue, even for computers. Indeed, the proof assistant MIZAR uses a variant of set theory called Tarski–Grothendieck set theory. Roughly speaking in this extension, there are as many Grothendieck universes as necessary.
A category is weakly (co)complete if (co)limits exist but are not unique. The homotopy category of a model category is weakly complete and weakly cocomplete. (I cannot understand why @Fernando does not appear when I write it at the beginning of the comment ; could someone help me to edit this comment ?)
I don't understand what you mean by homotopy limit $Fun(S,Ho(M))\to Ho(M))$. Do you mean a right adjoint of the diagonal functor ? Then this is just a limit. The homotopy category of any cofibrantly generated model category is weakly complete and weakly cocomplete, i.e. limits and colimits exist but are not unique. This is explained in M. Hovey's book Model Categories.
That periodicity of Laver's tables is unbounded is proved using large-cardinal axiom en.wikipedia.org/wiki/Laver_table: it is not a transfinite induction, so it is not exactly an answer to your question, but the only known proof requires transfinite techniques.
@PietroMajer It is actually easy to find a provable statement with a very long proof. I read somewhere that there are more than 10000 new theorems proved by year in the world. Take these 10000 theorems $T_1,\dots T_{10000}$. Then the proof of the statement $T_1 \hbox{ and } \dots \hbox{ and }T_{10000}$ should be very long. More interesting is the question whether the quotient of the length of the minimal proof by the length of the statement can be arbitrarily large. But I doubt very much that this question can be formalized.
@PietroMajer About "the shortest proof has by far more symbols than there are atoms in the universe" : I have a question, maybe too informal to be asked in MO (I don't know): is it possible to prove that there exist provable statements, let's say in ZFC, whose minimal proof (if such a thing makes sense) can be as long as we want ?
Your question has no answer. Or that depends what you mean by intuition. What is the intuition behind the number $\pi$ for example ? It is the surface of the unit disk. So what ? Is it helpful ? Do you have a better intuition of $\pi$ after that ?
