Timeline for The unification of Mathematics via Topos Theory
Current License: CC BY-SA 2.5
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 25, 2010 at 23:17 | comment | added | Harry Gindi | I'm a fan of category theory in general and think toposes are just nifty (for geometry at least), but this answer made me cringe. | |
| Jun 24, 2010 at 12:54 | comment | added | Boyarsky | Dear Neel: Good luck with the representation theory; it's a beautiful subject. (It boggles my mind how it could have any applications of the sort you suggest, but perhaps that is due to my own ignorance of logic.) | |
| Jun 24, 2010 at 12:49 | comment | added | Neel Krishnaswami | Dear Boyarsky: Unfortunately, I don't know much about any of those three fields! I'm a computer scientist, so I have to admit in embarassment that most non-discrete areas of mathematics are foreign to me. (I do hope to learn some representation theory one day, due to its applications to the model theory of linear logic.) | |
| Jun 23, 2010 at 19:24 | comment | added | The Mathemagician | @Neel I've seem MacLane and Modeijk's book-mature students only need apply,I think if you're not at least a first year graduate student,this is going to be a very tough read indeed. | |
| Jun 23, 2010 at 17:23 | comment | added | Boyarsky | Dear Neel: Unfortunately I don't understand what your example is saying (even the insight which you say hadn't been noticed before). I should have said "interesting theorem in a field of mathematics different from logic", since logicians appear to already be sold on topoi. Since you say the quote in the question is true, in the spirit of "any mathematical field" let's be specific and take 3 big fields: PDE, Riemannian geometry, and representation theory. | |
| Jun 23, 2010 at 16:34 | comment | added | Neel Krishnaswami | Fiore and Simpson's "Lambda-Definability with Sums via Grothendieck Logical Relations" showed how to adapt the idea of a cover algebra or Grothendieck topology to the setting of structural proof theory, which Balat et al subsequently used to give a normalization algorithm for the lambda calculus with disjoint sum types. The insight was that the case-distinction in the disjunction elimination rule could be split apart and the pieces could be taken as a kind of "open cover" of the whole proof. | |
| Jun 23, 2010 at 15:54 | comment | added | Boyarsky | Please give an example of an interesting theorem generated via the procedure of the second paragraph. | |
| Jun 23, 2010 at 13:23 | history | answered | Neel Krishnaswami | CC BY-SA 2.5 |