Envelope-to: lojban-list-archive@lojban.org
Delivery-date: Thu, 01 Apr 2021 08:08:38 -0700
Sender: lojban@googlegroups.com
Date: Thu, 1 Apr 2021 08:08:28 -0700 (PDT)
From: Corbin Simpson <mostawesomedude@gmail.com>
To: lojban <lojban@googlegroups.com>
Message-Id: <ac15b0d5-c27c-4d8c-a459-4f80e9970bddn@googlegroups.com>
Subject: [lojban] Lojban is a logical failure
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_7126_1665397760.1617289708648"
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_7126_1665397760.1617289708648
Content-Type: multipart/alternative; 
	boundary="----=_Part_7127_1683252756.1617289708648"

------=_Part_7127_1683252756.1617289708648
Content-Type: text/plain; charset="UTF-8"

Hey all,

Time for the sort-of-annual reminder that Lojban falls far short of its 
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 [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 collection of rewrite rules which each match sequences of words within 
well-formed sentences and replace them with new sequences of words which 
are still well-formed

We have two of three, for what it's worth. The failure is in this third 
component. 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 to 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 
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 transform 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].)

Contrary to popular belief, types are emergent features of type theory; 
they 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 
ready stream of examples comes from the fact that sets are like partial 
(*truncated*) types; they have elements and equivalence, but no proofs.

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 three 
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 
computationally:

* To prove formal facts about Lojban utterances [6]
* To optimize Lojban utterances, 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. 
It sketches several rules and even gives some examples for the "logical" 
connectives, but it is far from complete. Similarly, la brismu suggests a 
handful 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/show/homotopy%20type%20theory
[3] https://golem.ph.utexas.edu/category/2021/02/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] https://github.com/webyrd/Barliman
[9] http://docs.idris-lang.org/en/latest/

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

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

Hey all,<div><br></div><div>Time for the sort-of-annual reminder that Lojba=
n falls far short of its goals. I'll spell out an explicit recipe for achie=
ving those goals.<br></div><div><br></div><div>Suppose that Lojban were log=
ical; that is, suppose that it has a logic [0]. A logic has three component=
s:</div><div><br></div><div>* A collection of letters which form a collecti=
on of words</div><div>* A grammar which indicates whether a sequence of wor=
ds is a well-formed sentence</div><div>* A collection of rewrite rules whic=
h each match sequences of words within well-formed sentences and replace th=
em with new sequences of words which are still well-formed</div><div><br></=
div><div>We have two of three, for what it's worth. The failure is in this =
third component. If we had all three, then we might call Lojban a *type the=
ory* [1]. In a type theory, we start with a sentence, and then apply rewrit=
e rules to create new sentences. A sequence of rewrite rules, along with a =
starting sentence, is called a *proof* when the rules can be applied in seq=
uence to the starting sentence in order to produce a new final sentence.</d=
iv><div><br></div><div>The defining feature of type theory is types. A type=
 is a collection of proofs, called *elements* of the type, which might be e=
quivalent 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 t=
his for two different proofs which lead to the same element in the same typ=
e, by transforming one proof into another, and so on. (This leads to [2].)<=
/div><div><br></div><div>Contrary to popular belief, types are emergent fea=
tures of type theory; they do not have to be predefined. If we had a collec=
tion of rewrite rules for Lojban, then we could discover types within Lojba=
n's existing corpus. A ready stream of examples comes from the fact that se=
ts are like partial (*truncated*) types; they have elements and equivalence=
, but no proofs.</div><div><br></div><div>In fact, this would give the nati=
ve type theory [3][4][5] of Lojban. A native type theory is one which is ge=
nerated directly from the three components I mentioned earlier, but ignorin=
g any "types" which might be defined internally already. For example, {ctai=
pe} does not actually refer to Lojban's types. The native type theory could=
 be directly put to use computationally:</div><div><br></div><div>* To prov=
e formal facts about Lojban utterances [6]</div><div>* To optimize Lojban u=
tterances, shortening or clarifying them [7]</div><div>* To synthesize Lojb=
an utterances which describe a partially-specified world [8]<br></div><div>=
* To compile Lojban utterances into executable programs [9]</div><div><br><=
/div><div>Iterating on CLL has not produced the rewrite rules that we might=
 desire. It sketches several rules and even gives some examples for the "lo=
gical" connectives, but it is far from complete. Similarly, la brismu sugge=
sts a handful of rewrite rules borrowed from CLL and other logics, but is m=
issing the tense system, BAI, Lojban-in-Lojban grammar, mekso, and much mor=
e.</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/logic<br></div><div>[1] https://ncatlab.org/nlab/s=
how/type+theory</div><div>[2] https://ncatlab.org/nlab/show/homotopy%20type=
%20theory</div><div>[3] https://golem.ph.utexas.edu/category/2021/02/native=
_type_theory.html<br></div><div>[4] https://golem.ph.utexas.edu/category/20=
21/03/native_type_theory_part_2.html<br></div><div>[5] https://golem.ph.ute=
xas.edu/category/2021/03/native_type_theory_part_3_1.html</div><div>[6] htt=
p://us.metamath.org/</div><div>[7] https://egraphs-good.github.io/</div><di=
v>[8] https://github.com/webyrd/Barliman</div><div>[9] http://docs.idris-la=
ng.org/en/latest/<br></div><div><br></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/ac15b0d5-c27c-4d8c-a459-4f80e9970bddn%40googlegroups.com?=
utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.com/d/msgid/l=
ojban/ac15b0d5-c27c-4d8c-a459-4f80e9970bddn%40googlegroups.com</a>.<br />

------=_Part_7127_1683252756.1617289708648--

------=_Part_7126_1665397760.1617289708648--