Don't worry too much about Bourbaki and Set Theory...Bourbaki didn't really use first order logic, anyways.
At any rate, there was an excellent discussion of the formalism discussed in Bourbaki's Theory of Sets over at the nForum a while back (I don't know how I missed it!).
Someone noted that Bourbaki's set theory is "equivalent" to ZGC (Zarmelo with the Axiom of Global Choice).
Addendum: for more details on Bourbaki's set theory, see the entry on Hilbert's Epsilon Calculus.
Wikipedia claims that Zarmelo set theory is "strong enough to carry out almost all ordinary mathematics not directly connected with set theory or logic" (Wikipedia).
Although, it should be noted, later editions of Bourbaki included the axiom of replacement...making it resemble ZFC more than ZGC (The Bourbaki View, fn 15).
Implications for Automated Theorem Provers
I got my hands ahold of a wonderful book:
- John Harrison, Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009).
Why is it so wonderful? Well, in chapter 6 it discusses Mizar-like declarative proof systems. In fact, the code accompanying the book actually implements a simplified version of it.
It wouldn't be terribly difficult to change the wording to use the Mathematical Vernacular.
Additionally, since the programming language is OCaml, one could take advantage of Camlp4 to extend the grammar to make the syntax prettier.
But I digress.
If one were to implement mathematics formally, one couldn't use ZGC without having problems covering topology (or category theory — large categories are defined how?).
However, if one were to take the conservative extension to ZFC, one would still run into problems (again, large categories?). What one would have to do is use BNG Set Theory.
So for any budding cyber-Bourbaki groups out there: you can't use ZGC, ZFC, but you must use BNG (which is not too bad!).
Although, the more I think about it, the more it doesn't matter as long as the behaviour of sets are "sufficiently nice". The implementation details don't matter for, e.g., the ordered pair...just the fact that (x,y)=(a,b) if and only if x=a and y=b. But now I'm just rambling!
Aside on Axioms and Specifications
One thing I always wondered about: why not use naive specifications instead of constructions (e.g., the ordered pair (x,y) as {{x,∅},{y}} or a million other different ways) or rigid axioms?
The answer is that a specification is axiomatic. One specifies the axiomatic behaviour through specifications, it would be logically equivalent to giving an axiomatic framework.
Addendum
To any budding cyber-Bourbakites out there, you will be relieved to find out that there exists an automated proof checker, the "Zermelo Proof Checker", which is based on the BNG axioms for set theory and some minor type theory.
If, like me, you use older hardware...you will run into problems when using zprover. Namely, eprover will always time out, saying something like "CPU time limit exceeded".
Well, zprover is a script that calls eprover and has a parameter that can be (and should be) changed on line 10:
TIME_LIMIT=5 # in seconds
Change it to 60, or something greater.
