Envelope-to: lojban-list-archive@lojban.org
Delivery-date: Thu, 10 Jun 2021 01:32:13 -0700
Sender: lojban@googlegroups.com
Received-SPF: pass (google.com: domain of rdentato@gmail.com designates 2a00:1450:4864:20::136 as permitted sender) client-ip=2a00:1450:4864:20::136;
MIME-Version: 1.0
References: <c30a5b0c-d2e3-4469-9414-a1ac93a0c572o@googlegroups.com>
In-Reply-To: <c30a5b0c-d2e3-4469-9414-a1ac93a0c572o@googlegroups.com>
From: Remo Dentato <rdentato@gmail.com>
Date: Thu, 10 Jun 2021 10:31:57 +0200
Message-ID: <CAAQ0imNWcV8qJL5YSc7k9Q-uPjsr6yf+3cuC8vrR0SO9jmnkHA@mail.gmail.com>
Subject: Re: [lojban] la brismu: Relational Lojban
To: lojban <lojban@googlegroups.com>
Content-Type: multipart/alternative; boundary="000000000000f95a3e05c465390a"
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: --

--000000000000f95a3e05c465390a
Content-Type: text/plain; charset="UTF-8"

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.


On Tue, Jul 14, 2020 at 7:20 AM <mostawesomedude@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/c30a5b0c-d2e3-4469-9414-a1ac93a0c572o%40googlegroups.com
> <https://groups.google.com/d/msgid/lojban/c30a5b0c-d2e3-4469-9414-a1ac93a0c572o%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>

-- 
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/CAAQ0imNWcV8qJL5YSc7k9Q-uPjsr6yf%2B3cuC8vrR0SO9jmnkHA%40mail.gmail.com.

