# What is the Relevancy of Other Foundations of Mathematics Besides ZFC

In mathematics, ZFC set theory has made a significant splash; it has lead the way for very important concepts such as the incompleteness theorem, the continuum hypothesis, aleph numbers, and innumerably many other things. However, other foundations of math, such as HoTT and category theory, haven't brought forth such significant results that I know of (save applications in computer science). Has HoTT, Category Theory, or any other foundation besides ZFC yeilded significant results or have the potential for significant results? Thanks in advance!

• Incompleteness has little connection with ZFC. – André Nicolas Aug 8 '16 at 17:25
• @AndréNicolas I was more referring to how set theory led to the theorem, as opposed to being used in the proof itself. – Stephen Fratamico Aug 8 '16 at 17:34
• If extensions of $\operatorname{ZFC}$ count - they're used all the time in set theory to obtain interesting and significant results. Assuming large cardinals to prove (the consistency of) theorems and, on the other hand, showing the necessity of such assumptions is a key area in modern day set theory. – Stefan Mesken Aug 8 '16 at 19:49
• @Stefan Thanks for the answer! Could you elaborate with a direct example or possibly a link? – Stephen Fratamico Aug 9 '16 at 3:15
• Well, category theory isn't a foundational theory in the way that ZFC or HoTT are, so expecting it to produce the same kinds of theorems misses the mark. – Malice Vidrine Aug 9 '16 at 4:35

First of all, to correct a common misconception: category theory is not a foundation for mathematics. Category theory is a language that can be used to describe lots of kinds of mathematics, including some foundations of mathematics, such as Lawvere's Elementary Theory of the Category of Sets; but those foundations are not the same as category theory.

Second, I would say that one reason ZFC gave rise to so many important consequences is that it was the first precise foundation for mathematics. In some sense, this is a historical accident; in principle another foundation such as ETCS or type theory could have been developed first, and in that case it would have been that foundation giving rise to all those significant developments, most of which are largely insensitive to the particular foundation of mathematics in which they are formulated.

Now that we are familiar with the notion of "foundation of mathematics", and many of the benefits of having such a foundation have already been reaped, we shouldn't expect "new" foundations to impact mathematics in the same way that ZFC did. Instead, their effects will be more incremental: providing better ways to formalize certain parts of mathematics, or enabling new mathematics that wasn't possible in ZFC. But this does not mean that, taken in their own, they are any less "foundational" than ZFC.

• Let me air some tangential frustration of language. I don't now of any mathematics which cannot be formalized in some extension of ZFC (I'm including things like NF which is still open as to whether or not it is consistent relative to any known theory). In other foundations this is slightly less pronounced because you sort of assume various large cardinal equivalents from the get go (read: universe like types, objects and so on). But ultimately, is there an actual example of something that we don't know how to interpret as sets in a sufficiently strong extension of ZFC? – Asaf Karagila Aug 9 '16 at 15:41
• @Stefan: I was led to understand that this is perfectly doable if you have some inaccessible cardinals lying around (infinitely many? class of them?). At least when talking about objects below the first inaccessible or something like that. Which for me, as far as things go, is a perfectly valid way to formalize something. – Asaf Karagila Aug 9 '16 at 15:51
• @Stefan: If nothing else, whatever your set theoretic inclination, adding "there is a proper class of inaccessible cardinals" is not a huge leap of faith. I agree it is tricky, but not to say it cannot be done entirely. – Asaf Karagila Aug 9 '16 at 15:59
• @AsafKaragila Synthetic homotopy theory, using univalence and higher inductive types, cannot be formalized directly in ZFC. True, one can invoke the theorem/conjecture that HoTT/UF has models in ZFC to translate it into statements that make sense in ZFC, but that's different from actually formalizing it as written. I'm not claiming the dividing line is perfectly sharp, but there is at least a continuum, and synthetic homotopy theory is way off on the other end of it. In particular, I think it's fair to say that no one equipped only with ZFC would have invented synthetic homotopy theory. – Mike Shulman Aug 9 '16 at 16:59
• Mike, just for the sake of clarity (and again, my gripe with the natural language semantics of these discussions). When you say "directly in ZFC" do you mean "pure ZFC" or "ZFC+whatever reasonably sounding large cardinals you want"? And I'm not arguing that language is the basis of thought, and a different language can therefore allow you to come up with new ideas. – Asaf Karagila Aug 9 '16 at 17:02

A meta comment: Zermelo set theory was initially developed over a century ago. HoTT has only been around a decade or so. Gödel's incompleteness theorems were published in 1931, over two decades after Zermelo set theory was initially developed. It seems a bit unfair to expect that HoTT should have already produced similarly groundbreaking new results.