Programming with Categories • Hacker News Board

Re: Programming with Categories

#21

Post by random3 » Wed, Sep 02, 2020, 5:56 PM UTC

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

Re: Programming with Categories

#22

Post by tombert » Wed, Sep 02, 2020, 5:58 PM UTC

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.

Re: Programming with Categories

#23

Post by mindcrime » Wed, Sep 02, 2020, 5:58 PM UTC

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?

Re: Programming with Categories

#24

Post by marcosdumay » Wed, Sep 02, 2020, 5:58 PM UTC

Thanks for replying. I gave up on the beginning because those jokes tend to always be the same.

(And to be fair, half of them are the same overused ones. But the others are good.)

Re: Programming with Categories

#25

Post by johncolanduoni » Wed, Sep 02, 2020, 6:00 PM UTC

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.

Re: Programming with Categories

#26

Post by mindcrime » Wed, Sep 02, 2020, 6:00 PM UTC

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.

Re: Programming with Categories

#27

Post by dkarl » Wed, Sep 02, 2020, 6:00 PM UTC

As so many undergraduate math textbooks say, "No background is assumed beyond sufficient mathematical maturity."

Re: Programming with Categories

#28

Post by aruss » Wed, Sep 02, 2020, 6:05 PM UTC

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.

Re: Programming with Categories

#29

Post by picklenerd » Wed, Sep 02, 2020, 6:07 PM UTC

This is almost every upper division undergrad math class. It was always fun watching people squirm when they pulled out some useful fact from their past 14 years of math education and then got told they had to prove it before they could use it.

Re: Programming with Categories

#30

Post by fractionalhare » Wed, Sep 02, 2020, 6:26 PM UTC

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