Timeline for Bourbaki's definition of the number 1
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 29 at 1:09 | comment | added | Timothy Chow | @AlexNelson I skimmed through your draft and it's very cool! | |
| May 28 at 17:24 | comment | added | Alex Nelson | @TimothyChow I have been procrastinating on writing a commentary about Bourbaki's foundations (more for "my future self" than anyone else), and I forgot about Grimm's paper. But reading his first paper, he glosses over a lot, and doesn't catch a number of errors in Bourbaki's first chapter, which makes me think he just skipped ahead to chapter 2. I don't understand why Grimm didn't use Isabelle to implement Bourbaki's system as an object logic ("Isabelle/Bourbaki"), I might have more to say later. | |
| Apr 18, 2020 at 17:08 | comment | added | Alex Nelson | @TimothyChow This sounds unexciting (after all, what's the difference between 4 symbols among friends?), but when it's repeated 1000 times in the full definition, it starts to add up. Particularly because the Cartesian product is used frequently in the definition of Equipotence, and the unordered pair is used in the Cartesian product. The definitions cascade instances of these simpler definitions, which have several variations in their implementations. I could go on and on, if you like :) | |
| Apr 18, 2020 at 16:57 | comment | added | Alex Nelson | @TimothyChow Oh, I agree with you. because there are syntactic variants for the same concept -- for example -- Mathias took a shortcut in using $\tau_{z}(\forall y)(y\in z\iff y=x)$ for the singleton $\{x\}$ whereas Bourbaki uses $\{x\}:=\{x,x\}$ which would be defined as $\tau_{z}(\forall y)(y\in z\iff (y=x\lor y=x))$ which is semantically identical but syntactically bigger, and expands to a larger number of symbols (albeit redundancies). They're semantically equivalent. There are many small syntactic variations which could be made, which explains the variation in sizes reported. | |
| Apr 18, 2020 at 16:31 | comment | added | Timothy Chow | @AlexNelson : If you have the time, I'd be curious to hear your take on Grimm's papers. Do you agree with me that he gets a slightly different number? If so, I have not read carefully enough to understand why. | |
| Apr 17, 2020 at 22:54 | comment | added | Alex Nelson | And for the sake of completeness, using a primitive ordered pair, the length of "1+1=2" is a modest 19,516,572,617,436,743,593 $\approx 1.9\times 10^{19}$ symbols. | |
| Apr 17, 2020 at 22:21 | history | edited | Alex Nelson | CC BY-SA 4.0 |
added 985 characters in body
|
| Apr 17, 2020 at 19:53 | comment | added | John Baez | Nice! By the way, this particular result 2,409,875,496,393,137,472,149,767,527,877,436,912,979,508,338,752,092,897 was calculated by Robert Solovay, not Adrian Mathias. See my own answer for Solovay's software. | |
| Apr 17, 2020 at 13:35 | history | edited | Alex Nelson | CC BY-SA 4.0 |
added 113 characters in body
|
| Apr 17, 2020 at 13:34 | comment | added | Alex Nelson | Damn it, man, I'm a mathematician, not a spelling bee champion! Err, I mean, thanks, I'll fix that :p | |
| Apr 17, 2020 at 7:54 | comment | added | Asaf Karagila♦ | Do you mean Mathias? | |
| Apr 17, 2020 at 4:22 | comment | added | Alex Nelson | Hmm...actually, if we simplify it further with substitutions, we can cut the representation of 1 down to $6.011873743380472\times 10^{37}$ symbols. | |
| Apr 17, 2020 at 4:06 | review | First posts | |||
| Apr 17, 2020 at 4:29 | |||||
| Apr 17, 2020 at 3:59 | history | answered | Alex Nelson | CC BY-SA 4.0 |