Re: [lojban] Re: Lojban is a logical failure

On Thursday, April 1, 2021 at 11:15:43 AM UTC-7 xxv 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 às 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.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+un...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/lojban/16ccd800-23f0-4c9f-9ee7-8c7f4f08223en%40googlegroups.com
> [1].
>
>
> Links:
> ------
> [1]
> https://groups.google.com/d/msgid/lojban/16ccd800-23f0-4c9f-9ee7-8c7f4f08223en%40googlegroups.com?utm_medium=email&utm_source=footer