Envelope-to: lojban-list-archive@lojban.org
Delivery-date: Wed, 09 Jun 2021 17:22:29 -0700
Sender: lojban@googlegroups.com
Date: Wed, 9 Jun 2021 17:22:22 -0700 (PDT)
From: Vincent Broman <vpbroman@gmail.com>
To: lojban <lojban@googlegroups.com>
Message-Id: <af60c16b-df28-4263-8f2a-7ab86d35971an@googlegroups.com>
In-Reply-To: <c30a5b0c-d2e3-4469-9414-a1ac93a0c572o@googlegroups.com>
References: <c30a5b0c-d2e3-4469-9414-a1ac93a0c572o@googlegroups.com>
Subject: [lojban] Re: la brismu: Relational Lojban
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_2418_161718695.1623284542900"
Reply-To: lojban@googlegroups.com
Precedence: list
Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com
X-Spam_score: -2.6
X-Spam_score_int: -25
X-Spam_bar: --

------=_Part_2418_161718695.1623284542900
Content-Type: multipart/alternative; 
	boundary="----=_Part_2419_1487686479.1623284542900"

------=_Part_2419_1487686479.1623284542900
Content-Type: text/plain; charset="UTF-8"

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


On Monday, July 13, 2020 at 10:20:16 PM UTC-7 mostawe...@gmail.com wrote:

> 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/af60c16b-df28-4263-8f2a-7ab86d35971an%40googlegroups.com.

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

<div>Your aims look interesting.</div><div>Unfortunately I don't know enoug=
h category theory and formal logic to follow it all.</div><div>If you want =
to model the full language, then one interesting and helpful fact to know i=
s that are a lot of reduction rules for various cmavo, i.e. definitions whi=
ch provide substitutions for patterns, so that you can rewrite text with a =
smaller collection of primitive terms.</div><div>I've tried to collect a bu=
nch of those, but there are others that seem to float in the air until you =
meet the right person knowing the lore.</div><div>The xorlo definitions are=
 good examples.</div><div>&nbsp;I've written tolerably good approximations =
for a bunch of UI written in terms of SEI myself.<br></div><div><br></div><=
div>Vincent Broman</div><div>mihe la bremenli</div><div><br></div><br><div =
class=3D"gmail_quote"><div dir=3D"auto" class=3D"gmail_attr">On Monday, Jul=
y 13, 2020 at 10:20:16 PM UTC-7 mostawe...@gmail.com wrote:<br/></div><bloc=
kquote class=3D"gmail_quote" style=3D"margin: 0 0 0 0.8ex; border-left: 1px=
 solid rgb(204, 204, 204); padding-left: 1ex;"><div dir=3D"ltr"><div>coi</d=
iv><div><br></div><div>I have written some living notes for {la brismu}, a =
relational interpretation of Lojban. This interpretation is built on the ma=
thematics of sets and relations. My two goals are to define a semantics for=
 Lojban which can be readily mapped to computable relational algebra, and a=
lso to provide the community with a more rigorous and mathematical examinat=
ion of Lojban itself.</div><div><br></div><div>My notes are published at <a=
 href=3D"https://github.com/MostAwesomeDude/brismu/" target=3D"_blank" rel=
=3D"nofollow" data-saferedirecturl=3D"https://www.google.com/url?hl=3Den&am=
p;q=3Dhttps://github.com/MostAwesomeDude/brismu/&amp;source=3Dgmail&amp;ust=
=3D1623356817804000&amp;usg=3DAFQjCNEdQ9eiMEVRX4sdz6XKesyPKrkXsQ">https://g=
ithub.com/MostAwesomeDude/brismu/</a> and I have tried to make them somewha=
t readable. They&#39;re not perfect and likely contain errors.</div><div><b=
r></div><div>For those who aren&#39;t on IRC, and haven&#39;t seen any of t=
his before, I&#39;ll explain a bit of background, including the maths. Firs=
t, what is logic? Logic is when we draw conclusions from assumptions. To us=
e a common notation, we might have propositions P, Q, R, ... and we might d=
enote a rule P -&gt; Q which concludes Q given P. This general idea is comm=
on to all formal logics.</div><div><br></div><div>Next, what is a category,=
 and why does it matter to logic? <a href=3D"http://math.ucr.edu/home/baez/=
