[linkdd]

I've read a lot about Category Theory, and I'm amazed at the abstraction level that lets you compose with different mathematical domains (geometry, topology, arithmetic, sets, ...).

And yet, the current mathematics relies heavily on the ZFC set theory. Why is that ? (Is that assumption even correct ?)

From what I've learned so far, the set theory suffers from Russel's Paradox[0] (does the set of all sets that does not contain itself, contains itself ?). That's what motivated the formalization of Type Theory and the invention of Type Systems in programming languages.

According to wikipedia[1], some type theories can serve as an alternative to set theory as a foundation of mathematics.

It seems to me that the Category Theory fits the description. So why don't we see a huge "adoption" in math fields ?

Thank you in advance for your clarifications :)

[0] - https://en.wikipedia.org/wiki/Russell%27s_paradox [1] - https://en.wikipedia.org/wiki/Type_theory

[johncolanduoni]

ZFC does not suffer from Russel’s paradox, since it doesn’t allow a “set of all sets”. If it did, the search for new foundations would be much more widespread. New foundations are usually only considered seriously once they can be shown to be relatively consistent with ZFC or the slightly stronger but still uncontreversial TG set theory.

There are people working on categorical foundations, but the main reason for lack of broader popularity or drive is that most mathematicians don’t do work that is “foundational” in that sense. For example, if you’re an analyst, you generally don’t care exactly how your real numbers are built (dedekind cuts, Cauchy sequences, etc.). You only care that they satisfy a certain set of properties, you can define functions between them, and that’s about it. Most mathematical reasoning at this level is insensitive to differences in proposed foundations, except “constructive” foundations that don’t have the law of excluded middle (that are unpopular since they make many proofs harder and some impossible).

What is very popular in mathematics is using category theory at a high level; basically every field uses its concepts and notation to some degree at this point. New foundations are only really relevant to this program in that they may make automated proof checking easier, which is also not a widespread practice in mathematics.

[spekcular]

It is not true that "basically every field uses its concepts and notation to some degree at this point." In particular this is false for mainstream combinatorics, PDE, and probability theory, to give a few examples.

In fact, I would suggest that most mathematicians don't care about category theory at all.

[bitdizzy]

This all hinges on "mainstream". For example, in combinatorics, combinatorial species are a vast organization of the all-important concept of generating function. They were developed by category theorists and are most tidily organized along categorical lines. If you don't think this is close enough to mainstream, I can't dispute that. It's a value judgment.

There is often an undercurrent of category theory within a subject that maybe most people are not privy to. Anything to do with sheaves or cohomology (which I know factors into some approaches to PDEs) are using categorical ideas.

Every generation, it seems, has some contingent of serious mathematicians who consider category theory marginal in their field of interest. But every generation, that contingent grows smaller as more mathematics as practiced is brought into the fold. Maybe they're coming for you next :)

[spekcular]

Respectfully, I disagree. The question of what's mainstream and valued by the community is empirical and can be answered by looking at what's published in the leading combinatorics journals. And anyone can check those out and see that categories are basically absent. So as a sociological fact, I maintain it's far from the mainstream.

Whether combinatorialists ought to elevate certain work is of course of a question of value, but it's also a different question.

Also, in no way are sheaves or (co)homology essentially category-theoretic ideas. It's possible to develop and use these ideas without mentioning categories at all (and e.g. Hatcher's introductory textbook does just this, although he mentions in an appendix the categorical perspective later). In general I think it's good to remember that homological algebra and category theory are not the same subject. Sure, I can develop a theory of chain complexes over an arbitrary abelian category, but most of the time you just need Hom and Tor over a ring. (Again, see Hatcher.)

Finally, I'm not sure there has been a serious uptake in category theory in the mainstream of some field of mathematics since, I don't know, at least 50 years ago? We've understood for a while now what it's good and not good for. This hasn't stopped people from trying to inject it in fields where it doesn't do any good (e.g. probability), but for that reason those attempts are mostly ignored.

[bitdizzy]

> Respectfully, I disagree. The question of what's mainstream and valued by the community is empirical and can be answered by looking at what's published in the leading combinatorics journals. And anyone can check those out and see that categories are basically absent. So as a sociological fact, I maintain it's far from the mainstream.

