Timeline for Do higher types in HoTT provide mathematical structures beyond ZFC?
Current License: CC BY-SA 4.0
29 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 25 at 13:09 | comment | added | Andrej Bauer | @MonroeEskew: Map and function are synonymous, functions $A \to B$ coincide with functional relations. "All" means $∀$ as in first-order logic, as you would expect. So long as we only observe sets (types of homotopy level 0), we see something like Zermelo's bounded set theory. But the homotopical circle $S^1$ has level $1$, so it's better to think of it as the groupoid with one point and $\mathbb{Z}$-many "abstract" loops on it. We cannot show that $S^1$ has two distinct points, but it isn't equivalent to a singleton either (because of the loops). | |
| Jul 25 at 11:54 | comment | added | Monroe Eskew | @AndrejBauer About your example of the homotopical circle, I am pushed to ask, what do you mean by “all”? What do you mean by “map”, and is it synonymous with “function”? We clearly do different kinds of math, but this example doesn’t seem to jive with “classical” or “ordinary” math from my humble perspective. | |
| Jul 24 at 22:01 | comment | added | Asaf Karagila♦ | Andrej, I don't know about other people. But when you go like "Ugh, I'm gonna get comments about this being a thing, because I choose to present my argument in a specific way" it elicit responses, exactly of the kind you're anticipating. Nobody feels the need to defend ZFC. I think I'm just a bit confused with the exasperated tone, and I imagine other people are too. | |
| Jul 24 at 17:49 | comment | added | Pan Mrož | Thank You for kind answer, you didnt misunderstood the question | |
| Jul 24 at 17:33 | comment | added | Andrej Bauer | Given the discussion in the comments, I rewrote my answer in the hope of expressing myself more clearly. I would also like to point out that I answered the technical qustions asked by the OP. If the OP thinks I answered the wrong questions, or misunderstood the questions, then it's their turn to try to explain what they're asking. | |
| Jul 24 at 17:26 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 1366 characters in body
|
| Jul 24 at 14:50 | comment | added | Andrej Bauer | @pastebee: Both ZFC and HoTT have the natural numbers, directly, without any model-theoretic acrobatics. So I don't see why you claim that ZFC doesn't have the natural numbers. | |
| Jul 24 at 14:48 | comment | added | Andrej Bauer | Why do people feel like they need to defend set theory? | |
| Jul 24 at 14:46 | comment | added | Andrej Bauer | @MonroeEskew: in that example sets are (implicitly) embedded into the category of topological spaces as discrete spaces. I'm not saying it's the "right' way to do things, I am just trying to explain by analogy why in HoTT you can't use sets to define $S^1$. It's like trying to define the usual topological circle by performing constructions on discrete topological spaces. | |
| Jul 24 at 14:09 | comment | added | Monroe Eskew | @AndrejBauer Sorry for the naive question, but aren't you just forgetting to specify the topology in the set-theoretic construction of the circle? You can't ask about homeomorphisms regarding a bare collection of points. | |
| Jul 24 at 11:52 | comment | added | Asaf Karagila♦ | @NaïmFavier: I'm glad for you. I'm proving theorems by writing proofs. I enjoy programming, and I enjoy doing maths the way I do it. I'd say it's a hobby, but I do have a permanent job as a mathematician and programming is just a side hobby. If you don't mind, I'll keep doing it this way. | |
| Jul 24 at 11:35 | comment | added | Naïm Favier | @AsafKaragila I don't know about you, but I'm proving theorems by writing code, and HoTT makes this pleasant and intellectually satisfying. | |
| Jul 24 at 10:54 | comment | added | Asaf Karagila♦ | To pull from the programming analogy, I agree that writing code in Common Lisp is very different from writing code in assembly. Even if the end result of the CL code is the same exact code. But this comes down to your point of view on mathematics. Are we proving the existence of algorithms and programs, or are we writing code? If it is the former, then how does CL and Asm differ? | |
| Jul 24 at 10:18 | comment | added | paste bee | And the existence of the interpretation means that HoTT doesn't prove any more than ZFC (plus inaccessibles) does about sets, so in that sense it's not adding anything. Even if you accept that it has more structures than ZFC does, these structures don't tell us anything new about the things ZFC already had; even if a proof about sets is first discovered in HoTT, it follows immediately that a proof also exists in ZFC with enough inaccessibles. | |
| Jul 24 at 10:06 | comment | added | paste bee | More seriously, I don't think the line between "working in an interpretation of a theory" and just defining things is as solid as you're acting like it is, and "if you define things you're not working in ZFC" seems ridiculous. The core difference here isn't "HoTT has $S^1$ and ZFC doesn't", it's that HoTT has $S^1$ as a primitive object, while ZFC uses a more complicated encoding. The appropriate equivalent of HoTT's "type" in ZFC is just a rather long definition, and by replacing it with "set" you're instead looking at a different statement that's not true in HoTT either. | |
| Jul 24 at 10:00 | comment | added | paste bee | There's a simpler example of a structure that exists in HoTT but not ZFC: the natural numbers, because doing things in a model of PA built in ZFC is not the same thing as doing things in ZFC. At all. | |
| Jul 24 at 9:07 | comment | added | Alec Rhea | @NaïmFavier As someone who learned to code in Haskell and Python in the last year (algos/neural networks for day trading) I was amazed at how useful my experience with set theory was, partucularly with haskell — set builder notation is built into the syntax! | |
| Jul 24 at 8:29 | comment | added | Naïm Favier | The programming analogue of the objection would be that Haskell is redundant because you can compile it to assembly. | |
| Jul 24 at 8:05 | comment | added | Andrej Bauer | Anyhow, I made my reply to the imaginary objection more explicit, as it seems that I am being misuderstood. | |
| Jul 24 at 8:04 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
deleted 144 characters in body
|
| Jul 24 at 8:03 | comment | added | Andrej Bauer | I am most definitely not. | |
| Jul 24 at 7:51 | comment | added | Asaf Karagila♦ | (You're just making an argument in favour of assembly programming here...) | |
| Jul 24 at 7:16 | comment | added | Andrej Bauer | @AsafKaragila: what I am trying to get across (but not very well) is that building a model $M_X$ of foundation $X$ in foundation $Y$ doesn't really count as "doing $X$-things in $Y$". It's "doing $X$-things in $M_X$". Abstraction matters, also in your javascript example: vectors may appear as big numbers outside Javascript, but so long as we work in Javascript, we don't have direct access to those numbers. (And also, they're really voltages in a digital circuit.) | |
| Jul 24 at 7:08 | comment | added | Asaf Karagila♦ | @Andrej: Isn't this just cherrypicking an interpretation to make the argument? This is like saying that since I can encode strings as vectors in Javascript, they are inherently distinct from integers. Even though that residing in your memory, even a vector is just a big number... | |
| Jul 23 at 22:00 | comment | added | Andrej Bauer | @AlecRhea: I am not sure how to explain it succinctly. Perhaps like this. Sets can be seen as a subcategory of topological spaces, namely the discrete spaces (also the indiscrete ones, but that's not important right now). Therefore, if one defined the circle as the set of all points at unit distance from the origin, that will be a discrete space that is not homeomorphic to the usual circle. No construction that passes through set theory can ever produce a non-discrete space in this way. This situation is analogous to what happens in HoTT. | |
| Jul 23 at 21:54 | comment | added | Naïm Favier | The synthetic circle constructed as a HIT is a (proper) groupoid, while the "analytic" circle constructed as a set of points in $\mathbb{R}^2$ is, well, a set, so they are not equivalent. AFAIK real-cohesive HoTT offers a way to link the two constructions together. (Also note the incredible difference in complexity between the two: the circle HIT can be defined in two lines, while the analytic circle requires a working definition of the real numbers...) | |
| Jul 23 at 21:21 | vote | accept | Pan Mrož | ||
| Jul 23 at 21:24 | |||||
| Jul 23 at 21:20 | comment | added | Alec Rhea | But non-Euclidean geometry is more flexible than its Euclidean counterpart, it just depends on what your intuition says a ‘triangle’ should be… ;^). More seriously this is a very interesting post; could you elaborate a bit on how the circle realized in type theory ‘isn’t equivalent’ to the one we can realize through the standard set-theoretical constructions? I find synthetic approaches to geometry appealing; is this maybe equivalent to the synthetic differential geometry approach using topoi formulated in a set theoretical universe? | |
| Jul 23 at 21:04 | history | answered | Andrej Bauer | CC BY-SA 4.0 |