Sender: lojban@googlegroups.com
Date: Mon, 13 Jul 2020 14:35:20 -0700 (PDT)
From: mostawesomedude@gmail.com
To: lojban <lojban@googlegroups.com>
Message-Id: <c30a5b0c-d2e3-4469-9414-a1ac93a0c572o@googlegroups.com>
Subject: [lojban] la brismu: Relational Lojban
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_1425_171465629.1594676120812"
Reply-To: lojban@googlegroups.com
Precedence: list
Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com
X-Spam_score: -2.5
X-Spam_score_int: -24
X-Spam_bar: --

------=_Part_1425_171465629.1594676120812
Content-Type: multipart/alternative; 
	boundary="----=_Part_1426_1595603184.1594676120813"

------=_Part_1426_1595603184.1594676120813
Content-Type: text/plain; charset="UTF-8"

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

-- 
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+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/lojban/c30a5b0c-d2e3-4469-9414-a1ac93a0c572o%40googlegroups.com.

------=_Part_1426_1595603184.1594676120813
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div>coi</div><div><br></div><div>I have written some livi=
ng notes for {la brismu}, a relational interpretation of Lojban. This inter=
pretation is built on the mathematics of sets and relations. My two goals a=
re to define a semantics for Lojban which can be readily mapped to computab=
le relational algebra, and also to provide the community with a more rigoro=
us and mathematical examination of Lojban itself.</div><div><br></div><div>=
My notes are published at https://github.com/MostAwesomeDude/brismu/ and I =
have tried to make them somewhat readable. They&#39;re not perfect and like=
ly contain errors.</div><div><br></div><div>For those who aren&#39;t on IRC=
, and haven&#39;t seen any of this before, I&#39;ll explain a bit of backgr=
ound, including the maths. First, what is logic? Logic is when we draw conc=
lusions from assumptions. To use a common notation, we might have propositi=
ons P, Q, R, ... and we might denote a rule P -&gt; Q which concludes Q giv=
en P. This general idea is common to all formal logics.</div><div><br></div=
><div>Next, what is a category, and why does it matter to logic? http://mat=
h.ucr.edu/home/baez/rosetta.pdf has the long and enlightening answers, but =
I&#39;ll summarize what&#39;s relevant. A category is a collection of objec=
ts, say X, Y, Z, ... and a collection of arrows, f : X -&gt; Y, g : Y -&gt;=
 Z, ... where each arrow has a source object and a target object. Whenever =
one arrow&#39;s target is another&#39;s source, then we may compose them, a=
nd this composition is associative. Moreover, there is an identity arrow fo=
r each object; these arrows act like units under composition. Note how, for=
 most logics, we immediately have a corresponding category whose objects ar=
e propositions and arrows are deduction rules. As we will cover, the arrows=
 are much more important than the objects.<br></div><div><br></div><div>Wha=
t does it mean for Lojban to be logical? Traditionally, the logical connect=
ives 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 wit=
h {gi&#39;e}. We might thus imagine that Lojban has some of the structure o=
f a formal logic, and that we can document the rules under which one bridi =
may become another bridi.</div><div><br></div><div>Which logical properties=
 does Lojban have? On first blush, CLL and many associated materials sugges=
t that Lojban implements a classical logic. Propositions are assigned truth=
 values, either true or false, when considered in a context. A double-negat=
ion rule is given. Data may be freely copied. A traditional model for Lojba=
n might therefore be the category of sets and functions, which happens to h=
ave as its internal logic this same sort of classical Boolean behavior. A f=
unction takes many values and sends them to a single result, and that&#39;s=
 what it seems like {du&#39;u} does. Or perhaps {jei}. (Each of these sente=
nces hides an IRC fight; I recall this particular one being particularly si=
lly.)</div><div><br></div><div>But Lojban is quite relational. cmavo like {=
fa} and {se} witness how selbri are like relations. Many rules in CLL are b=
idirectional, which is a hallmark of relational algebra. Relational logic i=
s different from classical logic in that, rather than asking whether someth=
ing is true, we ask under which conditions something is true. The typical m=
odel for relational logic would be the category of sets and relations, rath=
er 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 impo=
rt logic, but capturing witnesses for each relationship.</div><div><br></di=
v><div>Why does any of this matter? Suppose I said {lo du&#39;u mi mlatu ku=
 bridi lo ka ce&#39;u cinfo}. The logical truth of this statement depends, =
partially but necessarily, on the rule that (in my ad-hoc metasyntax) {da c=
info de} =3D&gt; {da mlatu de}; that is; for a bridi which claims that some=
thing is a lion, we can conclude that it is a cat. (It happens that I am no=
t a cat.) If these rules can be transformed into computer code in a lightwe=
ight and straightforward way, then we can directly compute with Lojban utte=
rances. 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.</div><div><br></div><div>Why is my approach right? It migh=
t not be. I&#39;ve had three false starts so far, at least. Axioms and rule=
s 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&#39;ve proven is {lo&#39;i broda ku broda}, true for eac=
h of the various subsets of all the broda1. I&#39;ve used the formal prover=
 Metamath, which is fully syntactic and doesn&#39;t require any sort of typ=
e theory, to prove the very first parts, but Metamath requires hand-hard-co=
ding parsing rules, which is unpleasant. Nonetheless I&#39;ll share what li=
ttle I&#39;ve got: https://gist.github.com/MostAwesomeDude/fadf9e8098fe7536=
0c99070a937dcb67</div><div><br></div><div>What are day-to-day dialect chang=
es? 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 sum=
ti, but I axiomatically define {bridi} to relate {du&#39;u} to {ka} via ter=
bri. {lo&#39;i} is much more useful than normal, because sets are discussed=
 up front rather than being minimized. Scoping rules are quite different, b=
ut prenexes still work for disambiguation, and it&#39;s only noticable when=
 using {na} negation. And of course this is all within only a few dozen wor=
ds! There&#39;s so much left to do.<br></div><div><br></div><div>Thanks for=
 reading.</div><div><br></div><div>mi&#39;e la korvo .i di&#39;ai<br></div>=
</div>

<p></p>

-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;lojban&quot; group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:lojban+unsubscribe@googlegroups.com">lojban+unsub=
scribe@googlegroups.com</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/d/msgid/lojban/c30a5b0c-d2e3-4469-9414-a1ac93a0c572o%40googlegroups.com?=
utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.com/d/msgid/l=
ojban/c30a5b0c-d2e3-4469-9414-a1ac93a0c572o%40googlegroups.com</a>.<br />

------=_Part_1426_1595603184.1594676120813--

------=_Part_1425_171465629.1594676120812--