Return-path: Envelope-to: lojban-list-archive@lojban.org Delivery-date: Thu, 01 Apr 2021 10:14:22 -0700 Received: from mail-oi1-f183.google.com ([209.85.167.183]:56137) by stodi.digitalkingdom.org with esmtps (TLS1.3) tls TLS_AES_128_GCM_SHA256 (Exim 4.94) (envelope-from ) id 1lS0tY-00GUpm-CA for lojban-list-archive@lojban.org; Thu, 01 Apr 2021 10:14:22 -0700 Received: by mail-oi1-f183.google.com with SMTP id a6sf2375221oic.22 for ; Thu, 01 Apr 2021 10:14:12 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:reply-to:precedence:mailing-list :list-id:list-post:list-help:list-archive:list-subscribe :list-unsubscribe; bh=0EfEL+a8W1lCKlFa7MpF8ixHW2aFCr5FyuYPVRcNtJw=; b=PH7ue2juGtwRR7xN9buUtHpVlHXBlPpWM+YNuUEzflP5UMiz8937eTFwmLWMIzRXga K3HpcdE/9zLnDAKQTLmnumGyI7kGhU1DnM6NNl+0hfZzaqJJcvQNuv68vCDEaTsnFuWH URwrA0kNehlFnly6a4uDS2ru35pRoH2Go1s2t+iqK6rbUKQ3srokcrFiDY7w3rDmdXUb T4n9t3owlwNsydSw70qIUUjRKYH2sfN1EooCDtTuiS8bFtXX1TJAF3CxnYky8fAmwxwp pdy4xMYZKl7XJ9CE9lOuaUdNPkKaUE3yE2KZFOG5mf1KOg3eGCF34Z9rn/lpHYWb0tWH QCEg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:reply-to:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=0EfEL+a8W1lCKlFa7MpF8ixHW2aFCr5FyuYPVRcNtJw=; b=p2aQvJ42voWG3XSZFkw2FRAj8Z//Elpz5OGNbZ11jLv7lvvQMS0o8isqKXffVGzH6u o6WMRPOmPjwsQgqXVek95OO1KAWJiaEMBfBtPFndgIbMSd0HH31Gt3FsuuzBZhPTe4TC slmweD05FUcYndJ8oWUn7MAEYXzRyqsW79pOuhJWBpc9hzGQYM2ebvkSmmvl+GeEAmfN MVkhhMVz85JvDe9EhVt3pO+c84XTSnQscZkGd4MlZuSUhXcnplRV+4ipBS9POxl00N4I c5dcGL6qufDy84ubHeXpBuT6HkIR7yde+fg2v3/cAKyoxIeX/Smperra0tcDrc6FEbPi Xm9A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:reply-to :precedence:mailing-list:list-id:x-spam-checked-in-group:list-post :list-help:list-archive:list-subscribe:list-unsubscribe; bh=0EfEL+a8W1lCKlFa7MpF8ixHW2aFCr5FyuYPVRcNtJw=; b=mh3xTdH5SeHPjQf6o0XHNfxLfmIyRpAlLOgnB5M7MfXSUMteHBzEdzBUA3Zw6mXpLz 6sVfX6PpLMxW6dHwF+FOU8pVKuV3IHkLgFcebIiCrd5kqqAXgo2AiUBzbJPnsiH7Lhtb GaRER6ohkCZkyHkzkHih/gF9aipz1v+cmJ6uA2/G5c5Bc6UylT3WGd3h66K0sdoWj35j y+n9acUv/zIFpr+rH0lJD0vBMEyKWZoOlQhb+ALFgJWUWTDynHVb72dkqlM+9LlIZC8Y g3F9zI5h1rhIjYrLghJ1gCrC6NVYzEeOAC7lB4lR1WAO7oUQxB5uDp9ztxscHKPmsqoy JZxQ== Sender: lojban@googlegroups.com X-Gm-Message-State: AOAM531gz1mOJebQ5+2LeR3C9U28vdJimzmQy81aEUGO+YHfa+DqNRM3 WLbd8eBq/9cQ5b331V75FJ4= X-Google-Smtp-Source: ABdhPJwcqcQ3xq+MR72USI3FqjJj28OmmReCcAVvUxRQTVRufOdT/1qyS9vjsTGSG09ZnNvOHeNfhA== X-Received: by 2002:aca:d941:: with SMTP id q62mr6913173oig.119.1617297251199; Thu, 01 Apr 2021 10:14:11 -0700 (PDT) X-BeenThere: lojban@googlegroups.com Received: by 2002:a9d:6a47:: with SMTP id h7ls1536762otn.9.gmail; Thu, 01 Apr 2021 10:14:10 -0700 (PDT) X-Received: by 2002:a05:6830:14d2:: with SMTP id t18mr3808864otq.50.1617297250660; Thu, 01 Apr 2021 10:14:10 -0700 (PDT) Date: Thu, 1 Apr 2021 10:14:09 -0700 (PDT) From: Corbin Simpson To: lojban Message-Id: <16ccd800-23f0-4c9f-9ee7-8c7f4f08223en@googlegroups.com> In-Reply-To: <2d3e019b-5f57-4288-98a8-cc7fe3bf41a2n@googlegroups.com> References: <2d3e019b-5f57-4288-98a8-cc7fe3bf41a2n@googlegroups.com> Subject: [lojban] Re: Lojban is a logical failure MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_7135_865273499.1617297249832" X-Original-Sender: MostAwesomeDude@gmail.com Reply-To: lojban@googlegroups.com Precedence: list Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com List-ID: X-Spam-Checked-In-Group: lojban@googlegroups.com X-Google-Group-Id: 1004133512417 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , X-Spam-Score: -2.6 (--) X-Spam_score: -2.6 X-Spam_score_int: -25 X-Spam_bar: -- ------=_Part_7135_865273499.1617297249832 Content-Type: multipart/alternative; boundary="----=_Part_7136_544043645.1617297249832" ------=_Part_7136_544043645.1617297249832 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable You are literally standing in front of the detailed plan, complete with=20 links and notes, built from years of conversation about the nature of=20 Lojban and maths, and you have the audacity to ask "do we have a plan?"=20 {mi'a} have a plan, and it's the one I just explained. {mi'o} have a=20 different plan: you need to learn some maths and stop being so squeamish=20 about working directly with logic itself. Start from the definition of a category. Every category gives a logic; the= =20 objects of the category are equivalence classes of propositions, and the=20 modus-ponens of the logic is witnessed by the category's arrows. This is=20 the foundation of categorical logic. From there, you can learn about type= =20 theory and topos theory. I have spoon-fed you for years on IRC, and in this moment, you are like=20 Henry the 8th in "A Man for All Seasons" [0], a vain king who believes=20 himself to be a master of both English and Latin, who stands in the mud=20 without even thinking about it, and who demonstrates their lack of=20 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,=20 > mostawe...@gmail.com escreveu: > >> 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 >> >> We have two of three, for what it's worth. The failure is in this third= =20 >> component. If we had all three, then we might call Lojban a *type theory= *=20 >> [1]. In a type theory, we start with a sentence, and then apply rewrite= =20 >> rules to create new sentences. A sequence of rewrite rules, along with a= =20 >> starting sentence, is called a *proof* when the rules can be applied in= =20 >> sequence to the starting sentence in order to produce a new final senten= ce. >> >> The defining feature of type theory is types. A type is a collection of= =20 >> proofs, called *elements* of the type, which might be equivalent to each= =20 >> other. To show equivalence for two objects, we would need a pair of proo= fs=20 >> which transform one object into another. We can also do this for two=20 >> different proofs which lead to the same element in the same type, by=20 >> transforming one proof into another, and so on. (This leads to [2].) >> >> Contrary to popular belief, types are emergent features of type theory;= =20 >> they do not have to be predefined. If we had a collection of rewrite rul= es=20 >> for Lojban, then we could discover types within Lojban's existing corpus= . A=20 >> ready stream of examples comes from the fact that sets are like partial= =20 >> (*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= =20 >> native type theory is one which is generated directly from the three=20 >> components I mentioned earlier, but ignoring any "types" which might be= =20 >> defined internally already. For example, {ctaipe} does not actually refe= r=20 >> to Lojban's types. The native type theory could be directly put to use= =20 >> 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= =20 >> world [8] >> * To compile Lojban utterances into executable programs [9] >> >> Iterating on CLL has not produced the rewrite rules that we might desire= .=20 >> It sketches several rules and even gives some examples for the "logical"= =20 >> connectives, but it is far from complete. Similarly, la brismu suggests = a=20 >> handful of rewrite rules borrowed from CLL and other logics, but is miss= ing=20 >> 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=20 >> cared to learn the relevant maths. >> > > Do we have a plan? No deadlines but some plan might be needed. Where to= =20 > start from? Can we solve problems iteratively?=20 > >> >> 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]=20 >> https://golem.ph.utexas.edu/category/2021/03/native_type_theory_part_2.h= tml >> [5]=20 >> 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/ >> >> --=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/16ccd800-23f0-4c9f-9ee7-8c7f4f08223en%40googlegroups.com. ------=_Part_7136_544043645.1617297249832 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
You are literally standing in front of the detailed plan, complete wit= h links and notes, built from years of conversation about the nature of Loj= ban 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 pl= an: you need to learn some maths and stop being so squeamish about working = directly with logic itself.

