Lojban is a logical failure

143 views
Skip to first unread message

Corbin Simpson

unread,
Apr 1, 2021, 11:08:28 AM4/1/21
to lojban
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.

Peace,
~ C.


John E Clifford

unread,
Apr 1, 2021, 12:24:38 PM4/1/21
to lojban
n lacks the underlying HOIL and derivation rules for it and so can never achieve even its goAL OF MONOPrsing, but eventually that comes to the same.


--
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/ac15b0d5-c27c-4d8c-a459-4f80e9970bddn%40googlegroups.com.

gleki.is...@gmail.com

unread,
Apr 1, 2021, 1:02:48 PM4/1/21
to lojban
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? 

Corbin Simpson

unread,
Apr 1, 2021, 1:07:22 PM4/1/21
to lojban
Sure. So, instead of waiting for rewrite rules to be issued like manna from heaven, we could explicitly write out rules which implement the behaviors that we typically imply in casual usage. IOW where are all the fluent speakers; they should already know these rules by heart and could just write them down for us~

CLL gives suggested equivalences for {se} (CLL 5.11), {ka} (CLL 11.4), distributive laws (CLL 14.8), forethought and afterthought connectors (CLL 14.5), etc. See la brismu [0] for a detailed exploration. lojban.io [1] uses these rules to partially canonicalize bridi.

Corbin Simpson

unread,
Apr 1, 2021, 1:14:09 PM4/1/21
to lojban
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.

Steve Pomeroy

unread,
Apr 1, 2021, 2:15:43 PM4/1/21
to loj...@googlegroups.com, Corbin Simpson
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
> --
> 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

Robert Baruch

unread,
Apr 1, 2021, 2:30:57 PM4/1/21
to loj...@googlegroups.com, Corbin Simpson
+1 for calling out toxic behavior like this.

To view this discussion on the web visit https://groups.google.com/d/msgid/lojban/5d8ed35bc26ecb99ee250fe535f68e01%40staticfree.info.

Corbin Simpson

unread,
Apr 1, 2021, 4:03:55 PM4/1/21
to lojban
I'm not a math genius. I'm just some person who was told that Lojban is a logical language and decided to take "logical" seriously as an adjective.

For what it's worth, it sounds like you understand what's going on in terms of social dynamics. To paraphrase your quote, I am rude to la gleki because la gleki has disrespected me for years *and* because la gleki has refused to study and work on understanding formal maths. I am happy to talk to any of the 730+ members who have *not* spent the past few years being backhanded and dismissive on IRC.

This isn't my first post to the list, either. I strongly recommend reading the posts from the past year, especially the ones where I went entirely unanswered [0][1][2]. You also should know that I am following the tradition of Clifford in directly critiquing the goals and status of Lojban [3].

John E Clifford

unread,
Apr 1, 2021, 8:21:29 PM4/1/21
to loj...@googlegroups.com
Well, I don’t understand category theory or HOIL, but I do understand that trying to make a natural language into a formal one will lead to an incomplete and unparsible syste, as converting English into Loglan/Lojban has done.  Start with the parsible system and build the natural on it and you get not only parsibility but also a guarantee that the parse is correct (something the Ls never had nor even though to have).  It is long slogging work, if Loglan/Lojban is worthwhile , then ding it this way is worthwile.  We’ve wasted 66 years already, so don’t waste any more.  (The sad thing is that, when the work is done, Loglan/Lojban will be sooo close, but never able to bridge the gap.)

Mike S.

unread,
Apr 1, 2021, 9:03:32 PM4/1/21
to loj...@googlegroups.com
Greetings Corbin,

On Thu, Apr 1, 2021 at 11:08 AM Corbin Simpson <mostawe...@gmail.com> wrote:
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

What sort of rewrite rules do you mean?  Are you talking about the transformation rules of propositional logic, for example, given "P and Q" conclude "P" (i.e. conjunction elimination)? Those sorts of rules are just the tip of the iceberg for something like Lojban.

If you are talking about the total collection of possible rewrite rules, including trivial ones, that could be posited for Lojban, then I suspect that the collection size would be staggering -- off the top of my head: within clauses, you can reorder terms and the matrix predicate using FA; depending on context, you can alternate CU and KU and other terminators; again, depending on context, you can sometimes move NA KU (at least thanks to Xorlo rules you can) and sometimes not, and of course, su'o can be rewritten as naku ro naku; there are bucket loads of particles which can interact with either clauses or more locally that have some modal-logic effect.  Even if you could sort out all the scope issues, sorting out the semantics would not be easy.  Then there is the actual lexicon; in general any predicate might have one or more equivalent decompositions (given x1 is a mother conclude x1 is a female parent) and probably has one or more hypernymic replacements (given x1 is a cat, conclude x1 is a feline, or carnivore, or mammal, or vertebrate, or ...).  Finally there is the (non-)compositional nature of tanru, the centerpiece of Lojban's semantics.  Thankfully, in practice most tanru are hyponyms of the tertau, so we can be relatively sure a xekri mlatu is a cat, though we can't be fully sure it's a black one, because "je" is not necessarily to be presumed (bizarrely to me).

