Baseline Lojban is 3% defined, 12% ontologized

[Corbin Simpson]

coi lo se kansa,

Here -- *after* April 1st -- is my annual status update.

I have continued to sporadically work towards formalizing Lojban. My project now includes *ontology*, the structuring of relations relative to each other. To make this manageable at scale, I have used my poset editor tool [0] to generate several diagrams, included those diagrams into the book when small or illustrative, and also compiled the data in the diagrams into Metamath axioms. For a taste of the result, see [1]. As a result, we are now 15% formalized, with 3% as dictionary-ready definitions and 12% belonging to an ontological class; for a breakdown by selma'o, see [4].

The main highlight since my last update is the inclusion of {pagbu} as the *mereology* relation. I am hoping that we can have a pluralist multiverse of axioms when it comes to mereology and set theory; in the future, we may give an optional bridge which allows mereologists to translate their theorems to sets for free. If any mereologists find this interesting, please read the axioms and definitions at [4] and let me know whether they're strong enough for you.

Instead of mathboxes or multiple-file databases, I've started directly encoding assorted baseline claims about various selbri. I hope that this will eventually be a third source of formal claims. For example, {mintu} has a symmetry from its definition [5] and {dunli} has one from its modal {du'i} definition [6]. This lets me get around the problem that these two example selbri have been impossible to convincingly define; their properties can be prior to {go} logical expansions or {ganai} extensions.

[0] https://github.com/MostAwesomeDude/zaha/
[1] https://mostawesomedude.github.io/brismu/mmtheorems5.html
[2] https://en.wikipedia.org/wiki/Olog

[3] https://mostawesomedude.github.io/brismu/foreword.html

[4] https://mostawesomedude.github.io/brismu/mmtheorems4.html#mm336b
[5] https://mostawesomedude.github.io/brismu/ax-mintu-sym.html
[6] https://mostawesomedude.github.io/brismu/ax-dunli-sym.html

To the LFK:
* Please meet annually.
* I wish to propose some definitions for a future dictionary project. To that end, I would like to discuss up to 75 currently-formalized valsi at a venue of your choice.
* Oh, unless it's Discord. Nothing personal, but I can't participate there.
* We actually need to talk about what a definition *is*. Does it have to start with {go}? Can we do {ge} or {ganai}?
* I have *so many* tiny notes that I'd love to discuss, if you're interested. Turns out second-order logic is *really* powerful, and there are lots of nuances that I'm taking lots of time to ponder. Your judgement could speed things up.
* Also, I'd like some feedback on the project and how it's informing your plans. In particular, I want better metavariables and also to bless my lujvo. I also want to know if you'd like to adopt a standard/recommended format for these sorts of "ontology logs" [2] to store ontological data.

di'ai,
~ C.