Sorry to dig up an old post. I am interested in your formalization of this first chapter. Is it available somewhere . I could not identify it in your mathbox.
Sylvain Le dimanche 14 juillet 2019 à 15:37:02 UTC, Benoit a écrit : > As for using Bourbaki to help us in set.mm, I would strongly advocate > following the global architecture/sectioning as close as possible, barring > some necessities with computer checking that I have not thought of. I am > not very happy with the current sectioning of set.mm, and a while ago, I > began to tweak a bit the order of the parts and sections (not actually in > set.mm, but in a draft), and the more it went, the closer it was to > Bourbaki's TOC. The first six books of Bourbaki are very unified, and > there are no (or almost none?) forward references (except for the examples, > famously in between stars). The TOC was well thought out by a group of top > mathematicians to emphasize the unity of mathematics and to permit a > systematic treatment of the fundamental structures (which, by the way, is > the title of this set of the first six books). It would be hard to find a > better ordering of the sections. > > The biggest problem with Bourbaki is that it ignores categories (it uses > the less agile "espèces de structures" instead, which was nonetheless, as > FL wrote, historically significant, together with the mere fact of > "thinking structurally"). Category theory was developed in the 1940's > whereas Bourbaki began in the 1930's, and it would have been too much work > to make the change after the global architecture of the treatise had been > set. But set.mm does not use categories either, so this is not a problem. > > By the way: I started a few months ago to try and formalize the first > chapter of the first book of Bourbaki (logic). Indeed, it starts at a very > low level, more than most logic textbooks that I know of, and this fact was > very interesting to me. While trying to adhere closer and closer to the > Bourbaki treatment (the things called "assemblages", etc.), I realized that > this was not very far from doing "metamath in metamath", and that one > should directly aim for this. So I stopped my project, and I would be very > interested in hearing from Mario (or anyone) if the "metamath in metamath" > project is dormant, on its way, soon to be resurrected... > > Benoit > > > > > > On Sunday, July 14, 2019 at 2:48:08 PM UTC+2, fl wrote: >> >> >> > or belonging to the sphere of influence of Germany (Banach) >> >> I have just noticed that Banach wrote in French in Polish reviews. So >> much for the German influence. >> >> >> http://pldml.icm.edu.pl/pldml/search/page.action?qt=SEARCH&q=c_0author_0eq.Banach*c_0language_0eq.all*sc.article*l_0*c_0fulltext_0eq.all >> >> -- >> FL >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/ad1f0526-392d-432e-af83-4e1e6b0c5df7n%40googlegroups.com.