Start from the definit= ion of a category. Every category gives a logic; the objects of the categor= y are equivalence classes of propositions, and the modus-ponens of the logi= c is witnessed by the category's arrows. This is the foundation of categori= cal logic. From there, you can learn about type theory and topos theory.

I have spoon-fed you for years on IRC, and in this m= oment, you are like Henry the 8th in "A Man for All Seasons" [0], a vain ki= ng who believes himself to be a master of both English and Latin, who stand= s in the mud without even thinking about it, and who demonstrates their lac= k of understanding every time they refuse to engage in self-directed study.=

[0] https://en.wikipedia.org/wiki/A_Man_for_A= ll_Seasons

On Thursday, April 1, 2021 at 10:02:48 AM UTC-7 gleki.is...= @gmail.com wrote:
Em q= uinta-feira, 1 de abril de 2021 =C3=A0s 18:08:28 UTC+3, mostawe...@gmail.com escreveu:
Hey all,

Time for t= he 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 co= llection 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 wi= thin well-formed sentences and replace them with new sequences of words whi= ch 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 sentence= s. 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 def= ining feature of type theory is types. A type is a collection of proofs, ca= lled *elements* of the type, which might be equivalent to each other. To sh= ow equivalence for two objects, we would need a pair of proofs which transf= orm one object into another. We can also do this for two different proofs w= hich lead to the same element in the same type, by transforming one proof i= nto another, and so on. (This leads to [2].)