--000000000000f95a3e05c465390a
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div>I&#39;m going to read your notes right now but I want=
ed to say that I *always* considered bridi to be relations, not predicates.=
<br></div><div></div><div> To me {ko&#39;a broda ko&#39;e} is not a predica=
te but the description of a situation in which {ko&#39;a} and {ko&#39;e} ar=
e are in the {broda} relationship.</div><div><br></div><div>Happy to see I&=
#39;m not the only one having this view.<br></div><div><br></div><div><br><=
/div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_a=
ttr">On Tue, Jul 14, 2020 at 7:20 AM &lt;<a href=3D"mailto:mostawesomedude@=
gmail.com">mostawesomedude@gmail.com</a>&gt; wrote:<br></div><blockquote cl=
ass=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid=
 rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div>coi</div><div><br=
></div><div>I have written some living notes for {la brismu}, a relational =
interpretation of Lojban. This interpretation is built on the mathematics o=
f sets and relations. My two goals are to define a semantics for Lojban whi=
ch can be readily mapped to computable relational algebra, and also to prov=
ide the community with a more rigorous and mathematical examination of Lojb=
an itself.</div><div><br></div><div>My notes are published at <a href=3D"ht=
tps://github.com/MostAwesomeDude/brismu/" target=3D"_blank">https://github.=
com/MostAwesomeDude/brismu/</a> and I have tried to make them somewhat read=
able. They&#39;re not perfect and likely contain errors.</div><div><br></di=
v><div>For those who aren&#39;t on IRC, and haven&#39;t seen any of this be=
fore, I&#39;ll explain a bit of background, including the maths. First, wha=
t is logic? Logic is when we draw conclusions from assumptions. To use a co=
mmon notation, we might have propositions P, Q, R, ... and we might denote =
a rule P -&gt; Q which concludes Q given P. This general idea is common to =
all formal logics.</div><div><br></div><div>Next, what is a category, and w=
hy does it matter to logic? <a href=3D"http://math.ucr.edu/home/baez/rosett=
a.pdf" target=3D"_blank">http://math.ucr.edu/home/baez/rosetta.pdf</a> has =
the long and enlightening answers, but I&#39;ll summarize what&#39;s releva=
nt. A category is a collection of objects, say X, Y, Z, ... and a collectio=
n of arrows, f : X -&gt; Y, g : Y -&gt; Z, ... where each arrow has a sourc=
e object and a target object. Whenever one arrow&#39;s target is another=
9;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 deduct=
ion rules. As we will cover, the arrows are much more important than the ob=
jects.<br></div><div><br></div><div>What does it mean for Lojban to be logi=
cal? Traditionally, the logical connectives have been central to the explan=
ation, and the logical connectives are so-called because they obey certain =
commutative and distributive properties at a syntactic level; e.g. bridi wi=
th {.e} can be transformed to bridi with {gi&#39;e}. We might thus imagine =
that Lojban has some of the structure of a formal logic, and that we can do=
cument the rules under which one bridi may become another bridi.</div><div>=
<br></div><div>Which logical properties does Lojban have? On first blush, C=
LL 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 freel=
y 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&#39;s what it seems like {du&#39;u} does.=
 Or perhaps {jei}. (Each of these sentences hides an IRC fight; I recall th=
is particular one being particularly silly.)</div><div><br></div><div>But L=
ojban 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 cond=
itions something is true. The typical model for relational logic would be t=
he category of sets and relations, rather than functions. Where a function =
gives a single result, a relation gives a set of many possible results. Thi=
s is akin to plural logic, but ranging explicitly over each possible world;=
 it is also similar to existential import logic, but capturing witnesses fo=
r each relationship.</div><div><br></div><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 lo=
gical truth of this statement depends, partially but necessarily, on the ru=
le 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 tha=
t it is a cat. (It happens that I am not a cat.) If these rules can be tran=
sformed into computer code in a lightweight and straightforward way, then w=
e can directly compute with Lojban utterances. This is not an idle high-lev=
el desire; I have diagrams like <a href=3D"http://corbinsimpson.com/danlu.p=
ng" target=3D"_blank">http://corbinsimpson.com/danlu.png</a> which show fra=
gments of such rules in a compact graphical form.</div><div><br></div><div>=
Why is my approach right? It might not be. I&#39;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 ar=
e 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=
9;i broda ku broda}, true for each of the various subsets of all the broda1=
. I&#39;ve used the formal prover Metamath, which is fully syntactic and do=
esn&#39;t require any sort of type theory, to prove the very first parts, b=
ut Metamath requires hand-hard-coding parsing rules, which is unpleasant. N=
onetheless I&#39;ll share what little I&#39;ve got: <a href=3D"https://gist=
.github.com/MostAwesomeDude/fadf9e8098fe75360c99070a937dcb67" target=3D"_bl=
ank">https://gist.github.com/MostAwesomeDude/fadf9e8098fe75360c99070a937dcb=
67</a></div><div><br></div><div>What are day-to-day dialect changes? I thin=
k 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, apparentl=
y {bridi} has shifted in definition, and terbri are no longer sumti, but I =
axiomatically define {bridi} to relate {du&#39;u} to {ka} via terbri. {lo&#=
39;i} is much more useful than normal, because sets are discussed up front =
rather than being minimized. Scoping rules are quite different, but prenexe=
s 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 words! 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" target=3D"_b=
lank">lojban+unsubscribe@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&amp;utm_source=3Dfooter" target=3D"_blank">https://group=
s.google.com/d/msgid/lojban/c30a5b0c-d2e3-4469-9414-a1ac93a0c572o%40googleg=
roups.com</a>.<br>
</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/CAAQ0imNWcV8qJL5YSc7k9Q-uPjsr6yf%2B3cuC8vrR0SO9jmnkHA%40m=
ail.gmail.com?utm_medium=3Demail&utm_source=3Dfooter">https://groups.google=
.com/d/msgid/lojban/CAAQ0imNWcV8qJL5YSc7k9Q-uPjsr6yf%2B3cuC8vrR0SO9jmnkHA%4=
0mail.gmail.com</a>.<br />

--000000000000f95a3e05c465390a--