I don't see how one could go about being totally thorough in specifying rewrite rules, and I am not sure it's even possible.  But maybe you have something much more focused in mind -- like a fragment of the full Lojban language that would be easier to manage.  That might work. I don't know.

Best,
-Mike

Corbin Simpson

unread,
Apr 2, 2021, 7:48:19 AM4/2/21
to lojban
Hi Mike,

While you're correct that the number of rules will not be ~10, like in a typical logic, but more like ~10,000; I do not find this to be a serious obstacle. Metamath [0] has tens of thousands of handwritten derivations, and a machine can check that they are well-formed and valid proofs in only a few seconds. I think that the main difficulty is in composing the rules in the first place.

The semantics I recommend for Lojban is a fragment of second-order logic (SOL). This embeds cleanly into HOL. Proof search is infeasible, but that is typical of programming languages; rather than hypernymy getting in the way of proof search, hypernymy offers many choices for folks writing in Lojban to express themselves with nuance.

There exist at least two gismu, {dugri} and {tenfa}, which address the same underlying relation. As an immediate and very satisfying consequence, Lojban cannot have a normal form without some arbitrary violence [6] to the baseline, in the form of a choice which well-orders the gismu. (We could go alphabetically, of course.)

Many words have been spilled on tanru. To be brief, writing (=>) for implication, I recommend the principles that:

* Each lujvo => each implied seljvajvo [1] from its terbri
* Each lujvo => the tanru it was made from
* Each tanru => its tertau

So, for example, from {nanbymlatu} "catloaf; cat sitting in a loaf shape" we could conclude {mlatu} "cat". Similarly, from {xekri mlatu} "black cat" we could conclude {mlatu}. It is okay that adjectives are vague; they still constrain what's logically possible, and that is enough.

Note also that, borrowing a bit of category theory, we should expect some allegory-like [7] behavior here. Specifically, if we imagine the (hypothetical!) rule that {xekri} => {skari}, then {xekri mlatu} => {skari mlatu} should be available, via some *two-dimensional rule* which allows us to lift rules on selbri to rules on seltau.

I strongly recommend that you read through my notes on formalization and rewrite rules [2]. I will summarize some points based on your specific listing:

* FA: These form a group (each FA rule can be undone, there's a do-nothing rule, FA rules compose) and so we only need one rule for introducing/eliminating each of the five FA, plus five more for swapping FA and generating a permutation group. Similar reasoning applies to SE.
* CU, KU, terminators in general: We could require that a parse tree is associated to each utterance. Then, the rules for terminators each say that a particular sort of branch in the parse tree can, because of the neighboring branches, optionally have a CU or KU or etc. You're quite correct that this is infeasible in Metamath or other embed-your-own-grammar systems that don't know about parse trees.
* NA: Should be in a distinct fragment of logic from the rest of the core. Lojban is relational, and relational logic is very different from Cartesian logic. If we are talking about relations first, rather than quantifiers first, then we should imagine bridi as not being true or false, but being true in zero or more contexts, with falsity being the special case where zero contexts work. This is all beside the fact that topos-based HOL doesn't necessarily have LEM or AOC [3]. {su'o} => {naku ro naku} doesn't work except in the special case of Boolean situations.
* Modal logic: Should also be in a distinct fragment. Making modal logic not collapse is something of a magic trick. In a tradition of Gödel, we imagine that modal logic S4 can embed IPC, the intuitionistic propositional calculus, but in order to make S4 work, we need something like an embedding of S4 into Peano arithmetic. The path for this ends up being IPC => S4 => LP => PA, where LP has the same modal behavior as S4, but whenever something is possible, LP carries a *proof* that it is possible. The upshot is that Lojban doesn't carry around those proofs, and so a lot of work will be required to infer them. See [4] or [5] for explanation.

There are totally non-logical particles that must be handled by parsers, like SA/SI/SU, so once again we have an immediate and satisfying consequence: No, baseline Lojban cannot be totally formalized at the syntactic level in terms of logic, and must be expanded first.

I hope that this is interesting food for thought. Yes, we must immediately agree that many parts of the baseline are not formalizable, and provably so. But the bulk of the baseline is gismu, and those are definitely related to each other, in addition to coding for relations in their own right. Where those relations can be formalized, we can derive rewrite rules. I haven't implemented them in code, but in la brismu, I give Peano arithmetic and basic manipulation of bridi, as well as a set-theoretic definition of {du} and {lo}; I think that there are concrete useful things to draw from formal efforts.

John E Clifford

unread,
Apr 2, 2021, 9:18:30 AM4/2/21
to loj...@googlegroups.com
Fascinating.  But since it is totally locked in to the structure (or lack of it) of Lojban, it is ultimately uninteresting.  The real question is to figure out what the structure of Lojan should be, given the structure of Language.  And, since that is not yet given, except very vaguely, that becomes the real question.  I think that, if the language question is answered, the Lojban (or whatever it wil finally be called) question will fall into place quite directly (though not easily).  But, since no one in this group is working on the basic problem, I don’t see the point of patching the leaky boat with more soluble paper.

--
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
Reply all
Reply to author
Forward
0 new messages