I am impressed! This is some beautiful work! And verify.lisp is amazingly short. Wow. I haven't tested it yet, nor fully digested the documentation, but wow. Nice!
A few questions?
1. "The relative order of independent proof lines does not matter."
I'm not clear on why that is. Or what "independent proof lines" means.
2. My editor can read/write UTF-8 but can only handle certain codesets, and only one at a time! Doh. Apparently bourbaki accepts any UTF-8 character as the name of a symbol, then I need a text editor that can mix and match codesets. What tool are you using?
3. On symtrees: "The tree is well-formed if the number of arguments of op is n and each treei is a well-formed tree whose type is a subtype of the corresponding argument type of op."
Beautiful! That solves the problem of "overloaded" functions very nicely!
Question: does bourbaki check for loops in the super/sub-type declarations? Or is that the user's responsibility?
4. Symbol arguments: are null substitutions allowed? For example, in Metamath a given type could be specified as permitting nulls with an axiom of this sort:
nullXYZ $a xyz $.
5. Doc clarification --
In your definitions "lisp-form*" is used but not defined. I'm assuming that is common knowledge to Lisp programmers, but ??? For example in 4.1.1:
theorem-form := ( th name var-spec lisp-form* )
6. How much for a software license?
First born? Oath of fealty? Or is it GPL?
7. I am wondering, jarpiain, if you have/would consider the Ghilbert approach of separating proofs from theorems. Essentially, a theorem can be considered as an assertion without a proof, like an axiom. Bourbaki has so much in common with Ghilbert I wonder if we could strive for unification at the conceptual level, assuming that the change(s) add to Bourbaki in an elegant and useful way. --ocat
8. Are there any places other than symbol name that would need to be addressed if a user desired to create a 7-bit ASCII version of Bourbaki? (It has been noted that typesetting will be desireable anyway, so the utility of Unicode seems less than its drawbacks for some users…) --ocat