I think it is also a reasonable interpretation to take "mainstream" as "pertaining to the main subject matter of the field". Anyway, I think it is the case that the mainstream of combinatorics or probability is yet so big that a particular researcher or even group of researchers can be comfortably in the mainstream and yet have never cared for or even heard of some other line of research that is also mainstream.

The founding paper of combinatorial species [1] has hundreds of citations including many in what I gather are top journals in combinatorics, and even some in the Annals of Probability. So, what are we to make of that? Some people who are serious enough about combinatorics or probability to get published in serious journals have read, perhaps understood, and maybe even taken seriously some of these categorical ideas?

In any case, I respect your viewpoint. In my youth I was a bit category-crazy, trying to use it to organize all of my mathematical knowledge. I'm much more prudent about it these days but I'm still an optimist that we will find more unifying ideas in mathematics through it.

[1] https://www.sciencedirect.com/science/article/pii/0001870881...

[spekcular]

It may the case that combinatorics is large, with mathematicians focused on their own particular sub-specialities, but I still don't believe category theory can properly be construed as "mainstream combinatorics" in any real sense.

Regarding your claim about that paper being cited by papers in top journals, I checked the first five pages of citations in Google Scholar for combinatorics and probability journal papers.

It's cited once in an offhand way in the concluding discussion of "The Cycle Structure of Random Permutations." No categorical concepts are used there. Ditto for the "Independent process approximations" paper (except now cited in the introduction). Another one-sentence mention in the context of background literature appears in "Tree-valued Markov chains derived from Galton-Watson processes." Same for "A Combinatorial Proof of the Multivariable Lagrange Inversion Formula" and "Bijections for Cayley Trees, Spanning Trees, and Their g-Analogues."

There's a one-sentence mention with actual (slight) mathematical content in "Limit Distributions and Random Trees Derived from the Birthday Problem with Unequal Probabilities." But you don't need categories to prove the bijection they're referring to, from what I understand.

In none of these instances is the work used in a substantive fashion, and unless I missed something no paper features the word "category." It's getting cited because authors have a duty to survey any potentially related background literature.

(On page 6 I found "Commutative combinatorial Hopf algebras," which does use a functor form that paper. It was published in a journal that is decent, but very far from the top.)

So, I think we can reject the notion that Joyal's paper has seriously influenced the fields of combinatorics or probability.

I'm sorry to harp on this, but I see claims like yours about the importance of category theory thrown around a lot on here, and often I feel that they're clearly wrong. So I thought it would be good to provide some details this time around.

[Koshkin]

> most mathematicians

Agree, but only on the level on which they do not care about the abstract math (algebra, topology, etc.) in general. As soon as you step into the territory of the abstract math, especially where different disciplines blend, such as homology and cohomology, category theory (and its diagram language) helps a lot to clarify things. (Incidentally, a lot of this stuff is now part of the "applied math" as well, having found its way into theoretical physics, for example.)

[spekcular]

I'm not sure I'm comfortable characterizing the fields where category theory is useful as "abstract math." Modern PDE is plenty abstract, for example. Probably it's better to say that the usefulness of category theory is proportional to the problem's distance from algebraic topology and algebraic geometry.

I also am reluctant to characterize theoretical physics as "applied math." I haven't seen anyone who calls themselves an applied mathematician use category theory in a substantive way (where here I am thinking about numerical computing, mathematical biology, and so on).

[joe_the_user]

I have only an MA in math - but I have the impression mathematicians can be arranged on spectrum between ad-hoc theorem provers and giant machinery builders, between those like Paul Erdős and those Alexander Grothendieck.

The thing to keep in mind is that a mathematical structure can be expressed as instance of any number of more general mathematical structures ("mathematical machinery"). The structures that useful, however, are those that are "illuminating", a somewhat vague criteria but one which generally include a structure facilitates and unifies proofs of important theorems. Wiles' proof of Fermat's Last Theorem showed the value of many forms of this mathematical machinery [1], including category theory.

At the same time, I think things like Godel theory of cutting down proofs and Chaitin's Omega constant give a suggestion that the some number of "important" theories within a given axiomatic system will have long proofs that don't necessarily benefit from the application of a given piece of mathematical machinery, whatever that machinery.

