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
A category is a deductive system. 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
By defining multiple categories, la brismu enables multiple theories of logical reasoning. Loj corresponds to ganai, gi reasoning, Core(Loj) corresponds to go, gi reasoning, and Selb corresponds to a sort of reasoning over selbri similar to wikipedia:is-a or wikipedia:has-a theories of ontology.