Envelope-to: lojban-list-archive@lojban.org
Delivery-date: Thu, 01 Apr 2021 14:02:07 -0700
Sender: lojban@googlegroups.com
Received-SPF: pass (google.com: domain of steve@staticfree.info designates 45.33.80.101 as permitted sender) client-ip=45.33.80.101;
Mime-Version: 1.0
Content-Type: text/plain; charset="UTF-8"; format=flowed
Content-Transfer-Encoding: quoted-printable
Date: Thu, 01 Apr 2021 13:38:40 -0400
From: Steve Pomeroy <steve@staticfree.info>
To: lojban@googlegroups.com
Cc: Corbin Simpson <mostawesomedude@gmail.com>
Subject: Re: [lojban] Re: Lojban is a logical failure
In-Reply-To: <16ccd800-23f0-4c9f-9ee7-8c7f4f08223en@googlegroups.com>
References: <ac15b0d5-c27c-4d8c-a459-4f80e9970bddn@googlegroups.com>
 <2d3e019b-5f57-4288-98a8-cc7fe3bf41a2n@googlegroups.com>
 <16ccd800-23f0-4c9f-9ee7-8c7f4f08223en@googlegroups.com>
Message-ID: <5d8ed35bc26ecb99ee250fe535f68e01@staticfree.info>
Reply-To: lojban@googlegroups.com
Precedence: list
Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com
X-Spam_score: -2.8
X-Spam_score_int: -27
X-Spam_bar: --

I'm just a lurker here, but you came in really hot and are now being=20
mean to people. Perhaps, IDK, be cool and we can work this whole thing=20
out together? Not everyone is a math genius like you.

"People may be rude to you because they are unhappy, someone hurt them=20
recently, you were disrespectful towards them, or because they were=20
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.
>=20
> 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.
>=20
> 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.
>=20
> [0] https://en.wikipedia.org/wiki/A_Man_for_All_Seasons
>=20
> On Thursday, April 1, 2021 at 10:02:48 AM UTC-7 gleki.is...@gmail.com
> wrote:
>=20
>> Em quinta-feira, 1 de abril de 2021 =C3=A0s 18:08:28 UTC+3,
>> mostawe...@gmail.com escreveu:
>>=20
>>> Hey all,
>>>=20
>>> 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.
>>>=20
>>> Suppose that Lojban were logical; that is, suppose that it has a
>>> logic [0]. A logic has three components:
>>>=20
>>> * 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
>>>=20
>>> 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.
>>>=20
>>> 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].)
>>>=20
>>> 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.
>>>=20
>>> 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:
>>>=20
>>> * 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]
>>>=20
>>> * To compile Lojban utterances into executable programs [9]
>>>=20
>>> 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.
>>>=20
>>> Lojban only cosplays as a logical language. We could fix that, if
>>> we cared to learn the relevant maths.
>>=20
>> Do we have a plan? No deadlines but some plan might be needed. Where
>> to start from? Can we solve problems iteratively?
>>=20
>>> Peace,
>>>=20
>>> ~ C.
>>>=20
>>> [0] https://ncatlab.org/nlab/show/logic
>>>=20
>>> [1] https://ncatlab.org/nlab/show/type+theory
>>> [2] https://ncatlab.org/nlab/show/homotopy%20type%20theory
>>> [3]
>>>=20
>> https://golem.ph.utexas.edu/category/2021/02/native_type_theory.html
>>>=20
>>> [4]
>>>=20
>>=20
> https://golem.ph.utexas.edu/category/2021/03/native_type_theory_part_2.ht=
ml
>>>=20
>>> [5]
>>>=20
>>=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 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].
>=20
>=20
> Links:
> ------
> [1]
> https://groups.google.com/d/msgid/lojban/16ccd800-23f0-4c9f-9ee7-8c7f4f08=
223en%40googlegroups.com?utm_medium=3Demail&utm_source=3Dfooter

--=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/5d8ed35bc26ecb99ee250fe535f68e01%40staticfree.info.