Envelope-to: lojban-list-archive@lojban.org
Delivery-date: Thu, 01 Apr 2021 09:24:45 -0700
Received-SPF: pass (google.com: domain of kali9putra@yahoo.com designates 74.6.128.83 as permitted sender) client-ip=74.6.128.83;
Date: Thu, 1 Apr 2021 16:24:35 +0000 (UTC)
From: "'John E Clifford' via lojban" <lojban@googlegroups.com>
To: lojban <lojban@googlegroups.com>
Message-ID: <555219299.1422165.1617294275560@mail.yahoo.com>
In-Reply-To: <ac15b0d5-c27c-4d8c-a459-4f80e9970bddn@googlegroups.com>
References: <ac15b0d5-c27c-4d8c-a459-4f80e9970bddn@googlegroups.com>
Subject: Re: [lojban] Lojban is a logical failure
MIME-Version: 1.0
Content-Type: multipart/alternative; 
	boundary="----=_Part_1422164_1289186508.1617294275558"
Content-Length: 11244
Reply-To: lojban@googlegroups.com
Precedence: list
Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com
X-Spam_score: -3.1
X-Spam_score_int: -30
X-Spam_bar: ---

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

 n lacks the underlying HOIL and derivation rules for it and so can never a=
chieve even its goAL OF MONOPrsing, but eventually that comes to the same.

    On Thursday, April 1, 2021, 10:37:57 AM CDT, Corbin Simpson <mostawesom=
edude@gmail.com> wrote: =20
=20
 Hey all,
Time for the sort-of-annual reminder that Lojban falls far short of its goa=
ls. I'll spell out an explicit recipe for achieving those goals.

