Envelope-to: lojban-list-archive@lojban.org
Delivery-date: Fri, 02 Apr 2021 05:07:52 -0700
Sender: lojban@googlegroups.com
Date: Fri, 2 Apr 2021 04:48:19 -0700 (PDT)
From: Corbin Simpson <mostawesomedude@gmail.com>
To: lojban <lojban@googlegroups.com>
Message-Id: <32cb2274-7e23-4680-91f7-eb21fda4ae7cn@googlegroups.com>
In-Reply-To: <CAOYwWb1hDUDEUoE0RzFMfVVU4+x2oYaE_ArVVt6in9R2uwbP_w@mail.gmail.com>
References: <ac15b0d5-c27c-4d8c-a459-4f80e9970bddn@googlegroups.com>
 <CAOYwWb1hDUDEUoE0RzFMfVVU4+x2oYaE_ArVVt6in9R2uwbP_w@mail.gmail.com>
Subject: Re: [lojban] Lojban is a logical failure
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_7116_928623691.1617364099764"
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_7116_928623691.1617364099764
Content-Type: multipart/alternative; 
	boundary="----=_Part_7117_1501506274.1617364099764"

------=_Part_7117_1501506274.1617364099764
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

Hi Mike,

While you're correct that the number of rules will not be ~10, like in a=20
typical logic, but more like ~10,000; I do not find this to be a serious=20
obstacle. Metamath [0] has tens of thousands of handwritten derivations,=20
and a machine can check that they are well-formed and valid proofs in only=
=20
a few seconds. I think that the main difficulty is in composing the rules=
=20
in the first place.

The semantics I recommend for Lojban is a fragment of second-order logic=20
(SOL). This embeds cleanly into HOL. Proof search is infeasible, but that=
=20
is typical of programming languages; rather than hypernymy getting in the=
=20
way of proof search, hypernymy offers many choices for folks writing in=20
Lojban to express themselves with nuance.

There exist at least two gismu, {dugri} and {tenfa}, which address the same=
=20
underlying relation. As an immediate and very satisfying consequence,=20
Lojban cannot have a normal form without some arbitrary violence [6] to the=
=20
baseline, in the form of a choice which well-orders the gismu. (We could go=
=20
alphabetically, of course.)

Many words have been spilled on tanru. To be brief, writing (=3D>) for=20
implication, I recommend the principles that:

* Each lujvo =3D> each implied seljvajvo [1] from its terbri
* Each lujvo =3D> the tanru it was made from
* Each tanru =3D> its tertau

So, for example, from {nanbymlatu} "catloaf; cat sitting in a loaf shape"=
=20
we could conclude {mlatu} "cat". Similarly, from {xekri mlatu} "black cat"=
=20
we could conclude {mlatu}. It is okay that adjectives are vague; they still=
=20
constrain what's logically possible, and that is enough.

Note also that, borrowing a bit of category theory, we should expect some=
=20
allegory-like [7] behavior here. Specifically, if we imagine the=20
(hypothetical!) rule that {xekri} =3D> {skari}, then {xekri mlatu} =3D> {sk=
ari=20
mlatu} should be available, via some *two-dimensional rule* which allows us=
=20
to lift rules on selbri to rules on seltau.

I strongly recommend that you read through my notes on formalization and=20
rewrite rules [2]. I will summarize some points based on your specific=20
listing:

* FA: These form a group (each FA rule can be undone, there's a do-nothing=
=20
rule, FA rules compose) and so we only need one rule for=20
introducing/eliminating each of the five FA, plus five more for swapping FA=
=20
and generating a permutation group. Similar reasoning applies to SE.
* CU, KU, terminators in general: We could require that a parse tree is=20
associated to each utterance. Then, the rules for terminators each say that=
=20
a particular sort of branch in the parse tree can, because of the=20
neighboring branches, optionally have a CU or KU or etc. You're quite=20
correct that this is infeasible in Metamath or other embed-your-own-grammar=
=20
systems that don't know about parse trees.
* NA: Should be in a distinct fragment of logic from the rest of the core.=
=20
Lojban is relational, and relational logic is very different from Cartesian=
=20
logic. If we are talking about relations first, rather than quantifiers=20
first, then we should imagine bridi as not being true or false, but being=
=20
true in zero or more contexts, with falsity being the special case where=20
zero contexts work. This is all beside the fact that topos-based HOL=20
doesn't necessarily have LEM or AOC [3]. {su'o} =3D> {naku ro naku} doesn't=
=20
work except in the special case of Boolean situations.
* Modal logic: Should also be in a distinct fragment. Making modal logic=20
not collapse is something of a magic trick. In a tradition of G=C3=B6del, w=
e=20
imagine that modal logic S4 can embed IPC, the intuitionistic propositional=
=20
calculus, but in order to make S4 work, we need something like an embedding=
=20
of S4 into Peano arithmetic. The path for this ends up being IPC =3D> S4 =
=3D>=20
LP =3D> PA, where LP has the same modal behavior as S4, but whenever=20
something is possible, LP carries a *proof* that it is possible. The upshot=
=20
is that Lojban doesn't carry around those proofs, and so a lot of work will=
=20
be required to infer them. See [4] or [5] for explanation.

There are totally non-logical particles that must be handled by parsers,=20
like SA/SI/SU, so once again we have an immediate and satisfying=20
consequence: No, baseline Lojban cannot be totally formalized at the=20
syntactic level in terms of logic, and must be expanded first.

I hope that this is interesting food for thought. Yes, we must immediately=
=20
agree that many parts of the baseline are not formalizable, and provably=20
so. But the bulk of the baseline is gismu, and those are definitely related=
=20
to each other, in addition to coding for relations in their own right.=20
Where those relations can be formalized, we can derive rewrite rules. I=20
haven't implemented them in code, but in la brismu, I give Peano arithmetic=
=20
and basic manipulation of bridi, as well as a set-theoretic definition of=
=20
{du} and {lo}; I think that there are concrete useful things to draw from=
=20
formal efforts.

[0] http://us.metamath.org/mpeuni/mmset.html
[1] https://mw.lojban.org/papri/seljvajvo
[2] https://github.com/MostAwesomeDude/brismu/
[3] https://en.wikipedia.org/wiki/Diaconescu%27s_theorem
[4] https://sartemov.ws.gc.cuny.edu/files/2013/01/Vienna2011-FOLP.pdf
[5] https://www.youtube.com/watch?v=3DRfSYN5wEW5U
[6]=20
https://math.stackexchange.com/questions/1493341/what-exactly-did-hermann-w=
eyl-mean
[7] https://ncatlab.org/nlab/show/allegory


On Thursday, April 1, 2021 at 6:03:32 PM UTC-7 Mike S. wrote:

> Greetings Corbin,
>
> On Thu, Apr 1, 2021 at 11:08 AM Corbin Simpson <mostawe...@gmail.com>=20
> wrote:
>
>> Hey all,
>>
>> Time for the sort-of-annual reminder that Lojban falls far short of its=
=20
>> goals. I'll spell out an explicit recipe for achieving those goals.
>>
>> Suppose that Lojban were logical; that is, suppose that it has a logic=
=20
>> [0]. A logic has three components:
>>
>> * A collection of letters which form a collection of words
>> * A grammar which indicates whether a sequence of words is a well-formed=
=20
>> sentence
>> * A collection of rewrite rules which each match sequences of words=20
>> within well-formed sentences and replace them with new sequences of word=
s=20
>> which are still well-formed
>>
>
> What sort of rewrite rules do you mean?  Are you talking about the=20
> transformation rules of propositional logic, for example, given "P and Q"=
=20
> conclude "P" (i.e. conjunction elimination)? Those sorts of rules are jus=
t=20
> the tip of the iceberg for something like Lojban.
>
> If you are talking about the total collection of possible rewrite rules,=
=20
> including trivial ones, that could be posited for Lojban, then I suspect=
=20
> that the collection size would be staggering -- off the top of my head:=
=20
> within clauses, you can reorder terms and the matrix predicate using FA;=
=20
> depending on context, you can alternate CU and KU and other terminators;=
=20
> again, depending on context, you can sometimes move NA KU (at least thank=
s=20
> to Xorlo rules you can) and sometimes not, and of course, su'o can be=20
> rewritten as naku ro naku; there are bucket loads of particles which can=
=20
> interact with either clauses or more locally that have some modal-logic=
=20
> effect.  Even if you could sort out all the scope issues, sorting out the=
=20
> semantics would not be easy.  Then there is the actual lexicon; in genera=
l=20
> any predicate might have one or more equivalent decompositions (given x1 =
is=20
> a mother conclude x1 is a female parent) and probably has one or more=20
> hypernymic replacements (given x1 is a cat, conclude x1 is a feline, or=
=20
> carnivore, or mammal, or vertebrate, or ...).  Finally there is the=20
> (non-)compositional nature of tanru, the centerpiece of Lojban's=20
> semantics.  Thankfully, in practice most tanru are hyponyms of the tertau=
,=20
> so we can be relatively sure a xekri mlatu is a cat, though we can't be=
=20
> fully sure it's a black one, because "je" is not necessarily to be presum=
ed=20
> (bizarrely to me).
>
> I don't see how one could go about being totally thorough in specifying=
=20
> rewrite rules, and I am not sure it's even possible.  But maybe you have=
=20
> something much more focused in mind -- like a fragment of the full Lojban=
=20
> language that would be easier to manage.  That might work. I don't know.
>
> Best,
> -Mike
>
>

--=20
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 e=
mail to lojban+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/=
lojban/32cb2274-7e23-4680-91f7-eb21fda4ae7cn%40googlegroups.com.

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

<div>Hi Mike,</div><div><br></div><div>While you're correct that the number=
 of rules will not be ~10, like in a typical logic, but more like ~10,000; =
I do not find this to be a serious obstacle. Metamath [0] has tens of thous=
ands of handwritten derivations, and a machine can check that they are well=
-formed and valid proofs in only a few seconds. I think that the main diffi=
culty is in composing the rules in the first place.</div><div><br></div><di=
v>The semantics I recommend for Lojban is a fragment of second-order logic =
(SOL). This embeds cleanly into HOL. Proof search is infeasible, but that i=
s typical of programming languages; rather than hypernymy getting in the wa=
y of proof search, hypernymy offers many choices for folks writing in Lojba=
n to express themselves with nuance.</div><div><br></div><div>There exist a=
t least two gismu, {dugri} and {tenfa}, which address the same underlying r=
elation. As an immediate and very satisfying consequence, Lojban cannot hav=
e a normal form without some arbitrary violence [6] to the baseline, in the=
 form of a choice which well-orders the gismu. (We could go alphabetically,=
 of course.)<br></div><div><br></div><div>Many words have been spilled on t=
anru. To be brief, writing (=3D&gt;) for implication, I recommend the princ=
iples that:</div><div><br></div><div>* Each lujvo =3D&gt; each implied selj=
vajvo [1] from its terbri<br></div><div>* Each lujvo =3D&gt; the tanru it w=
as made from</div><div>* Each tanru =3D&gt; its tertau</div><div><br></div>=
<div>So, for example, from {nanbymlatu} "catloaf; cat sitting in a loaf sha=
pe" we could conclude {mlatu} "cat". Similarly, from {xekri mlatu} "black c=
at" we could conclude {mlatu}. It is okay that adjectives are vague; they s=
till constrain what's logically possible, and that is enough.</div><div><br=
></div><div>Note also that, borrowing a bit of category theory, we should e=
xpect some allegory-like [7] behavior here. Specifically, if we imagine the=
 (hypothetical!) rule that {xekri} =3D&gt; {skari}, then {xekri mlatu} =3D&=
