Timeline for Cauchy reals and Dedekind reals satisfy "the same mathematical theorems"
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 17, 2019 at 12:18 | comment | added | Asaf Karagila♦ | @polfosol: I don't need to know the nutrition values of a tray of roasted potatoes. If anything, I need to know the amount of starch in the potatoes and whether or not I want to preboil, cut, peel, or otherwise tend to the potatoes before I roast them. With sage, rosemary, garlic, and for the advanced class also put a handful of mint and peppercorns when preboiling. | |
| Jul 17, 2019 at 12:15 | comment | added | polfosol | @AsafKaragila just a bit of nitpicking... I think Sage is not an optimal tool for those jobs. FWIW, I recommend using Wolfram alpha | |
| Jul 16, 2019 at 17:26 | comment | added | Asaf Karagila♦ | @Timothy: Yes, some people, at some point, might have to resort to proof assistant. For example, people who rely on UF for their work (I am not trying to disparage anyone here). I don't know if "almost every working mathematician" is right. Either I am not a working mathematician (did I take a holiday?) but I never thought about using Sage for anything other than making a nice herbal tea, or a nice tray of roasted potatoes. | |
| Jul 16, 2019 at 17:21 | comment | added | Timothy Chow | @AsafKaragila : Well, it's just my opinion, but I think that the day is coming when almost every working mathematician is going to be relying on proof assistants, and is going to have to grasp these sorts of distinctions at some level, much as today's mathematicians need to grasp whether (say) learning Sage is worth the time if they want to perform a certain computation. | |
| Jul 16, 2019 at 17:13 | comment | added | Asaf Karagila♦ | @Timothy: Yes, in other words, having a maintainable code base is not of any interest of those not interested in UF (and Coq, or some other proof assistant, since I suppose one can care about UF without caring about formal proof verification and whatnot). | |
| Jul 16, 2019 at 17:11 | comment | added | Timothy Chow | @AsafKaragila: I don't understand your point. For everyone who currently cares about UF, there was a time $t$ in the past when they did not care about it, so by the intermediate value theorem there was a point where they came to care about UF, presumably for some reason, and presumably sometimes those reasons were justified. You're saying that the considerations I mentioned cannot be regarded as justifiable reasons for coming to care about UF? Or that there can never be a justifiable reason for making that transition? | |
| Jul 16, 2019 at 15:58 | comment | added | Asaf Karagila♦ | @Timothy: It sounds to me that the people who "should" appreciate UF, based on your comments here, are exactly those people who care about UF to begin with... | |
| Jul 16, 2019 at 15:47 | comment | added | Kevin Buzzard | @TimothyChow as I'm sure you know, I've been trying to understand dependent type theory and homotopy type theory recently. And as I know you've guessed, the genesis of this question is exactly trying to understand what needs to be done in dependent type theory to work around the fact that the univalence axiom is not present. But once I realised that actually the issue was present in ZFC as well, that's what gave me the idea to ask on MO. | |
| Jul 16, 2019 at 15:42 | comment | added | Timothy Chow | ...except maybe the poor schmuck tasked with maintaining the ZFC code base! Anyway, I think this discussion can give one a better appreciation for the univalence axiom in homotopy type theory, and why such a trivial-sounding axiom can make a big practical difference in a proof assistant. | |
| Jul 16, 2019 at 15:40 | comment | added | Timothy Chow | I'm reminded of a discussion (on the Foundations of Mathematics mailing list, I think) about Univalent Foundations. To oversimplify a bit, the way UF is set up, proofs are "automatically" isomorphism-invariant, so peculiar conversations with the wag will never happen. The cost of doing things this way is that if you really want to prove the ZFC, fully set-theoretic version of the theorem, then you'll still have to do extra work. But arguably, once the isomorphism-invariant version is proved, nobody cares about proving the gory set-theoretic version anyway... | |
| Jul 16, 2019 at 15:19 | comment | added | user21820 | @KevinBuzzard: Let me just say that in my opinion as a logician and computer scientist, I do not think a computer program can find very complicated long proofs of a theorem about reals that unpacks the particular instantiation of the axiomatization of reals, even if it is not encapsulated behind the interface. It is much more likely that a proof utilizing solely the interface would be much shorter than a proof that unpacks at any point, so a good automated prover ought to find the axiomatization-based proof first. But this is an opinion, not a provable mathematical claim. | |
| Jul 16, 2019 at 11:06 | comment | added | Kevin Buzzard | In my mind, one interesting part of the story is that essentially all mathematicians are united in claiming that nobody cares about the proof. Now pity the poor computer proof verification person... | |
| Jul 16, 2019 at 10:56 | comment | added | Kevin Buzzard | This answer indicates a point which had not crystallised in my head until very recently. BSD is in class A, for sure, but there is no proof of this in the literature, and some mathematicians are simply not equipped to supply such a proof (my impression is that many do not even really understand the question), whereas others (perhaps the minority?) are well aware that such a proof exists but can understand the enormity of the task to actually supply such a proof. I'm a number theorist and I understand the statement of BSD. Along the way, I "instinctively" verified it was in A, without noticing. | |
| Jul 16, 2019 at 8:06 | comment | added | David Roberts♦ | I took Kevin to mean not the statement of the theorem falls into A. or B., but the proof mutatis mutandis, does ("The problem is that the proof by my wag friend might use facts about the set of real numbers which are true for one model but not the other. The statement is "sensible" but I have no guarantee that the proof is.") | |
| Jul 16, 2019 at 7:09 | comment | added | Philip Oakley | "most working mathematicians are Platonists who, when they think of the real numbers, think of some ideal set satisfying the properties they know the real numbers satisfy, and never concern themselves with pesky foundational issues regarding the actual model of the reals underlying the discussion." i.e. maths for maths sake, or maths for applied use. e.g. Furey C (2015) "A physics from Algebra". Do the reals represent the real word, or are they an abstract concept... | |
| Jul 16, 2019 at 6:51 | history | answered | Dan Romik | CC BY-SA 4.0 |