[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[lojban] Lojban is a logical failure
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.
[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/ac15b0d5-c27c-4d8c-a459-4f80e9970bddn%40googlegroups.com.