4 ms·

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, ar

by linkdd 6y ago

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 https://en.wikipedia.org/wiki/Russell%27s_paradox [1] - https://en.wikipedia.org/wiki/Type_theory https://en.wikipedia.org/wiki/Type_theory

Twisol 6y ago
> 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 https://arxiv.org/abs/1212.6543
- mindcrime 6y ago
  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.
random3 6y ago
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/the-princeton-companion-to-mathematics https://press.princeton.edu/books/hardcover/9780691118802/th... (VI.96) Some discussions too here https://math.stackexchange.com/questions/25761/introduction-to-bourbaki-structures-and-their-relation-to-category-theory#:~:text=Bourbaki's%20structures%20are%20anything%20which,of%20objects%20and%20their%20morphisms.&text=On%20the%20other%20hand%2C%20if,and%20structure%2C%20try%20model%20theory https://math.stackexchange.com/questions/25761/introduction-....
tombert 6y ago
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.
mindcrime 6y ago
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 6y ago
  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.
johncolanduoni 6y ago
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 6y ago
  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.
  - Koshkin 6y ago
    > 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.)
aruss 6y ago
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.
fractionalhare 6y ago
> 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.
mcphage 6y ago
> 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.
AnimalMuppet 6y ago
> 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.)
lmm 6y ago
> 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.
hwayne 6y ago
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.
housecarpenter 6y ago
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.)

by linkdd 6y ago

Twisol 6y ago

> 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 https://arxiv.org/abs/1212.6543

mindcrime 6y ago
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.

random3 6y ago

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/the-princeton-companion-to-mathematics https://press.princeton.edu/books/hardcover/9780691118802/th... (VI.96) Some discussions too here https://math.stackexchange.com/questions/25761/introduction-to-bourbaki-structures-and-their-relation-to-category-theory#:~:text=Bourbaki's%20structures%20are%20anything%20which,of%20objects%20and%20their%20morphisms.&text=On%20the%20other%20hand%2C%20if,and%20structure%2C%20try%20model%20theory https://math.stackexchange.com/questions/25761/introduction-....

tombert 6y ago

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.

mindcrime 6y ago

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 6y ago
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.

johncolanduoni 6y ago

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 6y ago
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.
- Koshkin 6y ago
  > 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.)

aruss 6y ago

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.

fractionalhare 6y ago

> 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.

mcphage 6y ago

> 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.

AnimalMuppet 6y ago

> 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.)

lmm 6y ago

> 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.

hwayne 6y ago

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.

housecarpenter 6y ago

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.)