And think that's related to efforts to apply category theory to programming via functional programming. I feel like it's an effective method for certain kinds of problems but that you get a certain problematic "it's the best for everything" evangelism that doesn't ultimately do the approach favors.

[1] https://en.wikipedia.org/wiki/Wiles%27s_proof_of_Fermat%27s_...

[Twisol]

> From what I've learned so far, the set theory suffers from Russel's Paradox

So-called "naive set theory" does, but my understanding is that this paradox (and others like it) sparked a crisis in mathematics that led to the creation of ZFC and others. ZFC is not known to be inconsistent (due to deep and technical reasons, I can't claim positively that it is consistent), and it was designed to avoid the paradoxes that plagued naive set theory.

Russell's type theory was another early contender for a formalism. For whatever reason (I'm not aware of all the details), Zermelo-Fraenkel set theory (later extended with the Axiom of Choice) won the popular mindshare. Personally, I'm more a fan of the Elementary Theory of the Category of Sets (ETCS) [1], which is indeed drawn from category theory. But it's equivalent in deductive power to ZFC, so what you pick mostly only matters if you're doing reverse mathematics. (This is what really answers your question, I think.)

Russell's type theory and modern type theories are distinct (and there is no single "type theory"). I'm led to believe the commonality is primarily with the usage of a hierarchy of universes, so that entities in one unverse can only refer to entities in a lower universe.

[1] "Rethinking set theory", Tom Leinster: https://arxiv.org/abs/1212.6543

[mindcrime]

but my understanding is that this paradox (and others like it) sparked a crisis in mathematics that led to the creation of ZFC and others. ZFC is not known to be inconsistent (due to deep and technical reasons, I can't claim positively that it is consistent), and it was designed to avoid the paradoxes that plagued naive set theory.

That was my understanding as well. Axiomatic Set Theory, with ZFC, doesn't suffer from the same problems as Naive Set Theory, which is why it was developed. Or so I've read.

[fractionalhare]

> And yet, the current mathematics relies heavily on the ZFC set theory. Why is that ? (Is that assumption even correct ?)

Set theory is the de facto modern standard because it has straightforward notation and sufficient power to prove the things most mathematicians care about, both algebraically and analytically. Other foundations exist, it's just that most mathematicians work at a level where set theory is more of a communication and notation tool than a foundation for which the nuances matter.

> From what I've learned so far, the set theory suffers from Russel's Paradox[0] (does the set of all sets that does not contain itself, contains itself ?).

No, naive set theory suffers from Russell's Paradox, but ZFC does not. ZFC was defined in order to avoid Russell's Paradox.

> That's what motivated the formalization of Type Theory and the invention of Type Systems in programming languages.

Russell's type theory, yes, which predates ZFC. But this has nothing to do with programming languages, which weren't a thing when this problem was being considered.

As for why category theory isn't used as a foundation - that's not really what category theory's "charter" is about. As user johncolanduoni explained, category theory is more of a framework for describing things with convenient algebraic abstractions than it is a foundation for mathematics. Category theory as practiced today is mostly done at a higher level than the foundational set theory.

[mindcrime]

IANAM, but...

1. I thought mathematics was moving more towards a category theory based foundation, as opposed to the set theoretical stuff.

2. Isn't it in part because we have over 120 years of results and proofs that are based on set theory, and people aren't just going to throw that out for something newer? Granted, Category Theory has been around in some form since about the 1940's, but it's still newer than set theory.

3. Russell's Paradox hasn't stopped people from using Set Theory to achieve useful results, and the axiomatization of Set Theory and the advent of ZFC is why (or at least part of why) that was possible, no?

[spekcular]

1. It's not. The work on "category-theoretic foundations," say HoTT, is (sociologically speaking) a highly niche topic. Most professional mathematicians who work on the foundations of mathematics do so in the framework of set theory.

2. ZFC is fully adequate for all the mathematics 99% of professional mathematicians do (and probably more than adequate in terms of strength). Also, all the mathematics 99% of mathematicians do is insensitive to foundational issues, so if you swapped ZFC for another axiomatization of similar strength, no one would notice.

3. I don't believe ZFC was the first to avoid the paradox, but yes, it does not suffer from Russell's Paradox.

[mcphage]

> So why don't we see a huge "adoption" in math fields ?

Because most math fields work at a higher level, and whether they consider set theory or category theory foundational doesn't matter. For instance, the defining property of ordered pairs is: `(a, b) = (c, d) iff a = c and b = d`. {a, {a,b}} is a (set-theoretic) model for ordered pairs, but it's not the only model. As long as a model exists, the question of "which model you're using" isn't relevant.

[lmm]

> And yet, the current mathematics relies heavily on the ZFC set theory. Why is that ? (Is that assumption even correct ?)

Not really. Most working mathematics is done without any particular foundational context (in fact, it's probably done in naive set theory). If you asked a mathematician, they'd tell you they were using ZFC, but only because everyone does; in practice they don't know or care what foundations they're working with.

> From what I've learned so far, the set theory suffers from Russel's Paradox[0] (does the set of all sets that does not contain itself, contains itself ?). That's what motivated the formalization of Type Theory and the invention of Type Systems in programming languages.

Naive set theory suffers from that paradox. ZFC is a minimal "patch" that avoids it (through the rather ugly hack of an axiom schema).

It shouldn't surprise any programmer that most people working in the field would rather use a bodge that lets them use all their existing theorems and avoid having to learn anything new, rather than a new foundational paradigm.

People who care deeply about foundations are working on things like HoTT. But it's just not that important to day-to-day working mathematicians.

[tombert]

ZFC Set Theory avoids Russell's paradox by having a few fundamental axioms that preclude it. It's actually mentioned in your wiki link in the `Set-theoretic responses` section.

ZFC is a bit messy sometimes, but it's actually kind of nice in its simplicity. I am a big fan of TLA+, for example, and it's really kind of beautiful how easily you can define incredibly precise invariants by using the set theory predicate logic.

[hwayne]

I once asked a logic professor I'm friends with and he spent fifteen minutes ranting about large ordinals and reverse mathematics and non-absolute logics. Apparently there is some incredibly weird stuff at the fringes of logic that we only really know how to handle in ZFC.

This is purely secondhand, of course, and I forget almost all of the details. Contemporary set theory is scary scary stuff.

[random3]

I think the current fundamental structures are influenced by the Bourbaki group, however it has gaps. Category Theory is likely able to fill those gaps and I guess it will end up as the foundational layer of both mathematics, computer science, and pretty much everything else. David Aubin wrote about this in https://press.princeton.edu/books/hardcover/9780691118802/th... (VI.96) Some discussions too here https://math.stackexchange.com/questions/25761/introduction-....

[housecarpenter]

It may be worth explicitly noting that category theory and set theory are not mutually exclusive. You can use set theory as the foundation, and build category theory on that, and then use category theory to do all that interconnection of fields and whatnot. To me it seems like the most natural way to do it, because set theory is simple and intuitive (kind of), whereas category theory is complicated and extremely abstract.

(Of course there is a lot of stuff in set theory that is counter-intuitive when you get to infinite sets, but I still think that's better than what you have with categories where they're just abstract algebraic objects and there isn't any intuition in the first place.)

[aruss]

Category theory isn't a type theory (in the sense that you can have the category of categories, which correspond to different type theories).

It's true that you can get away from Russell's paradox in category theory, but that's because categories are not sets and have different properties (there's less you can say about them because they're more general).

Type theories, particularly homotopy type theory, are becoming popular among some mathematicians, but not because they escape Russell's paradox (I'm not sure that they can say anything more about sets than set theory), but because they are more useful when constructing automated proof systems.

Edit: also, category theory is used a lot in very cutting edge math, like algebraic topology.

[AnimalMuppet]

> That's what motivated the formalization of Type Theory and the invention of Type Systems in programming languages.

I don't think that's right. The original invention of type systems in programming had nothing to do with Type Theory. The motivation wasn't from any theory. The point was to tell Fortran whether to treat a value as an integer or a floating-point number, which affected storage format and a bunch of other things. (Before Fortran, there was floating-point arithmetic, but the type was still just a computer word. The programmer had to keep track of what format it was in.)