[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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+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
[1].


Links:
------
[1]
https://groups.google.com/d/msgid/lojban/16ccd800-23f0-4c9f-9ee7-8c7f4f08223en%40googlegroups.com?utm_medium=email&utm_source=footer

--
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.