Timeline for A question about J.H. Conway's SURREAL NUMBERS
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 29, 2018 at 21:57 | comment | added | Todd Trimble | @MikeShulman That's interesting; thanks. I don't know if it's at all related, but I remember having trouble some years back trying to extend multiplication on numbers to multiplication on games. | |
| Jul 29, 2018 at 4:22 | comment | added | Mike Shulman | @ToddTrimble Just stumbled across this and thought I would add for the record that not all the uses of excluded middle have yet been eliminated. I can show constructively that the higher inductive-inductive surreal numbers from the book are an abelian group under addition, but I have not yet managed to multiply them; Conway's proof that multiplication respects equality (which is necessary for it to even define a function in the higher inductive case) uses excluded middle in a way I haven't yet been able to eliminate. | |
| Jul 28, 2014 at 21:51 | comment | added | Todd Trimble | Well, that would be an unfortunate (and unintended) reading of what I wrote -- but thank you for clarifying. | |
| Jul 28, 2014 at 21:48 | comment | added | Paul Taylor | What I meant was that one might get the idea from your use of the word "unnecessary" that Conway was just being lazy. Both his contribution and Mike's are significant. | |
| Jul 28, 2014 at 21:46 | comment | added | Todd Trimble | Um, well I've certainly "looked at" ONAG, and I could hardly have mistaken any of it for "trivial". | |
| Jul 28, 2014 at 21:21 | comment | added | Paul Taylor | There is nothing trivial about what either John Conway or Mike Shulman did, and I recommend that you look at it. In fact, Mike's formulation is like a two-sided version of my "plump" ordinals. | |
| Jul 28, 2014 at 20:56 | comment | added | Todd Trimble | "eliminating the double negations"... that's interesting. I recall that Conway's arguments were rife with appeals to excluded middle; it's good to know that those were unnecessary. | |
| Jul 28, 2014 at 20:39 | history | answered | Paul Taylor | CC BY-SA 3.0 |