Envelope-to: lojban-list-archive@lojban.org
Delivery-date: Thu, 01 Apr 2021 11:31:07 -0700
Sender: lojban@googlegroups.com
Received-SPF: pass (google.com: domain of robert.c.baruch@gmail.com designates 2607:f8b0:4864:20::d34 as permitted sender) client-ip=2607:f8b0:4864:20::d34;
MIME-Version: 1.0
References: <ac15b0d5-c27c-4d8c-a459-4f80e9970bddn@googlegroups.com>
 <2d3e019b-5f57-4288-98a8-cc7fe3bf41a2n@googlegroups.com> <16ccd800-23f0-4c9f-9ee7-8c7f4f08223en@googlegroups.com>
 <5d8ed35bc26ecb99ee250fe535f68e01@staticfree.info>
In-Reply-To: <5d8ed35bc26ecb99ee250fe535f68e01@staticfree.info>
From: Robert Baruch <robert.c.baruch@gmail.com>
Date: Thu, 1 Apr 2021 11:30:42 -0700
Message-ID: <CAPEoGEJVgmDbWbbN+o+=-mX7kG-BNv2NPhfE3VJwROa4seZymQ@mail.gmail.com>
Subject: Re: [lojban] Re: Lojban is a logical failure
To: lojban@googlegroups.com
Cc: Corbin Simpson <mostawesomedude@gmail.com>
Content-Type: multipart/alternative; boundary="0000000000009e3e7505beed6e0d"
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: --

--0000000000009e3e7505beed6e0d
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

+1 for calling out toxic behavior like this.

On Thu, Apr 1, 2021 at 11:15 AM Steve Pomeroy <steve@staticfree.info> wrote=
:

> I'm just a lurker here, but you came in really hot and are now being
> mean to people. Perhaps, IDK, be cool and we can work this whole thing
> out together? Not everyone is a math genius like you.
>
> "People may be rude to you because they are unhappy, someone hurt them
> recently, you were disrespectful towards them, or because they were
> never taught the correct way to act around people." [0]
>
> [0] https://www.wikihow.com/Be-Cool
>
> On 2021-04-01 13:14, Corbin Simpson wrote:
> > You are literally standing in front of the detailed plan, complete
> > with links and notes, built from years of conversation about the
> > nature of Lojban and maths, and you have the audacity to ask "do we
> > have a plan?" {mi'a} have a plan, and it's the one I just explained.
> > {mi'o} have a different plan: you need to learn some maths and stop
> > being so squeamish about working directly with logic itself.
> >
> > Start from the definition of a category. Every category gives a logic;
> > the objects of the category are equivalence classes of propositions,
> > and the modus-ponens of the logic is witnessed by the category's
> > arrows. This is the foundation of categorical logic. From there, you
> > can learn about type theory and topos theory.
> >
> > I have spoon-fed you for years on IRC, and in this moment, you are
> > like Henry the 8th in "A Man for All Seasons" [0], a vain king who
> > believes himself to be a master of both English and Latin, who stands
> > in the mud without even thinking about it, and who demonstrates their
> > lack of understanding every time they refuse to engage in
> > self-directed study.
> >
> > [0] https://en.wikipedia.org/wiki/A_Man_for_All_Seasons
> >
> > On Thursday, April 1, 2021 at 10:02:48 AM UTC-7 gleki.is...@gmail.com
> > wrote:
> >
> >> Em quinta-feira, 1 de abril de 2021 =C3=A0s 18:08:28 UTC+3,
> >> mostawe...@gmail.com escreveu:
> >>
> >>> 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.
> >>
> >> Do we have a plan? No deadlines but some plan might be needed. Where
> >> to start from? Can we solve problems iteratively?
> >>
> >>> 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.ht=
ml
> >>>
> >>> [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/16ccd800-23f0-4c9f-9ee7-8c7f4f08=
223en%40googlegroups.com
> > [1].
> >
> >
> > Links:
> > ------
> > [1]
> >
> https://groups.google.com/d/msgid/lojban/16ccd800-23f0-4c9f-9ee7-8c7f4f08=
223en%40googlegroups.com?utm_medium=3Demail&utm_source=3Dfooter
>
> --
> 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/5d8ed35bc26ecb99ee250fe535f68e01=
%40staticfree.info
> .
>

--=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/CAPEoGEJVgmDbWbbN%2Bo%2B%3D-mX7kG-BNv2NPhfE3VJwROa4seZymQ%40mail.gma=
il.com.

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

<div dir=3D"ltr">+1 for calling out toxic behavior like this.<br></div><br>=
<div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Thu, Ap=
r 1, 2021 at 11:15 AM Steve Pomeroy &lt;<a href=3D"mailto:steve@staticfree.=
info">steve@staticfree.info</a>&gt; wrote:<br></div><blockquote class=3D"gm=
ail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,=
204,204);padding-left:1ex">I&#39;m just a lurker here, but you came in real=
ly hot and are now being <br>
mean to people. Perhaps, IDK, be cool and we can work this whole thing <br>
out together? Not everyone is a math genius like you.<br>
<br>
&quot;People may be rude to you because they are unhappy, someone hurt them=
 <br>
recently, you were disrespectful towards them, or because they were <br>
never taught the correct way to act around people.&quot; [0]<br>
<br>
[0] <a href=3D"https://www.wikihow.com/Be-Cool" rel=3D"noreferrer" target=
=3D"_blank">https://www.wikihow.com/Be-Cool</a><br>
<br>
On 2021-04-01 13:14, Corbin Simpson wrote:<br>
&gt; You are literally standing in front of the detailed plan, complete<br>
&gt; with links and notes, built from years of conversation about the<br>
&gt; nature of Lojban and maths, and you have the audacity to ask &quot;do =
we<br>
&gt; have a plan?&quot; {mi&#39;a} have a plan, and it&#39;s the one I just=
 explained.<br>
&gt; {mi&#39;o} have a different plan: you need to learn some maths and sto=
p<br>
&gt; being so squeamish about working directly with logic itself.<br>
&gt; <br>
&gt; Start from the definition of a category. Every category gives a logic;=
<br>
&gt; the objects of the category are equivalence classes of propositions,<b=
r>
&gt; and the modus-ponens of the logic is witnessed by the category&#39;s<b=
r>
&gt; arrows. This is the foundation of categorical logic. From there, you<b=
r>
&gt; can learn about type theory and topos theory.<br>
&gt; <br>
&gt; I have spoon-fed you for years on IRC, and in this moment, you are<br>
&gt; like Henry the 8th in &quot;A Man for All Seasons&quot; [0], a vain ki=
ng who<br>
&gt; believes himself to be a master of both English and Latin, who stands<=
br>
&gt; in the mud without even thinking about it, and who demonstrates their<=
br>
&gt; lack of understanding every time they refuse to engage in<br>
&gt; self-directed study.<br>
&gt; <br>
&gt; [0] <a href=3D"https://en.wikipedia.org/wiki/A_Man_for_All_Seasons" re=
l=3D"noreferrer" target=3D"_blank">https://en.wikipedia.org/wiki/A_Man_for_=
All_Seasons</a><br>
&gt; <br>
&gt; On Thursday, April 1, 2021 at 10:02:48 AM UTC-7 <a href=3D"mailto:glek=
i.is...@gmail.com" target=3D"_blank">gleki.is...@gmail.com</a><br>
&gt; wrote:<br>
&gt; <br>
&gt;&gt; Em quinta-feira, 1 de abril de 2021 =C3=A0s 18:08:28 UTC+3,<br>
&gt;&gt; <a href=3D"mailto:mostawe...@gmail.com" target=3D"_blank">mostawe.=
..@gmail.com</a> escreveu:<br>
&gt;&gt; <br>
&gt;&gt;&gt; Hey all,<br>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; Time for the sort-of-annual reminder that Lojban falls far sho=
rt<br>
&gt;&gt;&gt; of its goals. I&#39;ll spell out an explicit recipe for achiev=
ing<br>
&gt;&gt;&gt; those goals.<br>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; Suppose that Lojban were logical; that is, suppose that it has=
 a<br>
&gt;&gt;&gt; logic [0]. A logic has three components:<br>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; * A collection of letters which form a collection of words<br>
&gt;&gt;&gt; * A grammar which indicates whether a sequence of words is a<b=
r>
&gt;&gt;&gt; well-formed sentence<br>
&gt;&gt;&gt; * A collection of rewrite rules which each match sequences of<=
br>
&gt;&gt;&gt; words within well-formed sentences and replace them with new<b=
r>
&gt;&gt;&gt; sequences of words which are still well-formed<br>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; We have two of three, for what it&#39;s worth. The failure is =
in this<br>
&gt;&gt;&gt; third component. If we had all three, then we might call Lojba=
n a<br>
&gt;&gt;&gt; *type theory* [1]. In a type theory, we start with a sentence,=
 and<br>
&gt;&gt;&gt; then apply rewrite rules to create new sentences. A sequence o=
f<br>
&gt;&gt;&gt; rewrite rules, along with a starting sentence, is called a *pr=
oof*<br>
&gt;&gt;&gt; when the rules can be applied in sequence to the starting sent=
ence<br>
&gt;&gt;&gt; in order to produce a new final sentence.<br>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; The defining feature of type theory is types. A type is a<br>
&gt;&gt;&gt; collection of proofs, called *elements* of the type, which mig=
ht<br>
&gt;&gt;&gt; be equivalent to each other. To show equivalence for two objec=
ts,<br>
&gt;&gt;&gt; we would need a pair of proofs which transform one object into=
<br>
&gt;&gt;&gt; another. We can also do this for two different proofs which le=
ad<br>
&gt;&gt;&gt; to the same element in the same type, by transforming one proo=
f<br>
&gt;&gt;&gt; into another, and so on. (This leads to [2].)<br>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; Contrary to popular belief, types are emergent features of typ=
e<br>
&gt;&gt;&gt; theory; they do not have to be predefined. If we had a collect=
ion<br>
&gt;&gt;&gt; of rewrite rules for Lojban, then we could discover types with=
in<br>
&gt;&gt;&gt; Lojban&#39;s existing corpus. A ready stream of examples comes=
 from<br>
&gt;&gt;&gt; the fact that sets are like partial (*truncated*) types; they =
have<br>
&gt;&gt;&gt; elements and equivalence, but no proofs.<br>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; In fact, this would give the native type theory [3][4][5] of<b=
r>
&gt;&gt;&gt; Lojban. A native type theory is one which is generated directl=
y<br>
&gt;&gt;&gt; from the three components I mentioned earlier, but ignoring an=
y<br>
&gt;&gt;&gt; &quot;types&quot; which might be defined internally already. F=
or example,<br>
&gt;&gt;&gt; {ctaipe} does not actually refer to Lojban&#39;s types. The na=
tive<br>
&gt;&gt;&gt; type theory could be directly put to use computationally:<br>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; * To prove formal facts about Lojban utterances [6]<br>
&gt;&gt;&gt; * To optimize Lojban utterances, shortening or clarifying them=
 [7]<br>
&gt;&gt;&gt; * To synthesize Lojban utterances which describe a<br>
&gt;&gt;&gt; partially-specified world [8]<br>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; * To compile Lojban utterances into executable programs [9]<br=
>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; Iterating on CLL has not produced the rewrite rules that we mi=
ght<br>
&gt;&gt;&gt; desire. It sketches several rules and even gives some examples=
 for<br>
&gt;&gt;&gt; the &quot;logical&quot; connectives, but it is far from comple=
te. Similarly,<br>
&gt;&gt;&gt; la brismu suggests a handful of rewrite rules borrowed from CL=
L<br>
&gt;&gt;&gt; and other logics, but is missing the tense system, BAI,<br>
&gt;&gt;&gt; Lojban-in-Lojban grammar, mekso, and much more.<br>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; Lojban only cosplays as a logical language. We could fix that,=
 if<br>
&gt;&gt;&gt; we cared to learn the relevant maths.<br>
&gt;&gt; <br>
&gt;&gt; Do we have a plan? No deadlines but some plan might be needed. Whe=
re<br>
&gt;&gt; to start from? Can we solve problems iteratively?<br>
&gt;&gt; <br>
&gt;&gt;&gt; Peace,<br>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; ~ C.<br>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; [0] <a href=3D"https://ncatlab.org/nlab/show/logic" rel=3D"nor=
eferrer" target=3D"_blank">https://ncatlab.org/nlab/show/logic</a><br>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; [1] <a href=3D"https://ncatlab.org/nlab/show/type+theory" rel=
=3D"noreferrer" target=3D"_blank">https://ncatlab.org/nlab/show/type+theory=
</a><br>
&gt;&gt;&gt; [2] <a href=3D"https://ncatlab.org/nlab/show/homotopy%20type%2=
0theory" rel=3D"noreferrer" target=3D"_blank">https://ncatlab.org/nlab/show=
/homotopy%20type%20theory</a><br>
&gt;&gt;&gt; [3]<br>
&gt;&gt;&gt; <br>
&gt;&gt; <a href=3D"https://golem.ph.utexas.edu/category/2021/02/native_typ=
e_theory.html" rel=3D"noreferrer" target=3D"_blank">https://golem.ph.utexas=
.edu/category/2021/02/native_type_theory.html</a><br>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; [4]<br>
&gt;&gt;&gt; <br>
&gt;&gt; <br>
&gt; <a href=3D"https://golem.ph.utexas.edu/category/2021/03/native_type_th=
eory_part_2.html" rel=3D"noreferrer" target=3D"_blank">https://golem.ph.ute=
xas.edu/category/2021/03/native_type_theory_part_2.html</a><br>
&gt;&gt;&gt; <br>
&gt;&gt;&gt; [5]<br>
&gt;&gt;&gt; <br>
&gt;&gt; <br>
&gt; <a href=3D"https://golem.ph.utexas.edu/category/2021/03/native_type_th=
eory_part_3_1.html" rel=3D"noreferrer" target=3D"_blank">https://golem.ph.u=
texas.edu/category/2021/03/native_type_theory_part_3_1.html</a><br>
&gt;&gt;&gt; [6] <a href=3D"http://us.metamath.org/" rel=3D"noreferrer" tar=
get=3D"_blank">http://us.metamath.org/</a><br>
&gt;&gt;&gt; [7] <a href=3D"https://egraphs-good.github.io/" rel=3D"norefer=
rer" target=3D"_blank">https://egraphs-good.github.io/</a><br>
&gt;&gt;&gt; [8] <a href=3D"https://github.com/webyrd/Barliman" rel=3D"nore=
ferrer" target=3D"_blank">https://github.com/webyrd/Barliman</a><br>
&gt;&gt;&gt; [9] <a href=3D"http://docs.idris-lang.org/en/latest/" rel=3D"n=
oreferrer" target=3D"_blank">http://docs.idris-lang.org/en/latest/</a><br>
&gt; <br>
&gt;=C2=A0 --<br>
&gt; You received this message because you are subscribed to the Google<br>
&gt; Groups &quot;lojban&quot; group.<br>
&gt; To unsubscribe from this group and stop receiving emails from it, send=
<br>
&gt; an email to <a href=3D"mailto:lojban%2Bunsubscribe@googlegroups.com" t=
arget=3D"_blank">lojban+unsubscribe@googlegroups.com</a>.<br>
&gt; To view this discussion on the web visit<br>
&gt; <a href=3D"https://groups.google.com/d/msgid/lojban/16ccd800-23f0-4c9f=
-9ee7-8c7f4f08223en%40googlegroups.com" rel=3D"noreferrer" target=3D"_blank=
">https://groups.google.com/d/msgid/lojban/16ccd800-23f0-4c9f-9ee7-8c7f4f08=
223en%40googlegroups.com</a><br>
&gt; [1].<br>
&gt; <br>
&gt; <br>
&gt; Links:<br>
&gt; ------<br>
&gt; [1]<br>
&gt; <a href=3D"https://groups.google.com/d/msgid/lojban/16ccd800-23f0-4c9f=
-9ee7-8c7f4f08223en%40googlegroups.com?utm_medium=3Demail&amp;utm_source=3D=
footer" rel=3D"noreferrer" target=3D"_blank">https://groups.google.com/d/ms=
gid/lojban/16ccd800-23f0-4c9f-9ee7-8c7f4f08223en%40googlegroups.com?utm_med=
ium=3Demail&amp;utm_source=3Dfooter</a><br>
<br>
-- <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%2Bunsubscribe@googlegroups.com" target=3D"=
_blank">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/5d8ed35bc26ecb99ee250fe535f68e01%40staticfree.info" rel=
=3D"noreferrer" target=3D"_blank">https://groups.google.com/d/msgid/lojban/=
5d8ed35bc26ecb99ee250fe535f68e01%40staticfree.info</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/CAPEoGEJVgmDbWbbN%2Bo%2B%3D-mX7kG-BNv2NPhfE3VJwROa4seZymQ=
%40mail.gmail.com?utm_medium=3Demail&utm_source=3Dfooter">https://groups.go=
ogle.com/d/msgid/lojban/CAPEoGEJVgmDbWbbN%2Bo%2B%3D-mX7kG-BNv2NPhfE3VJwROa4=
seZymQ%40mail.gmail.com</a>.<br />

--0000000000009e3e7505beed6e0d--