Suppose that Lojban were logical; that is, suppose that it has a logic [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 sentence* A collect=
ion of rewrite rules which each match sequences of words within well-formed=
 sentences and replace them with new sequences of words which are still wel=
l-formed
We have two of three, for what it's worth. The failure is in this third com=
ponent. If we had all three, then we might call Lojban a *type theory* [1].=
 In a type theory, we start with a sentence, and then apply rewrite rules t=
o create new sentences. A sequence of rewrite rules, along with a starting =
sentence, is called a *proof* when the rules can be applied in sequence to =
the starting sentence in order to produce a new final sentence.
The defining feature of type theory is types. A type is a collection of pro=
ofs, called *elements* of the type, which might be equivalent to each other=
. To show equivalence for two objects, we would need a pair of proofs which=
 transform one object into another. We can also do this for two different p=
roofs which lead to the same element in the same type, by transforming one =
proof into another, and so on. (This leads to [2].)
Contrary to popular belief, types are emergent features of type theory; the=
y do not have to be predefined. If we had a collection of rewrite rules for=
 Lojban, then we could discover types within Lojban's existing corpus. A re=
ady stream of examples comes from the fact that sets are like partial (*tru=
ncated*) types; they have elements and equivalence, but no proofs.
In fact, this would give the native type theory [3][4][5] of Lojban. A nati=
ve type theory is one which is generated directly from the three components=
 I mentioned earlier, but ignoring any "types" which might be defined inter=
nally already. For example, {ctaipe} does not actually refer to Lojban's ty=
pes. The native type theory could be directly put to use computationally:
* To prove formal facts about Lojban utterances [6]* To optimize Lojban utt=
erances, shortening or clarifying them [7]* To synthesize Lojban utterances=
 which describe a partially-specified world [8]
* To compile Lojban utterances into executable programs [9]
Iterating on CLL has not produced the rewrite rules that we might desire. I=
t sketches several rules and even gives some examples for the "logical" con=
nectives, but it is far from complete. Similarly, la brismu suggests a hand=
ful of rewrite rules borrowed from CLL and other logics, but is missing the=
 tense system, BAI, Lojban-in-Lojban grammar, mekso, and much more.
Lojban only cosplays as a logical language. We could fix that, if we cared =
to learn the relevant maths.

Peace,
~ C.

[0] https://ncatlab.org/nlab/show/logic
[1] https://ncatlab.org/nlab/show/type+theory[2] https://ncatlab.org/nlab/s=
how/homotopy%20type%20theory[3] https://golem.ph.utexas.edu/category/2021/0=
2/native_type_theory.html
[4] https://golem.ph.utexas.edu/category/2021/03/native_type_theory_part_2.=
html
[5] https://golem.ph.utexas.edu/category/2021/03/native_type_theory_part_3_=
1.html[6] http://us.metamath.org/[7] https://egraphs-good.github.io/[8] htt=
ps://github.com/webyrd/Barliman[9] http://docs.idris-lang.org/en/latest/


--=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/ac15b0d5-c27c-4d8c-a459-4f80e9970bddn%40googlegroups.com.
 =20

--=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/555219299.1422165.1617294275560%40mail.yahoo.com.

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

<html><head></head><body><div class=3D"ydpf371694fyahoo-style-wrap" style=
=3D"font-family:Helvetica Neue, Helvetica, Arial, sans-serif;font-size:13px=
;"><div></div>
        <div dir=3D"ltr" data-setdir=3D"false">n lacks the underlying HOIL =
and derivation rules for it and so can never achieve even its goAL OF MONOP=
rsing, but eventually that comes to the same.</div><div dir=3D"ltr" data-se=
tdir=3D"false"><br></div><div><br></div>
       =20
        </div><div id=3D"yahoo_quoted_8016624701" class=3D"yahoo_quoted">
            <div style=3D"font-family:'Helvetica Neue', Helvetica, Arial, s=
ans-serif;font-size:13px;color:#26282a;">
               =20
                <div>
                    On Thursday, April 1, 2021, 10:37:57 AM CDT, Corbin Sim=
pson &lt;mostawesomedude@gmail.com&gt; wrote:
                </div>
                <div><br></div>
                <div><br></div>
                <div><div id=3D"yiv0500317138">Hey all,<div><br></div><div>=
Time for the sort-of-annual reminder that Lojban falls far short of its goa=
ls. I'll spell out an explicit recipe for achieving those goals.<br></div><=
div><br></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 collection of letters which form a collection of words</div><div>* A gr=
ammar which indicates whether a sequence of words is a well-formed sentence=
</div><div>* A collection of rewrite rules which each match sequences of wo=
rds within well-formed sentences and replace them with new sequences of wor=
ds which are still well-formed</div><div><br></div><div>We have two of thre=
e, for what it's worth. The failure is in this third component. If we had a=
ll three, then we might call Lojban a *type theory* [1]. In a type theory, =
we start with a sentence, and then apply rewrite rules to create new senten=
ces. A sequence of rewrite rules, along with a starting sentence, is called=
 a *proof* when the rules can be applied in sequence to the starting senten=
ce in order to produce a new final sentence.</div><div><br></div><div>The d=
efining feature of type theory is types. A type is a collection of proofs, =
called *elements* of the type, which might be equivalent to each other. To =
show equivalence for two objects, we would need a pair of proofs which tran=
sform one object into another. We can also do this for two different proofs=
 which lead to the same element in the same type, by transforming one proof=
 into another, and so on. (This leads to [2].)</div><div><br></div><div>Con=
trary to popular belief, types are emergent features of type theory; they d=
o not have to be predefined. If we had a collection of rewrite rules for Lo=
jban, then we could discover types within Lojban's existing corpus. A ready=
 stream of examples comes from the fact that sets are like partial (*trunca=
ted*) types; they have elements and equivalence, but no proofs.</div><div><=
br></div><div>In fact, this would give the native type theory [3][4][5] of =
Lojban. A native type theory is one which is generated directly from the th=
ree components I mentioned earlier, but ignoring any "types" which might be=
 defined internally already. For example, {ctaipe} does not actually refer =
to Lojban's types. The native type theory could be directly put to use comp=
utationally:</div><div><br></div><div>* To prove formal facts about Lojban =
utterances [6]</div><div>* To optimize Lojban utterances, shortening or cla=
rifying them [7]</div><div>* To synthesize Lojban utterances which describe=
 a partially-specified world [8]<br></div><div>* To compile Lojban utteranc=
es into executable programs [9]</div><div><br></div><div>Iterating on CLL h=
as not produced the rewrite rules that we might desire. It sketches several=
 rules and even gives some examples for the "logical" connectives, but it i=
s far from complete. Similarly, la brismu suggests a handful of rewrite rul=
es borrowed from CLL and other logics, but is missing the tense system, BAI=
, Lojban-in-Lojban grammar, mekso, and much more.</div><div><br></div><div>=
Lojban only cosplays as a logical language. We could fix that, if we cared =
to learn the relevant maths.<br></div><div><br></div><div>Peace,<br></div><=
div>~ C.<br></div><div><br></div><div>[0] https://ncatlab.org/nlab/show/log=
ic<br></div><div>[1] https://ncatlab.org/nlab/show/type+theory</div><div>[2=
] https://ncatlab.org/nlab/show/homotopy%20type%20theory</div><div>[3] http=
s://golem.ph.utexas.edu/category/2021/02/native_type_theory.html<br></div><=
div>[4] https://golem.ph.utexas.edu/category/2021/03/native_type_theory_par=
t_2.html<br></div><div>[5] https://golem.ph.utexas.edu/category/2021/03/nat=
ive_type_theory_part_3_1.html</div><div>[6] http://us.metamath.org/</div><d=
iv>[7] https://egraphs-good.github.io/</div><div>[8] https://github.com/web=
yrd/Barliman</div><div>[9] http://docs.idris-lang.org/en/latest/<br></div><=
div><br></div>

<p></p>

-- <br>
You received this message because you are subscribed to the Google Groups "=
lojban" group.<br>
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a rel=3D"nofollow noopener noreferrer" ymailto=3D"mailto:lojban+un=
subscribe@googlegroups.com" target=3D"_blank" href=3D"mailto:lojban+unsubsc=
ribe@googlegroups.com">lojban+unsubscribe@googlegroups.com</a>.<br>
To view this discussion on the web visit <a rel=3D"nofollow noopener norefe=
rrer" target=3D"_blank" href=3D"https://groups.google.com/d/msgid/lojban/ac=
15b0d5-c27c-4d8c-a459-4f80e9970bddn%40googlegroups.com?utm_medium=3Demail&a=
mp;utm_source=3Dfooter">https://groups.google.com/d/msgid/lojban/ac15b0d5-c=
27c-4d8c-a459-4f80e9970bddn%40googlegroups.com</a>.<br>
</div></div>
            </div>
        </div></body></html>

<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/555219299.1422165.1617294275560%40mail.yahoo.com?utm_medi=
um=3Demail&utm_source=3Dfooter">https://groups.google.com/d/msgid/lojban/55=
5219299.1422165.1617294275560%40mail.yahoo.com</a>.<br />

------=_Part_1422164_1289186508.1617294275558--