Timeline for In what respect are univalent foundations "better" than set theory?
Current License: CC BY-SA 3.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 22 at 7:21 | comment | added | Peter Gerdes | Mathematicians are utterly comfortable with the idea that one can view some objects differently or abstract away from particular questions of representation when they don't matter. Practically, what's important for the average mathematician for foundations is that in the rare situation they need to use it it's as intuitive as possible and comprehension and sets are intuitive while keeping track of types gets ugly in exactly the cases you need to turn to foundations to verify your reasoning. | |
| Nov 27, 2017 at 1:53 | comment | added | Carl Mummert | Of course, many mathematicians will also say that the question "is $\pi$ surjective" does not make such sense, and that the possibly clarifying question "do you mean the $\pi$ in $\{\pi\}$ or the $\pi$ in $\mathbb{R}$?" also does not make sense. (If this doesn't make sense: in systems where "elements" of a set are actually functions into the set, the question whether an element is surjective is very well formed, just as questions about $\pi \cap \sin$ are well formed in set theory.) | |
| Nov 26, 2017 at 10:22 | comment | added | Asaf Karagila♦ | @David: Yes, we probably agree more than people who don't know us very well would think. And yes, sophisticated proof assistants should include some implicit type casting. I am just sick and tired of the argument that "since you can formally write things which are type-mismatching in ZFC, it's not a great foundation for mathematics and therefore type theory is better". If we continue banging on the programming analogy, this would be to say that C is a bad programming language because you can write code which is a recursion without a valid halting clause. | |
| Nov 26, 2017 at 10:08 | comment | added | David Roberts♦ | @Asaf I think we don't disagree that much, I was just pointing out it is a feature of both approaches. Mathematicians in practice gloss over coercions where they have a structure as a 'substructure' of another even when there is merely a given/canonical injective function. Proof assistants with any level of sophistication are intelligent enough/carefully designed to also use this technique without bothering the human operator to explicitly apply the required inclusion function in every single instance. | |
| Nov 26, 2017 at 7:46 | comment | added | Asaf Karagila♦ | @David: And also just because it is not a part of the language of set theory I have absolute freedom to construct $\omega$, and everything else and then when I have $\Bbb R$ or whatever I can define $\Bbb N$ as a subset of that. Yes, the standard way to prove there is a model of the natural numbers is to use $\omega$. But this is not some reason to insist that it is the only way to do it. This is just feigning ignorance. And this is a valid approach, and many analysis books (especially for non mathematicians) start with positing the existence of the reals and define the naturals etc. from that | |
| Nov 26, 2017 at 7:42 | comment | added | Asaf Karagila♦ | @David: Again, this is not a counterargument in favor of set theory, it is simply one counter to "type theory is better because in set theory you can ask 'meaningfully' questions that are meaningless to a working mathematician". I'm simply pointing out that this is the kettle calling 5he pot black. | |
| Nov 26, 2017 at 4:27 | comment | added | Derek Elkins left SE | @NoahSnyder NuPRL actually does have subtyping relationships though they don't always produce what you'd expect. For example, in NuPRL $\mathbb{Z}$ is a subtype of $\mathbb{Z}/n\mathbb{Z}$ (that's not backwards) and the term $0$ is an inhabitant of both types. It also defines $\mathbb{N}$ as a subset type of $\mathbb{Z}$ (which is primitive) so the term $0$ is also a term of $\mathbb{N}$. However, if you built the rationals out of $\mathbb{Z}$, the rational $0$ would be a quite different term than the integer $0$. | |
| Nov 25, 2017 at 23:43 | comment | added | David Roberts♦ | @Asaf but the 0 of the naturals, the 0 of the rationals, the 0 of the reals and so on are different sets, so what's different when you use the implicit coercion in set theory and in type theory? People identify the set of natural numbers defined in von Neumann style perhaps with the natural numbers in the complex numbers and all intermediate rings without making explicit the functions that do so. | |
| Nov 25, 2017 at 22:02 | comment | added | Asaf Karagila♦ | (1) I never said that this is a defense of set theory, but it is just the common type theory argument why type theory is better than set theory, and I simply point out that it's not really an argument that you can make from a "classical type-theory argument". (2) And I agree about the second comment, yes, but for the love of god, is English complete nonsensical and should be replaced just because I can say "My table barks like a cat" which is a type mismatch question? This is generally throwing the baby with the bathwater and the kitchen sink. | |
| Nov 25, 2017 at 20:24 | comment | added | Noah Snyder | Also when we teach we acknowledge that this is a spot where we're doing something confusing. That is the first few pages about groups will be careful to distinguish between units or multiplication in different groups using notation like $\cdot_G$ and $e_G$, but then we drop that quickly afterwards. So it's somewhere that we're aware that a formal version should be more careful than the informal. Also, it's a fair and often good question in class to ask "Sorry, where is that multiplication taking place?" but a bad and troll-y question to ask "How many elements does that multiplication have." | |
| Nov 25, 2017 at 20:13 | comment | added | Noah Snyder | Though I also think that's very special to exactly the situation of "traditional numbers" and not to anything else in mathematics, and so one could argue that that intuition is problematic. I mean are the 0 in $\mathbb{Z}$ and $\mathbb{Z}/n\mathbb{Z}$ different mathematical objects? Certainly the $0$ in $\mathbb{C}$ and the $0$ in $\mathbb{Z}/n\mathbb{Z}$ are different! | |
| Nov 25, 2017 at 20:07 | comment | added | Noah Snyder | Isn't that just an argument that a "polymorphic" foundation would be an even better approximation of informal mathematics? I don't see how it's a defense of set theory. | |
| Nov 25, 2017 at 20:01 | comment | added | Asaf Karagila♦ | I hate that sort of argument against set theoretic foundation. I find it silly. If you also tell your run of the mill analyst that $0$ of $\Bbb R$ and $0$ of $\Bbb C$ and $0$ of $\Bbb N$ and $0$ of $\Bbb Z$ and $0$ of $\Bbb Q$ are all different mathematical objects, you are probably going to get the same reaction as you would when you ask what is the set $\sin\cap\cos$. | |
| Nov 25, 2017 at 19:34 | comment | added | Qiaochu Yuan | Agreed; I wrote a blog post describing my sense of the informal type system that mathematicians are already using (but usually not making explicit) here: qchu.wordpress.com/2013/05/28/the-type-system-of-mathematics A related thing that's strange about ZFC is that it defines sets to be, essentially, a type of tree, but for the purpose of actually doing mathematics we ignore almost all of the tree structure when we consider sets up to isomorphism. | |
| S Nov 25, 2017 at 18:40 | history | answered | Noah Snyder | CC BY-SA 3.0 | |
| S Nov 25, 2017 at 18:40 | history | made wiki | Post Made Community Wiki by Noah Snyder |