gt; {skari mlatu} should be available, via some *two-dimensional rule* whic=
h allows us to lift rules on selbri to rules on seltau.<br></div><div><br><=
/div><div>I strongly recommend that you read through my notes on formalizat=
ion and rewrite rules [2]. I will summarize some points based on your speci=
fic listing:</div><div><br></div><div>* FA: These form a group (each FA rul=
e can be undone, there's a do-nothing rule, FA rules compose) and so we onl=
y need one rule for introducing/eliminating each of the five FA, plus five =
more for swapping FA and generating a permutation group. Similar reasoning =
applies to SE.<br></div><div>* CU, KU, terminators in general: We could req=
uire that a parse tree is associated to each utterance. Then, the rules for=
 terminators each say that a particular sort of branch in the parse tree ca=
n, because of the neighboring branches, optionally have a CU or KU or etc. =
You're quite correct that this is infeasible in Metamath or other embed-you=
r-own-grammar systems that don't know about parse trees.</div><div>* NA: Sh=
ould be in a distinct fragment of logic from the rest of the core. Lojban i=
s relational, and relational logic is very different from Cartesian logic. =
If we are talking about relations first, rather than quantifiers first, the=
n we should imagine bridi as not being true or false, but being true in zer=
o or more contexts, with falsity being the special case where zero contexts=
 work. This is all beside the fact that topos-based HOL doesn't necessarily=
 have LEM or AOC [3]. {su'o} =3D&gt; {naku ro naku} doesn't work except in =
the special case of Boolean situations.</div><div>* Modal logic: Should als=
o be in a distinct fragment. Making modal logic not collapse is something o=
f a magic trick. In a tradition of G=C3=B6del, we imagine that modal logic =
S4 can embed IPC, the intuitionistic propositional calculus, but in order t=
o make S4 work, we need something like an embedding of S4 into Peano arithm=
etic. The path for this ends up being IPC =3D&gt; S4 =3D&gt; LP =3D&gt; PA,=
 where LP has the same modal behavior as S4, but whenever something is poss=
ible, LP carries a *proof* that it is possible. The upshot is that Lojban d=
oesn't carry around those proofs, and so a lot of work will be required to =
infer them. See [4] or [5] for explanation.</div><div><br></div><div>There =
are totally non-logical particles that must be handled by parsers, like SA/=
SI/SU, so once again we have an immediate and satisfying consequence: No, b=
aseline Lojban cannot be totally formalized at the syntactic level in terms=
 of logic, and must be expanded first.</div><div><br></div><div>I hope that=
 this is interesting food for thought. Yes, we must immediately agree that =
many parts of the baseline are not formalizable, and provably so. But the b=
ulk of the baseline is gismu, and those are definitely related to each othe=
r, in addition to coding for relations in their own right. Where those rela=
tions can be formalized, we can derive rewrite rules. I haven't implemented=
 them in code, but in la brismu, I give Peano arithmetic and basic manipula=
tion of bridi, as well as a set-theoretic definition of {du} and {lo}; I th=
ink that there are concrete useful things to draw from formal efforts.<br><=
/div><div><br></div><div>[0] http://us.metamath.org/mpeuni/mmset.html<br></=
div><div>[1] https://mw.lojban.org/papri/seljvajvo</div><div>[2] https://gi=
thub.com/MostAwesomeDude/brismu/</div><div>[3] https://en.wikipedia.org/wik=
i/Diaconescu%27s_theorem</div><div>[4] https://sartemov.ws.gc.cuny.edu/file=
s/2013/01/Vienna2011-FOLP.pdf</div><div>[5] https://www.youtube.com/watch?v=
=3DRfSYN5wEW5U</div><div>[6] https://math.stackexchange.com/questions/14933=
41/what-exactly-did-hermann-weyl-mean</div><div>[7] https://ncatlab.org/nla=
b/show/allegory<br></div><div><br></div><br><div class=3D"gmail_quote"><div=
 dir=3D"auto" class=3D"gmail_attr">On Thursday, April 1, 2021 at 6:03:32 PM=
 UTC-7 Mike S. wrote:<br/></div><blockquote class=3D"gmail_quote" style=3D"=
margin: 0 0 0 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-lef=
t: 1ex;"><div dir=3D"ltr"><div>Greetings Corbin,</div><div class=3D"gmail_q=
uote"></div></div><div dir=3D"ltr"><div class=3D"gmail_quote"><div dir=3D"l=
tr" class=3D"gmail_attr"><br></div><div dir=3D"ltr" class=3D"gmail_attr">On=
 Thu, Apr 1, 2021 at 11:08 AM Corbin Simpson &lt;<a href data-email-masked =
rel=3D"nofollow">mostawe...@gmail.com</a>&gt; wrote:<br></div><blockquote c=
lass=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px soli=
d rgb(204,204,204);padding-left:1ex">Hey all,<div><br></div><div>Time for t=
he sort-of-annual reminder that Lojban falls far short of its goals. I&#39;=
ll spell out an explicit recipe for achieving those goals.<br></div><div><b=
r></div><div>Suppose that Lojban were logical; that is, suppose that it has=
 a logic [0]. A logic has three components:</div><div><br></div><div>* A co=
llection of letters which form a collection of words</div><div>* A grammar =
which indicates whether a sequence of words is a well-formed sentence</div>=
<div>* A collection of rewrite rules which each match sequences of words wi=
thin well-formed sentences and replace them with new sequences of words whi=
ch are still well-formed</div></blockquote><div><br></div></div></div><div =
dir=3D"ltr"><div class=3D"gmail_quote"><div>What sort of rewrite rules do y=
ou mean?=C2=A0 Are you talking about the transformation rules of propositio=
nal logic, for example, given &quot;P and Q&quot; conclude &quot;P&quot; (i=
.e. conjunction elimination)? Those sorts of rules are just the tip of the =
iceberg for something like Lojban.<br></div><div><br></div><div> If you are=
 talking about the total collection of possible rewrite rules, including tr=
ivial ones, that could be posited for Lojban, then I suspect that the colle=
ction size would be staggering -- off the top of my head: within clauses, y=
ou can reorder terms and the matrix predicate

 using FA; depending on context, you can alternate CU and KU and other term=
inators; again, depending on context, you can sometimes move NA KU (at leas=
t thanks to Xorlo rules you can) and sometimes not, and of course, su&#39;o=
 can be rewritten as naku ro naku; there are bucket loads of particles whic=
h can interact with either clauses or more locally that have some modal-log=
ic effect.=C2=A0 Even if you could sort out all the scope issues, sorting o=
ut the semantics would not be easy.=C2=A0 Then there is the actual lexicon;=
 in general any predicate might have one or more equivalent decompositions =
(given x1 is a mother conclude x1 is a female parent) and probably has one =
or more hypernymic replacements (given x1 is a cat, conclude x1 is a feline=
, or carnivore, or mammal, or vertebrate, or ...).=C2=A0 Finally there is t=
he (non-)compositional nature of tanru, the centerpiece of Lojban&#39;s sem=
antics.=C2=A0 Thankfully, in practice most tanru are hyponyms of the tertau=
, so we can be relatively sure a xekri mlatu is a cat, though we can&#39;t =
be fully sure it&#39;s a black one, because &quot;je&quot; is not necessari=
ly to be presumed (bizarrely to me).<br></div><div><br></div><div>I don&#39=
;t see how one could go about being totally thorough in specifying rewrite =
rules, and I am not sure it&#39;s even possible.=C2=A0 But maybe you have s=
omething much more focused in mind -- like a fragment of the full Lojban la=
nguage that would be easier to manage.=C2=A0 That might work. I don&#39;t k=
now.</div><div><br></div><div>Best,</div><div>-Mike<br></div><br></div></di=
v>
</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/32cb2274-7e23-4680-91f7-eb21fda4ae7cn%40googlegroups.com?=
utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.com/d/msgid/l=
ojban/32cb2274-7e23-4680-91f7-eb21fda4ae7cn%40googlegroups.com</a>.<br />

------=_Part_7117_1501506274.1617364099764--

------=_Part_7116_928623691.1617364099764--