Bourbaki and Metamath

[Jon P]

In this thread FL you say

> Bourbaki's treatise, one of the best things to do is to implement the proofs in set.mm

I wanted to ask if anyone has opinions or ideas on this? How much of the Bourbaki material do you think is implemented already in set.mm? Would that material be useful to add or is it the case that the same concepts are already covered in some different fashion? Is there anyone who is keen on this approach?

I always admired the Bourbaki group. I also wonder if having the textbooks as a scaffold might make progress relatively quick, I think they do spell out everything in quite rigorous detail. 

[fl]

 

I wanted to ask if anyone has opinions or ideas on this? How much of the Bourbaki material do you think is implemented already in set.mm?

2 / 35 ?

 

> Is there anyone who is keen on this approach?

Everybody. When people make structures, they use Bourbaki's work without knowing it.

 

I always admired the Bourbaki group. I also wonder if having the textbooks as a scaffold might make progress relatively quick,

It won't be quick but there will be a companion to the proofs in metamath and THAT it's important.

-- 

FL

[fl]

I wanted to ask if anyone has opinions or ideas on this?

Actually Bourbaki for structures is like Knuth for algorithms. It's not that Knuth invented them, but since he made a complete, careful, well-written and systematic presentation of them, you can be sure that every time someone is talking about an algorithm, he is quoting Knuth's treatise directly or indirectly and not always by naming Knuth. For Bourbaki, the original works were mainly done by Germans (Dedekind, Grassman, Hausdorff) or belonging to the sphere of influence of Germany (Banach) with the exception of Cayley (groups) who was British and Fréchet (distances) who was French but it was still necessary to complete, harmonize and disseminate them.

--
FL

[fl]

>  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

[Benoit]

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

[fl]

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 really like their use of squares and links to explain that a bound variable simply doesn't exist. It's the best approach to the problem I've ever seen.

And they use Hilbert's tau without explaining what's the f*** with that. I love them.

-- 

FL

[Sylvain Kerjean]

Sorry to dig up an old post, but is your formalization available somewhere ? I couldn't identify it in your mathbox

Sylvain