Hi friends, I have gone long enough without letting this group know about a project of mine: la brismu, a living book which presents the constructed language Lojban as a logic. About two thirds of la brismu is written in Metamath, providing a computer-verified basis for trusting various high-level statements.
I know you'll want the technical details. The database is humble: "The source has 1660 statements; 293 are $a and 320 are $p." 70 of those are mapped from iset.mm using a homomorphism, but we also have alternative ontologies to set theory, particularly mereology. Lojban naturally behaves like a second-order set theory, with relations first instead of functions, along with lots of sugar. This encodes about 18% of Lojban's baseline vocabulary one way or another, to give an indication of how large a complete database would be. Why Metamath? Verification speed, simplicity of hacking the database, and direct integration of Lojban syntax. On that second point, la brismu (currently) incorporates five Python scripts of no more than 100 lines each, taking advantage of the fact that a purpose-crafted Metamath parser can be written in maybe 20 lines of code. We generate extra Metamath statements corresponding to high-level ontologies of science; I'd rather not hand-write hundreds of statements about animals, colors, etc. when I can generate them from diagrams. A living version of la brismu is published online [0]. Collaboration is invited on GitHub [1]. Thanks for reading! Peace, ~ C. [0] https://brismu.systems/ [1] https://github.com/brismu/brismu -- 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/95962f9b-a2fc-46e7-8f52-bddaea894e7dn%40googlegroups.com.
