brismu
la brismu is a living book which documents a proposed logic and formal semantics for Lojban. It features a collection of proposed axioms of Lojbanic logic, a collection of wikipedia:Metamath proofs built upon that logic, a schematic ontology which organizes selbri, and logical definitions for several common gismu. As of October 2024, it is the largest and most-formalized approach to logical Lojban, defining over 4% of the baseline and ontologizing another 12%.
Definitions
la brismu supports defining valsi in terms of other valsi via go bi-implications. For example, the following definition of se, inspired by CLL examples 11.1 and 11.2, is formalized as ~df-se:
go ko'e se bu'a ko'a gi ko'a bu'a ko'e
Ontologies
Informal ontologies are given for the following concepts:
- Chemistry
- Colors
- Cultures
- Geometry
- Phylogenetics
In the future, ontology logs will be provided for readability and maintainability.
Categories
The following categories are defined:
- Loj, whose objects are equivalence classes of bridi and arrows are implications
- Core(Loj), the core of Loj, whose objects are equivalence classes of bridi and arrows are bi-implications
- Selb, the bicategory of relations whose objects are classes of sumti, arrows are binary selbri, and transformations are inclusions of subrelations between selbri