4 ms·
It might help to consider the history of types and sets. Sets (and consequently modern math and logic) have not been around for as long as we might think. Mayb
by amw-zero 5y ago
It might help to consider the history of types and sets.
Sets (and consequently modern math and logic) have not been around for as long as we might think. Maybe we had them in different forms, but sets as we know them today were born in 1874 in this paper: https://srjcstaff.santarosa.edu/~jomartin/IrratFiles/Cantors1874Paper.pdf https://srjcstaff.santarosa.edu/~jomartin/IrratFiles/Cantors....
Around 1901, Bertrand Russell discovered a paradox in this formulation of sets, so-called Russel's Paradox: https://en.wikipedia.org/wiki/Russell's_paradox https://en.wikipedia.org/wiki/Russell's_paradox. There are then many ways of dealing with this paradox. The most widely accepted way is to just reformulate the axioms, which was done with Zermelo-Frankel set theory: https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t.... When people use the word "mathematics" today, they generally implicitly mean that ZFC is being used. It's the most widely accepted mathematical foundation we have.
Another path was proposed by Russell himself, and that is the notion of "type." By restricting the way in which certain operations and their arguments can be considered "valid," his own paradox can be avoided.
So from the beginning, sets are about _collecting_, and types are about _restricting_.
- ProfHewitt 5y agoTypes are about rigorously constructing mathematical abstractions from primitive types defined up to a unique isomorphism. In fact, types have become the primary foundation of Computer Science. Russell introduced the crucial concept of the order of a proposition to block his famous paradox as follows: Without orders on propositions, the paradoxical predicate I’mNotSelfApplicable (such that I’mNotSelfApplicable[I’mNotSelfApplicable]⇔¬I’mNotSelfApplicable[I’mNotSelfApplicable]) could be constructed using the following recursive definition: I’mNotSelfApplicable:Predicate<i>≡¬I’mNotSelfApplicable[I’mNotSelfApplicable] Since I’mNotSelfApplicable is a predicate variable in the definition, ¬I’mNotSelfApplicable[I’mNotSelfApplicable]:Predicate<i+1>. Consequently, I’mNotSelfApplicable:Predicate<i>⇒I’mNotSelfApplicable:Predicate<i+1> which is a contradiction meaning that I'mNotSelfApplicable does not exist. See video: https://www.youtube.com/watch?v=AJP1VL7shiI https://www.youtube.com/watch?v=AJP1VL7shiI
- ProfHewitt 5y agoUnfortunately, 1st-order ZFC has very severe limitations because it does not precisely define sets. However, ordinals that provide the backbone of sets have been precisely defined up to a unique isomorphism using types. See the following article: "Theory Ordinals can Replace ZFC in Computer Science" https://papers.ssrn.com/abstract=3457802 https://papers.ssrn.com/abstract=3457802
- amw-zero 5y agoEverything has limitations. I deeply trust the system that has served us extremely well over the last 150 years.
- ProfHewitt 5y agoOrthodoxy in science works until the next paradigm shift. See "In retrospect: The Structure of Scientific Revolutions" https://www.nature.com/articles/484164a https://www.nature.com/articles/484164a
- BoiledCabbage 5y agoIt almost seems like Type theory is a better foundation than set theory but we ended up with set theory due to historical accident.
- amw-zero 5y agoI don’t believe in historical accidents. We “ended up” with set theory because it’s an incredibly rich system that has powered almost every important mathematical discovery in the last 150 years. We use it because it is the most effective tool for formal reasoning that human beings have ever come up with. The fact that it has limitations, especially in the new world of computation, does not take away its utility. To me, sets seem like the much more foundational idea, since types were only suggested as a fix for Russell’s paradox. Almost all math can be done without ever running into the limitations of Russel’s paradox, so I look at type theory as more of an evolution of the understanding of sets than anything else.
- ProfHewitt 5y agoSets initially seemed appealing because they are less abstract than types. However, the lack of abstraction turned out to be a fatal flaw in attempts to make sets the foundations of mathematics because: * sets cannot be rigorously defined using 1st-order ZFC * sets cannot be used to define higher-level abstractions of mathematics
- ProfHewitt 5y agoBoiledCabbage: You are on the right track! [Dedekind 1888] started out on the correct path by defining natural numbers up to a unique isomorphism. Unfortunately, there was long detour through 1st-order logic :-( Powerful foundations are now urgently required to prevent successful cyberattacks. See the following: https://www.youtube.com/watch?v=AJP1VL7shiI https://www.youtube.com/watch?v=AJP1VL7shiI