rosetta.pdf" target=3D"_blank" rel=3D"nofollow" data-saferedirecturl=3D"htt=
ps://www.google.com/url?hl=3Den&amp;q=3Dhttp://math.ucr.edu/home/baez/roset=
ta.pdf&amp;source=3Dgmail&amp;ust=3D1623356817804000&amp;usg=3DAFQjCNHSXeh6=
-a50-t7UEqzuMeUYZRVlNQ">http://math.ucr.edu/home/baez/rosetta.pdf</a> has t=
he long and enlightening answers, but I&#39;ll summarize what&#39;s relevan=
t. A category is a collection of objects, 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, and this composition is associative. M=
oreover, there is an identity arrow for each object; these arrows act like =
units under composition. Note how, for most logics, we immediately have a c=
orresponding category whose objects are propositions and arrows are deducti=
on rules. As we will cover, the arrows are much more important than the obj=
ects.<br></div><div><br></div><div>What does it mean for Lojban to be logic=
al? Traditionally, the logical connectives have been central to the explana=
tion, and the logical connectives are so-called because they obey certain c=
ommutative and distributive properties at a syntactic level; e.g. bridi wit=
h {.e} can be transformed to bridi with {gi&#39;e}. We might thus imagine t=
hat Lojban has some of the structure of a formal logic, and that we can doc=
ument the rules under which one bridi may become another bridi.</div><div><=
br></div><div>Which logical properties does Lojban have? On first blush, CL=
L and many associated materials suggest that Lojban implements a classical =
logic. Propositions are assigned truth values, either true or false, when c=
onsidered 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 s=
ort of classical Boolean behavior. A function takes many values and sends t=
hem to a single result, and that&#39;s what it seems like {du&#39;u} does. =
Or perhaps {jei}. (Each of these sentences hides an IRC fight; I recall thi=
s particular one being particularly silly.)</div><div><br></div><div>But Lo=
jban is quite relational. cmavo like {fa} and {se} witness how selbri are l=
ike relations. Many rules in CLL are bidirectional, which is a hallmark of =
relational algebra. Relational logic is different from classical logic in t=
hat, rather than asking whether something is true, we ask under which condi=
tions something is true. The typical model for relational logic would be th=
e category of sets and relations, rather than functions. Where a function g=
ives 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.</div><div><br></div><div>Why does any of this matter? S=
uppose I said {lo du&#39;u mi mlatu ku bridi lo ka ce&#39;u cinfo}. The log=
ical truth of this statement depends, partially but necessarily, on the rul=
e that (in my ad-hoc metasyntax) {da cinfo de} =3D&gt; {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 trans=
formed into computer code in a lightweight and straightforward way, then we=
 can directly compute with Lojban utterances. This is not an idle high-leve=
l desire; I have diagrams like <a href=3D"http://corbinsimpson.com/danlu.pn=
g" target=3D"_blank" rel=3D"nofollow" data-saferedirecturl=3D"https://www.g=
oogle.com/url?hl=3Den&amp;q=3Dhttp://corbinsimpson.com/danlu.png&amp;source=
=3Dgmail&amp;ust=3D1623356817804000&amp;usg=3DAFQjCNGYu2oaonMnewkwyw0WZhd9o=
gC3ww">http://corbinsimpson.com/danlu.png</a> which show fragments of such =
rules in a compact graphical form.</div><div><br></div><div>Why is my appro=
ach right? It might not be. I&#39;ve had three false starts so far, at leas=
t. Axioms and rules are only as good as what they can prove without contrad=
icting themselves. I think that at some folklore theorems are provable in m=
y 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 br=
oda}, true for each of the various subsets of all the broda1. I&#39;ve used=
 the formal prover Metamath, which is fully syntactic and doesn&#39;t requi=
re any sort of type theory, to prove the very first parts, but Metamath req=
uires hand-hard-coding parsing rules, which is unpleasant. Nonetheless I=
9;ll share what little I&#39;ve got: <a href=3D"https://gist.github.com/Mos=
tAwesomeDude/fadf9e8098fe75360c99070a937dcb67" target=3D"_blank" rel=3D"nof=
ollow" data-saferedirecturl=3D"https://www.google.com/url?hl=3Den&amp;q=3Dh=
ttps://gist.github.com/MostAwesomeDude/fadf9e8098fe75360c99070a937dcb67&amp=
;source=3Dgmail&amp;ust=3D1623356817804000&amp;usg=3DAFQjCNE1z38CpSUBgAvcZN=
lNIcwniagH2w">https://gist.github.com/MostAwesomeDude/fadf9e8098fe75360c990=
70a937dcb67</a></div><div><br></div><div>What are day-to-day dialect change=
s? I think that {pa ka} is almost always the right way to quantify {ka}; {l=
o 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 sumt=
i, but I axiomatically define {bridi} to relate {du&#39;u} to {ka} via terb=
ri. {lo&#39;i} is much more useful than normal, because sets are discussed =
up front rather than being minimized. Scoping rules are quite different, bu=
t 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 word=
s! 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></blockquote></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/af60c16b-df28-4263-8f2a-7ab86d35971an%40googlegroups.com?=
utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.com/d/msgid/l=
ojban/af60c16b-df28-4263-8f2a-7ab86d35971an%40googlegroups.com</a>.<br />

------=_Part_2419_1487686479.1623284542900--

------=_Part_2418_161718695.1623284542900--