brismu: a relational interpretation of Lojban

[mostawe...@gmail.com]

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

[David A. Wheeler]

> On Jan 2, 2025, at 9:48 PM, mostawe...@gmail.com <mostawe...@gmail.com> wrote:
> 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.

> ...
> A living version of la brismu is published online [0]. Collaboration is invited on GitHub [1]. Thanks for reading! ...

> [0] https://brismu.systems/
> [1] https://github.com/brismu/brismu

Wow. That's amazing.

I think there should be a link from some of our Metamath pages to this work, so that
those interested can learn about it. I'm not sure where or what it should say.
Yet I think the fact this even *exists* is quite remarkable.

Thank you for sharing about this!

--- David A. Wheeler

[Glauco]

Hi,

Is there a page where we can see an example of a proof, similar to the ones shown in the Metamath Proof Explorer for set.mm?

Here’s an example of what I mean:
Identity Theorem

Thanks in advance!

Glauco

[mostawe...@gmail.com]

Yes! I will have to eventually write a Lojban-aware proof explorer, but I've gotten the stock Proof Explorer to generate some familiar-looking pages and dumped them into the webroot. For example, ~id [0] looks just like in the Intuitionistic Proof Explorer.

I have a few pages that have tables of proven statements; the entries in the table should all have working hyperlinks to the proofs. (A script checks them at build time.) For example, there's tables for the categories Loj and Selb [1][2], which show that our logic is justifiable in 1Lab's homotopy type theory. A typical proof *not* homomorphically borrowed from iset.mm might look like ~mintu-sym [3] which unwraps definitions and applies basic lemmas to justify a bit of folklore; in this case, the idea that {mintu}'s arguments are "interchangeable" [4] according to official definitions.

Also, unrelated, but to be clear: I just noticed that the copyright dedications are busted. Please rest assured that I'm working in the public domain, although I may use some aggressive copyleft to protect the build scripts if necessary. Lojban was borne from the desire to use Loglan without the creator's permission, and so Lojban development, just like most of maths and logic, is done without copyright.

Peace,
~ C.

[0] https://brismu.systems/id.html
[1] https://brismu.systems/loj.html
[2] https://brismu.systems/selb.html
[3] https://brismu.systems/mintu-sym.html

[4] https://jbovlaste.lojban.org/dict/mintu

[Glauco]

It's fascinating to see Metamath proofs for a framework that's significantly different from set.mm—even if I have to admit, I don't fully understand it! 😊

For those interested, here’s the Table of Contents:
👉 https://brismu.systems/mmtheorems.html

On a side note, I hadn't realized there was a .systems TLD—learn something new every day!