Contr= ary 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 Lojb= an, then we could discover types within Lojban's existing corpus. A rea= dy stream of examples comes from the fact that sets are like partial (*trun= cated*) types; they have elements and equivalence, but no proofs.

In fact, this would give the native type theory [3][4][5] o= f Lojban. A native type theory is one which is generated directly from the = three components I mentioned earlier, but ignoring any "types" wh= ich might be defined internally already. For example, {ctaipe} does not act= ually refer to Lojban's types. The native type theory could be directly= put to use computationally:

* To prove formal fac= ts about Lojban utterances [6]
* To optimize Lojban utterances, s= hortening or clarifying them [7]
* To synthesize Lojban utterance= s which describe a partially-specified world [8]
* To compile= Lojban utterances into executable programs [9]

It= erating on CLL has not produced the rewrite rules that we might desire. It = sketches several rules and even gives some examples for the "logical&q= uot; connectives, but it is far from complete. Similarly, la brismu suggest= s a handful of rewrite rules borrowed from CLL and other logics, but is mis= sing the tense system, BAI, Lojban-in-Lojban grammar, mekso, and much more.=

Lojban only cosplays as a logical language. We co= uld fix that, if we cared to learn the relevant maths.

Do we have a plan? N= o deadlines but some plan might be needed. Where to start from? Can we solv= e problems iteratively?=C2=A0

Peace,<= br>
~ C.

[0] https://ncatlab.org/nlab/show/logic
[2] https://ncatlab.org/nlab/show/homotopy%20type%20theory
[4] <= a href=3D"https://golem.ph.utexas.edu/category/2021/03/native_type_theory_p= art_2.html" rel=3D"nofollow" target=3D"_blank" data-saferedirecturl=3D"http= s://www.google.com/url?hl=3Den&q=3Dhttps://golem.ph.utexas.edu/category= /2021/03/native_type_theory_part_2.html&source=3Dgmail&ust=3D161738= 3242905000&usg=3DAFQjCNHve3Z1i3VrKyoGp6E0w-A9jhxVHg">https://golem.ph.u= texas.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

--
You received this message because you are subscribed to the Google Groups &= quot;lojban" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to lojban+unsub= scribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/l= ojban/16ccd800-23f0-4c9f-9ee7-8c7f4f08223en%40googlegroups.com.
------=_Part_7136_544043645.1617297249832-- ------=_Part_7135_865273499.1617297249832--