la brismu: Relational Lojban

94 views
Skip to first unread message

mostawe...@gmail.com

unread,
Jul 14, 2020, 1:20:16 AM7/14/20
to lojban
coi

I have written some living notes for {la brismu}, a relational interpretation of Lojban. This interpretation is built on the mathematics of sets and relations. My two goals are to define a semantics for Lojban which can be readily mapped to computable relational algebra, and also to provide the community with a more rigorous and mathematical examination of Lojban itself.

My notes are published at https://github.com/MostAwesomeDude/brismu/ and I have tried to make them somewhat readable. They're not perfect and likely contain errors.

For those who aren't on IRC, and haven't seen any of this before, I'll explain a bit of background, including the maths. First, what is logic? Logic is when we draw conclusions from assumptions. To use a common notation, we might have propositions P, Q, R, ... and we might denote a rule P -> Q which concludes Q given P. This general idea is common to all formal logics.

Next, what is a category, and why does it matter to logic? http://math.ucr.edu/home/baez/rosetta.pdf has the long and enlightening answers, but I'll summarize what's relevant. A category is a collection of objects, say X, Y, Z, ... and a collection of arrows, f : X -> Y, g : Y -> Z, ... where each arrow has a source object and a target object. Whenever one arrow's target is another's source, then we may compose them, and this composition is associative. Moreover, there is an identity arrow for each object; these arrows act like units under composition. Note how, for most logics, we immediately have a corresponding category whose objects are propositions and arrows are deduction rules. As we will cover, the arrows are much more important than the objects.

What does it mean for Lojban to be logical? Traditionally, the logical connectives have been central to the explanation, and the logical connectives are so-called because they obey certain commutative and distributive properties at a syntactic level; e.g. bridi with {.e} can be transformed to bridi with {gi'e}. We might thus imagine that Lojban has some of the structure of a formal logic, and that we can document the rules under which one bridi may become another bridi.

Which logical properties does Lojban have? On first blush, CLL and many associated materials suggest that Lojban implements a classical logic. Propositions are assigned truth values, either true or false, when considered in a context. A double-negation rule is given. Data may be freely copied. A traditional model for Lojban might therefore be the category of sets and functions, which happens to have as its internal logic this same sort of classical Boolean behavior. A function takes many values and sends them to a single result, and that's what it seems like {du'u} does. Or perhaps {jei}. (Each of these sentences hides an IRC fight; I recall this particular one being particularly silly.)

But Lojban is quite relational. cmavo like {fa} and {se} witness how selbri are like relations. Many rules in CLL are bidirectional, which is a hallmark of relational algebra. Relational logic is different from classical logic in that, rather than asking whether something is true, we ask under which conditions something is true. The typical model for relational logic would be the category of sets and relations, rather than functions. Where a function gives a single result, a relation gives a set of many possible results. This is akin to plural logic, but ranging explicitly over each possible world; it is also similar to existential import logic, but capturing witnesses for each relationship.

Why does any of this matter? Suppose I said {lo du'u mi mlatu ku bridi lo ka ce'u cinfo}. The logical truth of this statement depends, partially but necessarily, on the rule that (in my ad-hoc metasyntax) {da cinfo de} => {da mlatu de}; that is; for a bridi which claims that something is a lion, we can conclude that it is a cat. (It happens that I am not a cat.) If these rules can be transformed into computer code in a lightweight and straightforward way, then we can directly compute with Lojban utterances. This is not an idle high-level desire; I have diagrams like http://corbinsimpson.com/danlu.png which show fragments of such rules in a compact graphical form.

Why is my approach right? It might not be. I've had three false starts so far, at least. Axioms and rules are only as good as what they can prove without contradicting themselves. I think that at some folklore theorems are provable in my system, though, which gives me confidence that my approach is reasonable. The highest-level short tautology I've proven is {lo'i broda ku broda}, true for each of the various subsets of all the broda1. I've used the formal prover Metamath, which is fully syntactic and doesn't require any sort of type theory, to prove the very first parts, but Metamath requires hand-hard-coding parsing rules, which is unpleasant. Nonetheless I'll share what little I've got: https://gist.github.com/MostAwesomeDude/fadf9e8098fe75360c99070a937dcb67

What are day-to-day dialect changes? I think that {pa ka} is almost always the right way to quantify {ka}; {lo ka} is fine but misleading. Since I started this effort a few years ago, apparently {bridi} has shifted in definition, and terbri are no longer sumti, but I axiomatically define {bridi} to relate {du'u} to {ka} via terbri. {lo'i} is much more useful than normal, because sets are discussed up front rather than being minimized. Scoping rules are quite different, but prenexes still work for disambiguation, and it's only noticable when using {na} negation. And of course this is all within only a few dozen words! There's so much left to do.

Thanks for reading.

mi'e la korvo .i di'ai

Vincent Broman

unread,
Jun 9, 2021, 8:22:24 PM6/9/21
to lojban
Your aims look interesting.
Unfortunately I don't know enough category theory and formal logic to follow it all.
If you want to model the full language, then one interesting and helpful fact to know is that are a lot of reduction rules for various cmavo, i.e. definitions which provide substitutions for patterns, so that you can rewrite text with a smaller collection of primitive terms.
I've tried to collect a bunch of those, but there are others that seem to float in the air until you meet the right person knowing the lore.
The xorlo definitions are good examples.
 I've written tolerably good approximations for a bunch of UI written in terms of SEI myself.

Vincent Broman
mihe la bremenli

Remo Dentato

unread,
Jun 10, 2021, 4:32:10 AM6/10/21
to lojban
I'm going to read your notes right now but I wanted to say that I *always* considered bridi to be relations, not predicates.
To me {ko'a broda ko'e} is not a predicate but the description of a situation in which {ko'a} and {ko'e} are are in the {broda} relationship.

Happy to see I'm not the only one having this view.



--
You received this message because you are subscribed to the Google Groups "lojban" group.
To unsubscribe from this group and stop receiving emails from it, send an email to lojban+un...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/lojban/c30a5b0c-d2e3-4469-9414-a1ac93a0c572o%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages