Foreword

A category is a deductive system. ~ Lambek, via Encyclopedia of Philosophy

This is the landing page for brismu: a relational interpretation of Lojban, a small book which provides logical rules for manipulating Lojban text.

This book is born from notes for a basic interpretation of Lojban using category theory. According to the Encyclopedia of Philosophy, there is a category for "any deductive system T with objects formulae and morphisms proofs." I present a deductive system for Lojban with a strong focus on relations, category-theoretic framing, and formalizability. In this system, Lojban is syntax for a special flavor of category -- a bicategory of relations -- forming a fictional universe.

This book comes in two halves. This half is written mostly in English prose. The other half is a formally-verified collection of proofs about Lojban written mostly in Metamath, a system for formalizing symbolic logic. The other half explains which bridi are logically provable; this half explains the meaning of the various axioms.

This book is addressed at folks who know Lojban and want to gain a deeper understanding of Lojbanic logic. If the reader does not know Lojban, then they may be somewhat mystified by the purpose of this work. For that reader, please consider Lojban as a sort of neutral speakable language for reading well-formed formulae aloud.

There are no mathematical prerequisites. Instead, the first few pages will rapidly build up all of the mathematical concepts which are required, and any additional concepts will be built as needed.

Coverage

Of the 1343 baseline valsi recognized as selbri (1342 gismu, 1 cmavo), 161 selbri are partially defined via formal rules. All 12 baseline abstractors (NU) are informally defined. Of the 8 classic articles (LE), 2 are informally defined.

In addition, 8 experimental selbri are informally defined, as well as 6 cnino selbri which did not previously exist.

Essential theorems

Formal coverage

The following table shows how many valsi have been formalized in handwritten Metamath, not including automatically-generated rules.

Ontology coverage

The following table shows how many selbri have been ontologized: given partial meaning relative to other selbri, but not necessarily formally defined.

Credits

The bulk of this work was gathered by la korvo. I greet and thank the following Lojbanists for input and insights:

• la bremenli
• la guskant
• la ilmen
• la poros
• la selgu'a
• la selpa'i
• la tsani

I also thank the following Lojbanists for proposing experimental valsi which I ended up using:

• la krtisfranks
• la lalxu

Praise from Lojbanists

"alien language" -- la gleki

"sad...pathetic, really" -- la cadgu'a

"no one cares about formalism" -- la xaspeljba

3: Categorical Relational Algebra

Let's investigate more properties of the category of sumti and selbri. In this section, we'll think categorically, and look for abstract patterns which show up elsewhere in logic. We'll look at products and coproducts, as well as internal homs. We will be guided by the properties of bicategories of relations and regular and coherent logic. In fact, I'm going to introduce some basic connectives, and then introduce the inference rules from Appendix B of this paper.

Typed restriction: {poi},

If we have the implication that a first-order value must be typed in order to be used, then we can transform the implication into a type restriction.

ro da zo'u da brode nagi'a bu'a
=============================== (poi-intel)
ro da poi ke'a brode zo'u bu'a

Why {bu'a}? Because we can logically weaken any bridi by adding irrelevant typed variables to its prenex, and so {da} might not be used. We'll add a rule just for this sort of logical weakening.

     bu'a
--------------- (da-weak)
ro da zo'u bu'a

Another {zo'e} convention appears here; restrictions can occur over non-unary selbri. For example, I might want to talk about cats with an utterance like {ro da poi ke'a mlatu}; in that case, the implicit {zo'e} should be read as {zi'o}; I am talking only about the cats themselves and not their species. This doesn't mean that we've cleaved apart cats and their species; because cats are still identified by {mlatu}, the inherent ability to be related is still present. In other words, we are keeping the type information.

Finally, we can have a dependent type; we can range over relations, and then range over elements of the relation. Again, observe the {zo'e} convention.

          ro bu'a zo'u bu'e
------------------------------------- (da-dep-weak)
ro bu'a ro da poi ke'a bu'a zo'u bu'e

Creation and Deletion:

Relationship diagrams can create and delete data. Note, though, that the underlying relation is not erased. This is important both for preserving the behavior of the remaining data, and also for running in reverse. When we reverse deletion, we get creation of data from within the surrounding bridi.

ro da poi ke'a broda zi'o ro de poi zi'o broda ke'a zo'u:

 da broda de
============= (zi'o-del)
da broda zi'o

We can erase any column of the relation this way.

ro da poi ke'a broda zi'o ro de poi zi'o broda ke'a zo'u:

  da broda de
 ==============  (se-intel)
 de se broda da
================ (zi'o-del)
de se broda zi'o
================ (se-intel)
 zi'o broda de

It is fair to ask, after the previous section, whether {zi'o} can be removed from underneath {poi}. No, there is a strict separation between quantification and relation in coherent logic, and so we need to complete our quantifications before we can do relational restrictions. We'll see how to make the syntax lighter in later chapters.

Internal homs: {ka}, {ckaji},

We can now search for the internal hom (WP), the construction which behaves like functions with closure. It turns out that relationally, internal homs are built from Cartesian products. To see this, let's see the universal property: Given a pair (X, Y^X), we can apply the latter to the former, and get a Y. So the universal property comes as a single arrow apply : (X, Y^X) -> Y.

ro bu'a ro da zo'u:

        da bu'a
======================== (ckaji-intel) [CLL 11.4]
da ckaji pa ka ce'u bu'a

We will use {ka} for selbri which have been closed over, with {ce'u} indicating where holes remain. Arity will matter; {ckaji} can only fill in one hole at a time. Why {pa}? Because there's only one way to perform the closure, up to unique isomorphism, and so the quantifier ought to be "there exists exactly one". This is a common property of universal properties, but it is very different from traditional Lojban quantification, where {lo ka} is used to generically select relations. A notable consequence is that, in rules like (ckaji-intel), we will not bind the {ka} to any name, but we will bind each {de} just the same in both the top and bottom.

So, where were those Cartesian products? One is hidden inside {da broda de}: each solution to this bridi is a pair (da, de) drawn from their Cartesian product! But the reader might reasonably object that there was no {de} in the prenex for (ckaji-intel). We can make a more explicit coupling with {ckini}, which does for binary {ka} what {ckaji} does for unary {ka}. Note that we use explicit {ce'u} to mark each hole and keep track of arity.

ro bu'a ro da ro de zo'u:

           da bu'a de
================================ (ckini-intel)
da ckini de pa ka ce'u bu'a ce'u

I can think of a few useful lemmas to try out. First, let's see if we can connect {ckaji} and {ckini} without any more rules.

ro bu'a ro da ro de zo'u:

   da ckaji pa ka ce'u bu'a de
   ===========================   (ckaji-intel)
           da bu'a de
================================ (ckini-intel)
da ckini de pa ka ce'u bu'a ce'u

Looks reasonable. What about the symmetry within {ckini}? Can we, say, put {se} underneath {ka}? Yes, we can.

ro bu'a ro da ro de zo'u:

 da ckini de pa ka ce'u bu'a ce'u
 ================================   (ckini-intel)
            da bu'a de
           =============            (se-intel)
           de se bu'a da
=================================== (ckini-intel)
de ckini da pa ka ce'u se bu'a ce'u

NFOL I: Rewriting selbri

We can actually perform generalized rewriting underneath {ka}. We'll give a two-dimensional rule for when we're allowed to do this. The key insight is that SOL relations must be able to consider any value; therefore, every {ce'u} ranges over {ro da}. Accordingly:

ro da zo'u:      || ... zo'u:
                 ||
da broda         || ... brodi pa ka ce'u broda
~~~~~~~~ (rule)  || ~~~~~~~~~~~~~~~~~~~~~~~~~~ (rule under ka)
da brode         || ... brodi pa ka ce'u brode

This rule is reversible! It is also NFO'd, since we need SO universal quantification in order to justify it.

Truth, Falsity: {cei'i},

Truth is not very interesting; in any context, we may conclude an empty, vacuous truth.

cei'i (cei'i) (bicat-truth)

More interestingly, we can be in a state of negation. From such a state, we have a principle of explosion, and we may prove anything. Relationally, from falsity there are no possible worlds, and so we may assign these zero possible worlds any imaginary properties that we like, since there are no witnesses to contradict our imaginations.

ro bu'a zo'u:

gai'o
----- (gai'o) (bicat-falsity)
bu'a

I've added a courtesy prenex, but (gai'o) is usually going to be an arbitrary bridi composed from already-introduced variables, so it won't be necessary.

I don't really like the cmavo for these predicates, but there are no good alternatives.

Singleton, Empty Set: {nomei},

First, we'll need our unit object. This object will only have one way to represent and relate data. We'll have this be a one-element set, or singleton set. The bridi {da pamei de} relates this set to its lone element. We would like to be able to say {le pamei}, and maybe we will eventually, but for now we'll have to designate the uniqueness of these sumti in a different way; we'll say {tarci.bu} for the singleton object.

ro da poi pamei ke'a zo'u:

da du tarci.bu (pamei) (bicat-singleton)

For the empty set, however, the elements don't exist. This is a form of negation.

ro da poi nomei ke'a zo'u:

gai'o (nomei) (bicat-empty)

Projection: {fa'u}, {nomoi},

To characterize pairs, we will enlist some helpers. {fa'u} designates ordered pairs of elements, like {le se remei}. We can address each member of a pair with {nomoi} and {pamoi} respectively.

ro da ro de zo'u:

da nomoi da fa'u de (fa'u-nomoi) (bicat-projection)

.i

de pamoi da fa'u de (fa'u-pamoi) (bicat-projection)

We have reached the point where we need at least four distinct sumti, and so we will need {xi} to give us additional names. Note that, as before with {gi'e} and {se}, the symmetry of our proof tree leads to a symmetry underneath {fa'u}.

Pairs:

We can also draw from pairs of relations. It's a bit verbose; we have to draw from the pair, and then lay out the cardinal and ordinal relationships with an existential quantifier.

ro da poi ke'a broda fa'u brode zo'u:

su'o de su'o di zo'u da remei de fa'u di .ije de nomoi da .ije di pamoi da (remei) (bicat-pair)

This is the first time we've used such existential quantifiers. Unlike the top-level prenex, each existential quantification is scoped and can nest, with order mattering. In general, existential quantifiers aren't for top-level values that we want to capture and manipulate, but for inner plumbing in composite expressions. We'll see in a bit how to introduce and eliminate them more generally.

Disjoint Unions and Inclusions: {.a}, {.onai},

We can form disjoint unions for sumti by using {.onai}, and for selbri by using {jonai}.

In lieu of a community-accepted selbri, I will use the placeholder {dijro}, with the following place structure:

d1 is a disjoint union with value d2 from amongst possible types d3

Which is a useless mouthful on its own, but can be made worse with {zulrdijro} and {pritrdijro}, which have place structures:

z1 is a left-hand/first/fixed disjoint union with value z2

p1 is a right-hand/second/varying disjoint union with value p2

This is enough to be able to create binary coproducts.

ro da ro de zo'u:

da .onai de zulrdijro da (zulrdijro) (bicat-injection)

da .onai de pritrdijro de (pritrdijro) (bicat-injection)

We can also eliminate binary coproducts if they're formed in the prenex, leading to disjunction. While binary coproducts have an XOR behavior, since disjoint unions can only take on one possible value at a time, disjunction of bridi allows for an inclusive OR behavior, and so we'll use a different word.

ro da poi ke'a broda jonai brode zo'u:

su'o de zo'u da zulrdijro de .ija su'o de zo'u da pritrdijro de (ija-intro) (bicat-case)

The existential quantifiers are not wrong; they are closely scoped to each component bridi. {de} ranges over two different types here, one for each side of the disjoint union. We will later have more formal handling for these sorts of quantifiers.

This next rule is part of proofs by contradiction. Since a disjoint union can't be in two states at once, if we have existential witnesses which see it in both states, then we can conclude falsity.

ro da poi ke'a broda jonai brode zo'u:

da zulrdijro de .ije da pritrdijro de
------------------------------------- (ije-false) (bicat-case)
                gai'o

Distributivity

Before we get to the difficult-to-visualize rules, let's handle the distributive law quickly. There is only one distributive law, and it relates {.a} and {.e} in a one-way derivation. For any three bridi in context:

      bu'a .ije bu'e .ijabo bu'i
-------------------------------------- (ija-dist) (bicat-distributivity)
bu'a .ijebo bu'e .ija bu'a .ijebo bu'i

This rule is reminiscent of, but not literally, CLL 14.8. We don't want to really deal with the syntax of {bo} in general, and it's just here for grouping; we will leave the full details of parentheses to the interested (and masochistic) reader.

Conjunction & Disjunction

We continue to be extremely general and work under a single fixed context. First, a pair of rules for dismissing conjunction:

bu'a .ije bu'e
-------------- (ije-left) (bicat-conjunction)
     bu'a

bu'a .ije bu'e
-------------- (ije-right) (bicat-conjunction)
     bu'e

And now, a new sort of diagram, for a two-dimensional rule. Here we will take pairs of rules on the left, and create a new composite rule on the right. This will allow us to cleanly combine pairs of rules in a natural way.

bu'a  |
----  |
bu'e  |       bu'a
      |  -------------- (ije) (bicat-conjunction)
bu'a  |  bu'e .ije bu'i
----  |
bu'i  |

I hope that this makes sense, because we're about to take the duals and do it all again. First, a pair of rules for introducing disjunction:

     bu'a
-------------- (ija-left) (bicat-disjunction)
bu'a .ija bu'e

     bu'e
-------------- (ija-right) (bicat-disjunction)
bu'a .ija bu'e

And then another two-dimensional rule for removing disjunction:

bu'a  |
----  |
bu'i  |  bu'a .ija bu'e
      |  -------------- (ija) (bicat-disjunction)
bu'e  |       bu'i
----  |
bu'i  |

Existential Quantifiers:

Once again, we are going to forge a two-dimensional rule. This one is reversible. On the left, we have a context which holds for all possible values; on the right, we have individual values which witness each instance of a relation.

ro da poi ke'a broda zo'u:  ||
                            ||  su'o da zo'u bu'a
bu'a                        ||  ----------------- (su'o-intel) (bicat-existential quantifier)
----                        ||        bu'e
bu'e                        ||

It is crucial to keep in mind that universal claims live at the top, at the prenex, and existential claims are scoped to particular formulae in the body.

Think carefully about this rule, in both directions, to be sure that it makes sense. From left to right, if a rule always holds under some context, and we can choose a value from that context which witnesses the first part of the rule, then we can conclude the second part. From right to left, if we have a conditional conclusion which is waiting for a witness, then for all of the possible witnesses, it would be the case that conditionally we could draw the conclusion given the premise.

Note also that we assumed that {da} was free. We will make this assumption a lot. In fact...

Frobenius

Let's give the Frobenius law. This rule allows us to stretch the scope of existential quantifiers and include many component bridi. For a final time, please assume a fixed context under which {da} is free.

bu'a .ije su'o da zo'u bu'e
--------------------------- (ije-frob) (bicat-Frobenius)
su'o da zo'u bu'a .ije bu'e

4: Lojbanic Relations

Ordered sequences: {ce'o}, {nomoi}, {pamoi},

{ce'o} builds ordered sequences, which generalize ordered pairs by having more than two elements. We will need some metasyntactic help to address these sequences in a uniform way; we want to be able to address each part of a sequence numerically. In the following rules, the ellipsis ... metasyntactically represents additional variables linked by {ce'o}, forming the "rest" or "tail" of the sequence. This tail could well be empty.

Note for the future: Experimental {ra'ei} could represent additional elements, but is in entirely the wrong selma'o.

ro da zo'u:

da nomoi da ce'o ... (nomoi)

ro de zo'u:

de pamoi da ce'o de ce'o ... (pamoi)

ro di zo'u:

di remoi da ce'o de ce'o di ce'o ... (remoi)

...

Ternary relations: {bridi},

This entire section rests on whether {bridi} is semantic or syntactic; that is, whether it operates on live sets and values, or Lojban ASTs.

At last, we can define {bridi}. First, let's relate it to other selbri. {bridi} internalizes the rule of {ckaji} and {ckini}, which instantiate relations. When we connect terbri to selbri, we are asking the selbri whether the given terbri are present in the underlying relation. This is precisely the characteristic function! We use {du'u} to track whether a bridi is satisfying the characteristic of its selbri.

ro da poi ke'a broda ro de poi broda ke'a zo'u:

                           da broda de
================================================================== (bridi-intel-2)
pa du'u da broda de kei bridi pa ka ce'u broda ce'u kei da ce'o de

Just like with {ka}, we only get one {du'u} bound at a time. A {du'u} is definitely inhabited or not inhabited. On the top of the rule, we have one result for every pair in the selbri; on the bottom of the rule, we have one result for every pair in the Cartesian product (the full relation), and also a {du'u} indicating whether or not the pair is also in the selbri.

Reactions have been mixed, to say the least, to this approach. la gleki opines that terbri do not work this way. However, CLL insists that selbri and bridi and {bridi} work this way. The main contention is what parts of the bridi are syntactic and which are semantic, since Lojban does support text literals.

For posterity: selbri are syntactic representations of semantic equivalence classes. This gives us isomorphism-invariance; any particular {pa du'u} really does only have one class of equivalent bridi underneath it. This has consequences for discursive logic, in that {lo du'u mlatu} should be taken as a vague pattern which the listener must disambiguate from context, and not as a literal reference to an equivalence class of logical sentences.

5: Set Theory

At this point, we are ready to give the axioms for set theory. We will be using ZF.

Functions I: {fancu}, {pagyfancu}, {ficyfancu}, {gairfancu},

We won't get far without functions, so we'll ignore the lack of community standard and start with {fancu}. We'll preserve the original place structure and sharpen the definition to, "f1 is a function with domain f2 (set) and range/codomain f3 (set) and underlying relation f4 (binary ka)." Under this definition, functions have types, and all functions are merely relations satisfying a functional property.

So, what's this functional property? There's actually a family of them, but we'll start with the most general ones. We're going to take a selbri {broda} and bend it around a little, to something like {de se broda da .ije broda di}, composing it with itself, which gives a self-relation on a set. Now, let's compare that self-relation to {da du di}; this gives us our family of functional properties.

The first property we'll build is univalence, sometimes called the functional property: A relation R is univalent if R's dagger composed with R lattice-implies the identity relation on R's codomain. Consider, for example, {mlatu}. If we take each cat species to its collection of cats, and then take each resulting collection to all of the species in each collection, then we arrive back at each individual species. More generally, for binary relations:

zo'u:

 pa ka ce'u .e ce'u broda de kei kairni'i pa ka ce'u du ce'u
============================================================= (pagyfancu-intel)
zi'o pagyfancu le'i broda le'i se broda pa ka ce'u broda ce'u

I'm not going to further use or define {le'i}. What's going on here? For lack of a better convention, f1 is the "name", or "handle", of the function; this is not just a label, but the actual reference by which functions are internally identified in the logic. The good news is that you should already know roughly what this means if I say {lo pagyfancu}; the bad news is that we're still going to be irritatingly formal about the whole affair. A similar deal applies to the sets in the function type; they are technically supposed to be references to types, but we don't have quantification over types (yet?)

And why {pagyfancu}? First, univalence only guarantees that we have partial functions, not total functions. So we have the definition, "f1 is a partial function with domain f2, codomain f3=p2, underlying relation f4, but only covering subset p1 of the codomain." There are two ways to get to total functions. First, we can trivially transform between partial functions on some set S, and total functions on S + 1. Accordingly:

ro da poi ke'a fancu zo'u:

                 da pagyfancu ko'a ko'e pa ka ce'uxino ce'uxipa bu'a
===================================================================================== (fancu-partial)
da fancu ko'a ko'e .onai le pamei pa ka ce'uxipa se bu'a ce'uxino gi'onai du tarci.bu

This rule was made larger by subscripts on the {ce'u} so that I could ensure that the arguments are in the right order. It's very bulky, and it adds an extra coproduct. Instead, we can show that there's another functional property, totality, which is sort of like a dual to univalence: A relation R is total if R composed with its dagger is lattice-implied by the identity relation. This is like doing a basic covering check to ensure that every value in the domain is mapped to at least one thing in the codomain.

ro da poi ke'a pagyfancu le'i broda le'i se broda zo'u:

pa ka ce'u du ce'u kei kairni'i pa ka ce'u .e ce'u broda de
=========================================================== (fancu-intel)
  da fancu le'i broda le'i se broda pa ka ce'u broda ce'u

So, for example, it is the case that {fancu le'i mlatu le'i se mlatu pa ka ce'u mlatu ce'u}; this function has the same data as the relation (it is a subset of the Cartesian product of cats and cat species) but we are now carrying additional information which proves that it is functional.

We can examine equality of relations, carefully. We can't simply ask whether relations are equal, but we can both witness it syntactically and also logically. First, if two relations lattice-imply each other, then they're equivalent.

ro da poi bridi ke'a ku'o ro de poi bridi ke'a zo'u:

da kairni'i de .ije de kairni'i da
================================== (kairni'i-sym)
            da du de

Now, if we don't just have lattice-implication in the univalence property, but full inversion, so that R composed with its dagger is equivalent to the identity relation, then R is an injection. The nonce lujvo {ficyfancu} has place structure, "f1, f2, f3, f4 as normal, and also for all x3 in f2, {x1 frica x2} => {f1(x1) frica f1(x2)}." As you can see, this definition got a little rich, but injections are complicated.

ro da poi fancu ko'a ko'e zo'u:

da fancu ko'a ko'e de .ije de kairni'i pa ka ce'u du ce'u
========================================================= (ficyfancu-intel)
                da ficyfancu ko'a ko'e de

Dually, surjections technically have more data but are specified in roughly the same way, with R's dagger composed with R yielding the identity relation. The nonce lujvo {gairfancu} has place structure "function f1 has domain f2=g1 covering codomain f3=g2 with the fact that for all x1 in f2, exists x2 in f3 with f1(x1) = x2."

Note that if f2 and f3 were proper sets, then {gacri} could be defined as, among other things, a covering set! This means that when we run (gairfancu-intel) in reverse, we are invoking the Axiom of Choice.

ro da poi fancu ko'a ko'e ku'o ro de poi bridi ke'a zo'u:

da fancu ko'a ko'e de .ije pa ka ce'u du ce'u kei kairni'i de
============================================================= (gairfancu-intel)
                  da gairfancu ko'a ko'e de

Finally, as a definition, a bijection is both an injection and surjection, with nonce lujvo {mitfancu}, "isomorphism f1 has domain f2=m1 and codomain f3=m2, and in that direction, has witnessing relation f4=m3."

ro da poi fancu ko'a ko'e ku'o ro de poi bridi ke'a zo'u:

da ficyfancu je gairfancu ko'a ko'e de
====================================== (mitfancu-intel)
       da mitfancu ko'a ko'e de

Injections are, more generally, monomorphisms. We give the universal property for monomorphisms in regular logic: if a monomorphism f sends two objects to the same value, then the objects are the same as well.

ro bu'a poi ficyfancu ko'a ko'e ke'a ku'o ro de ro di zo'u:

de mintu di pa ka ce'u bu'a ce'u
-------------------------------- (ficyfancu-mono)
            de du di

Similarly, surjections are epimorphisms. Epimorphisms capture existential quantifiers.

ro bu'a poi gairfancu ko'a ko'e ke'a ku'o ro da zo'u:

su'o de zo'u de bu'a da (gairfancu-epi)

And bijections really are isomorphisms; we can turn them around arbitrarily, and a little work will show that in each every case where there's an isomorphism, we can use our standard dagger. Maybe that's provable with what we've got, but I'll just give it as an axiom:

 ro da poi mitfancu ko'a ko'e zo'u da mitfancu ko'a ko'e pa ka ce'u bu'a ce'u
=============================================================================== (mitfancu-iso)
ro da poi mitfancu ko'e ko'a zo'u da mitfancu ko'a ko'e pa ka ce'u se bu'a ce'u

Subsets:

One of the two essential relations of set theory is {cmima}, which relates sets to their elements. Like in some flavors of ZF, in Lojban we cannot forget to which set an element belongs.

Remember, we are using relational logic, and a single set is related to each of its elements. {da cmima de} is, for each particular {de}, going to be true once for each distinct {da}.

The other essential relation of set theory is {steci}, which relates sets to their subsets using set comprehension. Interestingly, unlike most flavors of ZF, not only does Lojban preserve which superset each subset belongs to, but also the unary {ka} property which built it. When we run with steci2 and steci3 but not steci1, then this effectively selects a choice property out of thin air! Thus, just to implement {steci} will require us to adopt ZFC in full, including the Axiom of Choice.

Fortunately, we are in a position to do just that. We'll relate {steci} to surjections by choosing inverse functions.

ro da poi bridi ke'a ku'o ro de poi cmima ke'a ro di poi cmima ke'a zo'u:

         pa ka ce'u bu'a kei steci de di
================================================= (steci-intel)
zi'o gairfancu di de pa ka ce'u bu'a gi'e du ce'u

Read carefully. On the top, we have a unary selbri, and on the bottom, we invoke it as part of a binary selbri. You could read the bottom function as both calling the top relation as a subroutine on the input, and also copying the input to the output.

Also, I'm using live sets here, despite using labels earlier. Sorry not sorry. I'll keep figuring it out.

Functions II

We'll need to be able to compose functions. The easy way is probably through the front door.

ro da poi ke'a fancu ko'a ko'e ku'o ro de poi ke'a fancu ko'e ko'i zo'u:

da fancu ko'a ko'e pa ka ce'u bu'a ce'u kei .ije de fancu ko'e ko'i pa ka ce'u bu'e ce'u
======================================================================================== (fancu-comp)
           zi'o fancu ko'a ko'i pa ka de zo'u ce'u bu'a de .ije de bu'e ce'u

Maybe that's not so easy! We have to explicitly spell out all of the guts of our functions being composed, and don't have a high-level relation representing composition.

Elements:

Almost all sets have elements. In categories of sets, elements are functions from the singleton set. We need to carefully note an equivalence while allowing for distinction; this is part of the "name" concept of functions. A cat, for example, is not the same as the function which chooses it from the set of cats; it is, however, equivalent to the name of the function, and that's a sort of sameness.

As a compromise, the function corresponding to the element can be called, and calling the function will yield the element. Function calls, like relation traversals, are done with {ckini}.

ro da poi cmima ke'a ku'o ro de poi bridi ke'a zo'u:

            zi'o fancu le pamei da de
-------------------------------------------------- (cmima-elt)
su'o di zo'u di cmima da .ije tarci.bu di ckini de

The quantification is not great here. {di} ranges over the set of {da}, which is effectively a dependent type. This doesn't surprise me greatly, since I expected to find 2-categorical structure, but it will complicate the quantification story. From this point forward, quantification is sketchy.

Subset structure

We'll give the axioms in ornate form. First, the Axiom of Extensionality: If two sets have all of the same supersets, then they're the same set.

ro da poi cmima ke'a ku'o ro de poi cmima ke'a zo'u:

pa ka zi'o steci da ce'u kei du pa ka zi'o steci de ce'u
-------------------------------------------------------- (steci-ext)
                        da du de

Next, the Axiom of the Empty Set: The empty set has no subsets; the set of subsets of the empty set is itself the empty set. This phrasing uses the idea that unary relations are equivalent to sets, which I haven't formalized further. It is lazy and probably we can do better.

le nomei du pa ka zi'o steci ce'u le nomei (steci-empty)

The Axiom of Pairing: Every pair of sets belongs to a set which contains both of them as elements. My version includes the steci1 which builds that set.

ro da poi cmima ke'a ku'o ro de poi cmima ke'a zo'u:

su'o di zo'u da cmima di .ije de cmima di (cmima-pair)

Finally, the Axiom of Union: We may take the union of a set's elements, and it will again be a set. I'm not sure if I like the awkward phrasing I've used here; it might be better put with more {cmima} and no {steci}.

ro da poi cmima ke'a zo'u:

su'o de zo'u pa ka ce'u cmima da kei steci de zi'o (steci-union)

Inline sets:

We can now give {ce}, which is like {ce'o} but forgets order. Since order is forgotten, when I write {ce ...} I mean that the set's elements can be permuted arbitrarily.

ro da poi ke'a cmima zo'u:

da cmima da ce ... (ce-intel)

Incidentally, this gives the Axiom of Pairing in a lighter fashion.

Axiom of Anti-Foundation

Controversially, although nobody's really said anything yet, relational set logic tends to use the Axiom of Anti-Foundation, AFA, instead of the Axiom of Foundation.

AFA corresponds sets with rooted connected directed cyclic graphs; the root maps to the top of the set, and each path in the graph corresponds to a membership chain, with each edge being a single instance of membership. We will ask that our relations respect this structure when it occurs.

Articles I: {lo},

We are not quite yet to defining 1+1=2, but we have something just as great, {lo}. In xorlo, {lo} is a generic selection. For BPFK, {lo} is in the formal gadri definition list. Here we are relatively precise about what {lo} means, but we also use nearly the same definition as BPFK, only swapping {poi} for {noi} and not claiming any particular difference between the two.

Without further ado, the moment is here.

zo'u:

su'o da poi ke'a broda zo'u da brode
==================================== (lo-intel)
         lo broda ku brode

Note that {lo} folds a hidden bound value within itself, like with {zi'o}. In addition, the prenex was consumed. When we use {lo}, we no longer have a variable {da} bound in scope.

We can also do a {be} expansion. {be} creates a side condition which must be moved into the main formula.

su'o da poi ke'a broda ku'o su'o de poi broda ke'a ku'o zo'u da brode .ije da broda de
====================================================================================== (be-intel)
                 su'o de poi broda ke'a zo'u lo broda be de ku brode

We can use the two-dimensional existential quantifier rule here, though, and obtain a prenexed form which is more ergonomic:

ro de poi broda ke'a zo'u:

su'o da poi ke'a broda zo'u da brode .ije da broda de
===================================================== (be-intel)
               lo broda be de ku brode

Natural Numbers Object: {kacna'u}, {kacli'e}, {sumji}, {pilji}, {li}, {no}, {pa}, ...

The set of natural numbers is equivalent to the unary relation {kacna'u}. First, let's populate the set. {li} is grammar for a numeric constant literal, the metavariable PA matches any such literal, and the relation {kacli'e} sends Lojban natural numbers to their successor/increment. Nothing magical, just mundane and tedious. Then, zero is a natural number:

li no kacna'u (kacna'u-zero)

And any successor of a natural number is also a natural number:

ro da zo'u:

              da kacna'u
======================================= (kacna'u-succ)
su'o de zo'u de kacna'u gi'e kacli'e da

But zero is not a successor:

ro da zo'u:

da kacli'e li no
---------------- (kacli'e-zero)
     gai'o

And the natural numbers have structural equality:

ro da ro de zo'u:

su'o di zo'u da .e de kacli'e di
-------------------------------- (kacli'e-succ)
            da du de

This NNO is as strong as BA, the system of "baby arithmetic" obtained by weakening Robinson's arithmetic Q. To raise it up to Q, we need to remove all "pseudo-zero" non-successors:

ro da zo'u:

da kacna'u gi'e na du li no
--------------------------- (kacli'e-standard)
su'o de zo'u de kacli'e da

We also need to add arithmetic. For addition, we define {sumji}. First, anything plus zero is itself:

ro da zo'u:

   da kacna'u
----------------- (sumji-zero)
da sumji da li no

Anything plus a successor is the successor of that thing and its -- look, it's simpler in formal Lojban!

ro da ro de ro di zo'u:

su'o daxivo zo'u di sumji da daxivo .ije de kacli'e daxivo
---------------------------------------------------------- (sumji-succ)
su'o daxivo zo'u daxivo sumji da de .ije daxivo kacli'e di

Maybe not too much simpler. Multiplication is similar, with {pilji}:

ro da zo'u:

     da kacna'u
-------------------- (pilji-zero)
li no pilji da li no

Again, the recursive case is simpler formally than informally. Note the similarity between the top parts of both recursive cases.

ro da ro de ro di zo'u:

su'o daxivo zo'u di pilji da daxivo .ije de kacli'e daxivo
----------------------------------------------------------- (pilji-succ)
su'o daxivo zo'u di sumji daxivo da .ije daxivo pilji da de

So, to be explicit, how do we use these? Well, let's define {li pa} as an example.

li no kacli'e li pa (kacli'e-pa)

li pa kacli'e li re (kacli'e-re)

Imagine the axiom schema which builds the NNO; CLL gives the algorithm for counting, and it's largely the same as standard decimal integer counting.

NFOL II: NNO Categoricity

We can give the induction principle for natural numbers with SO quantifiers.

ro bu'a zo'u:

ge li no bu'a gi ro da su'o de zo'u da na.a de bu'a .ije da kacli'e de
---------------------------------------------------------------------- (kacna'u-ind)
                  ro da zo'u da kacna'u nagi'a bu'a

Quantification I: {no}, {pa}, ...

An essential quantifier in maths is the uniqueness existential quantifier {pa}. We can build it from a careful modification of the standard phrasing.

ro bu'a ro de zo'u:

su'o da zo'u da bu'a .ije de bu'a nagi'a du da
============================================== (pa-unique)
              pa da zo'u da bu'a

This lines up with both our intuitions on {ka} from earlier, and also our understanding of what uniqueness means: Any proclaimed witness to non-uniquess is, by contraposition, actually equivalent to our original thing.

Articles II:

Next, we have {lo'i}, which selects sets. Specifically, from the BPFK rule, we have our rule:

lo se cmima be lo broda cu brode
================================ (lo'i-intel)
      lo'i broda ku brode

Remember, we can't forget our relationships. But we also can't remember our forgotten properties. {lo'i} quantifiers are satisfied for each subset of the original set. If we had three things which {broda}, then we would bind eight different sets to {lo'i broda}.

Quantifiers II

We can also quantify {lo'i} to force them to have a specific cardinality. This is done merely by plumbing through the PA.

lo se cmima be lo PA broda cu brode da
====================================== (lo'i-pa-intel)
      lo'i PA broda ku brode da

Since there is only one subset with the same cardinality as the superset, there's only one way to bind this value. So, in effect, {lo'i} with a quantifier allows us to truncate and collect all at once.

Sets as Extensions:

{kampu} relates {ka} properties to their corresponding sets. We can give an axiom for {kampu} in terms of {cmima}, via {lo'i}.

pa ka ce'u broda kei kampu lo'i broda (kampu-def)

Quantifiers III

We can place a natural number directly onto a {da} in order to quantify it. The resulting bridi is, as before, all-or-nothing, based on the cardinality of results, but otherwise doesn't change the binding. However, since the typical {poi} clause ranges over an entire relation, the cardinality of results usually can be quite high, and as a result, quantifying {da} usually just leads to getting results in batches.

What's typical isn't guaranteed, though, so there's no rule that will add a quantifier to {da}. We can forget quantifiers, though, and that's a valid one-way weakening.

 PA da broda de
---------------- (pa-weak)
su'o da broda de

Placing a natural number as an outer quantifier onto {lo} selects subsets of the given cardinality from the entire set of results. This interpretation is congruent with what we can derive from applying existing rule (lo-intel) to an outer quantifier.

       PA lo broda ku brode
================================== (lo-intel)
PA da poi ke'a broda ku'o brode de

And similarly, putting an outer quantifier onto {lo'i} selects subsets of the already-selected subset. If there are four {mlatu} total under consideration, then {re lo'i ci mlatu} will first select three cats, then select two of those, binding a total of twelve times.

CLL allows for {PA broda} to be shorthand for {PA lo broda}.

PA lo broda ku brode
==================== (pa-lo-sugar) [CLL 6.8]
 PA broda ku brode

BPFK defines {PA broda} as {PA da poi broda}. That sounds familiar, and indeed, we can recover this definition from a proof.

        PA broda ku brode
       ====================        (pa-lo-sugar)
       PA lo broda ku brode
================================== (lo-intel)
PA da poi ke'a broda ku'o brode de

Negation:

We now open the door to the ability to say no. First, note that the outer quantifier {no} can effectively act like a negation: If there are zero results, then we succeed, and if there are any results at all, then we fail. This is a gentle extension of negation as failure; this is failure as negation.

So, for unary selbri, we can start out by saying:

ro da poi ke'a broda zo'u:

no da broda
=========== (na-no-unary)
da na broda

But this is thorny for binary selbri. We will have a pair of one-way rules which have a round-trip in one direction but not the other.

ro da poi ke'a broda ro de pok broda ke'a zo'u:

no da broda no de
================= (na-no-binary-both)
 da na broda de

If we made this two-way, then {na} wouldn't always be dual to {no}.

ro da poi ke'a broda ro de pok broda ke'a zo'u:

no da broda de
-------------- (na-no-binary)
da na broda de

Logical Set Operators: {ja}, {jo'e},

By flipping around the universal properties, we can build some operators and also define more logical connections. First, let's define {ku'a}, the intersection of two sets.

     lo'i broda je brode ku brodi
====================================== (ku'a-intel) [CLL 14.15]
lo'i broda ku ku'a lo'i brode ku brodi

We know what {jo'e} is, too; it's the union of sets. We have the disjoint union already, and the non-disjoint union simply forgets that its components come from one option or another. What is {ja}, though? Traditionally, in classical logic, it's an inclusive Boolean OR. We need to preserve all of the related data, though, and for the OR operation, it's whether only one of the branches is taken, or both are taken. Those cases are themselves disjoint, and so we have an equivalence:

ro da ro de zo'u:

da broda jonai brode jonai ke broda je brode de
=============================================== (ja-intel)
            da broda ja brode de

This is an awkward amount of data. But now we can define {jo'e}:

     lo'i broda ja brode ku brodi
====================================== (jo'e-intel) [CLL 14.15]
lo'i broda ku jo'e lo'i brode ku brodi

Tracing back through the data, on the bottom of the equivalence, we have elements belonging to one set or the other or possibly both.

6: The Logical Language

Let's talk more about {du'u}. For many folks, {du'u} is the core of what makes Lojban logical; it is how we talk about propositions. What we can internalize under {du'u} are the one-way conclusions that can be drawn using classical logic. It is crucially important to understand that, while the relational and classical parts of Lojban do interact, the relational logic is the outer layer which hosts the classical logic inside.

Contradiction:

Relational logic is infamously squishy and gooey, with genuine witnesses to contradiction being rare. Nonetheless, there's at least one, based on the characteristic functions: a selbri cannot simultaneously relate given terbri and also not relate them.

ro da poi ke'a broda ro de poi broda ke'a zo'u:

pa du'u da broda de kei natfe pa du'u da na broda de (natfe-na)

natfe3 will be left blank as part of a convention of not specifying which logical system we are working under; it's still accessible, but we won't insist on it being any particular value.

List of {du'u} logic gismu

• {nibli}: x1 implies x2; poset (reflexive, antisymmetric, transitive)
• {natfe}: x1 contradicts x2; not clear whether symmetric
• {kanxe}: x1 is the conjunction of x2 and x3
• {vlina}: x1 is the disjunction of x2 or x3
• {sigda} [exp]: x1 is the material implication x2 => x3
• {tsida} [exp]: x1 is the material biimplication x2 <=> x3

7: Upward

Let's start tackling arbitrary easy gismu. Some/all of this can be merged with the new sections in the next chapter.

Example elements:

{mupli} is a straightforward combination of what we've already seen.

ro da ro de poi bridi ke'a ku'o ro di poi cmima ke'a zo'u:

da ckaji de gi'e cmima di
========================= (mupli-intel)
     da mupli de di

What's the difference between {mupli} and {fadni} here?

Restrictive Apposition:

Let's use some linguistic terminology. A restrictive appositive clause combines a relative clause with an identity relation. CLL 8.3 says that {po'u} means {poi du}, and we'll go with it.

ro da ro de zo'u:

da poi ke'a du de broda
======================= (po'u-intel) [CLL 8.3]
   da po'u de broda

Reciprocity:

simxu1 is a set, and for each pair of elements in the set, the selbri simxu2 relates that pair. We can give a very plain definition based on that description.

ro da poi cmima ke'a ro de poi ke'a cmima ro di poi ke'a cmima zo'u:

         de broda di
============================== (simxu-intel)
da simxu pa ka ce'u broda ce'u

Once again, since we are working relationally, we get many different sets, each of which satisfying the reciprocality property that we are designating.

Signs: {sinxa}, {la'e}, {lu'e},

As in CLL, we can define {la'e} and {lu'e} as shorthand for {sinxa}. Note that symbols and interpretations are things, and thus are subject to quantification.

ro da poi sinxa ke'a zo'u:

lo sinxa be da ku broda de
========================== (lu'e-intel) [CLL 6.10]
  lu'e da lu'u broda de

ro da poi ke'a sinxa zo'u:

lo se sinxa be da ku broda de
============================= (la'e-intel) [CLL 6.10]
    la'e da lu'u broda de

I recall discussion about whether sinxa3 is implicitly {mi} or {mi'a} or some similar connection to the speaker. However, I am not sure whether this is a cultural convention, and at any rate, leaving sinxa3 unbound allows for more flexible usage.

Additionally, {lu'i} and {lu'a} can be defined as {lo'i}-like expansions of {sinxa} which include a set quantification. These definitions are only hinted at in CLL, and were explored by la xorxes.

ro da zo'u:

lo sinxa be lo cmima be da ku broda
=================================== (lu'a-intel)
           lu'a da broda

lo sinxa be lo se cmima be da ku broda
====================================== (lu'i-intel)
            lu'i da broda

8: Abstractors

The basic idea behind abstractors is to take a selbri/bridi and produce a new selbri. Note carefully that the abstractors come in two families, depending on whether they take selbri or bridi. What's the difference? A selbri has {ce'u} slots open, and thus has an arity; it's a relation, after all. A bridi, however, is a concrete state of values being related by a relation (terbri related by selbri). They aren't the same type of thing.

"Hold on," you might object, "but what about nullary relations?" On one hand, yes, okay, the two selbri {cei'i} and {gai'o} are also bridi, because of this. But they're the only ones! All other nullary relations are isomorphic to one of those two.

"Hold on again," you might continue, "but don't all NU syntactically permit {ce'u}?" Yes, that's a fair objection. However, it is a well-established community standard that {du'u} and {nu} do not capture {ce'u}, and further that they capture fully-applied predicates with truth values.

First, {ka}. We understand {ka} pretty well by now; when we informally talk of e.g. {mlatu}, we are talking of {pa ka ce'u mlatu ce'u}, or mlatu/2, the binary relation which is inalienable from the text {zo mlatu}.

Next, {du'u}. We haven't yet dug into these, but they are fully constructed bridi; {lo mlatu ku cadzu} is represented as {pa du'u lo mlatu be zo'e ku cadzu zo'e zo'e}. Folks like to imagine these as having definite truth values, and it's tempting to join in; after all, surely every relation either does or does not contain a given row, right? Well, if we do that, then we actually hobble our logical power! It seems strange, but classical logic loses the ability to consider certain kinds of infinite objects if it would take infinite time to determine their truth value in a true-or-false context. What we can give is something nearly as good: Every subset of some set S has a complement relative to S. When S is a Von Neumann universe (a powerset of an ordinal, basically), then the elements of S have a bounded set theory that does allow for Boolean logic.

"Hold on," you might object, "but this sounds like romantic hogwash." There are two ways to look at it. One way is computationally: We can't know whether some element is definitely in a set or not without running a program, and that program can take forever. We can't tell if a real number is equal to zero or any other real number without running a program forever, either. Another way is logically: Gödel et al. have rigorously showed us that there's no way to just assign a truth value to an utterance like {nei na fatci}. Either way, it's very solid, and Boolean logic can either be classical, and have a gaping hole where we can be convinced of things that we can't build, or constructive, and have a lot of times where things are true, false, or not false; zero, non-zero, or not non-zero; infinte, finite, or not finite. For extra fun, we can say "not" as "not yet known to be, but maybe if we run the program just a little longer..." This is Turing's undecidability.

Okay, that's where we've been. Now let's go to new places.

Amounts: {jei},

Despite incompleteness, truth values are still limited to "true" and "false"; a relation either has or doesn't have (or is incomplete on) a row. We can enrich any relation by adjoining some type and using its elements to decorate rows, and we can use that enriched data in our characteristic function. Now, a row isn't simply present or not present, but present and annotated or not present.

First, let's generalize presence. Some selbri will have a hidden column for the likelihood that the relation holds, expressed as a classical probability in the unit interval. These are fuzzy sets. Fuzzy sets happen to need a universe relative to which to establish their probability distributions, which happens to just be the way in which subsets were given the ability to have complements in my earlier rant.

For now, I can't find any gismu which would directly allow accessing fuzzy membership probabilities, so I'll hold off on axioms, but the idea is roughly that a {du'u}, which is a proof of membership, could be traded freely for a {jei}, which indicates the degree of membership.

For {ni}, the story could be much brighter. We could imagine bending around a wire from a {ka}, so that {pa ka ce'u broda ce'u} could become {pa ni ce'u broda}, with broda2 becoming the measurement somehow. Questions abound, including why broda2 and not broda1, whether the arity change is correct, and how arithmetic evaluation interacts with the whole shebang. Nonetheless, the core theory is the same: Treat a numeric column as a numeric per-row annotation, and create a new abstracted relation which bends the wires. This makes {ni} like a subtype of {ka}, although the as-parent-type and the as-true-as relation send {ni} to different {ka}.

Events: {nu}, {mu'e}, {pu'u}, {za'i},

Now for tougher food. What is an event? For starters, an event happens. We'll think of this again in terms of annotations. Let's imagine some sort of spacetime coordinates around which the event is happening. Formally, the event has a spatiotemporal neighborhood. Within that neighborhood, the event is happening; outside that neighborhood, the event is not happening. Immediately, there is the problem where we cannot tell if an event is one instance, paused and resumed, or two instances; it's not obvious just by looking at the neighborhood. So we will have to be better about quantification. The good news is that universal and existential quantification should still work; the bad news is that we will need to allow more than just {pa nu} formation, because an event might have more than one neighborhood within which it is occurring.

Also, {nu} doesn't capture {ce'u}, so immediately we know that it abstracts over bridi, not selbri.

CLL says that each of the different event abstractors could be replaced with {nu}, being just as true, just less structured. We could take that to imply that there's structure within each specialized event abstractor.

First, {mu'e}, which treats events as points in spacetime. On one shoulder, quantum mechanics tells us that point idealizations are bogus; on the other shoulder, from the definition of "neighborhood", if we zoom out far enough from an event then we should eventually find a reference frame from which the entire event is visible. It follows that {mu'e} asserts that the neighborhood of an event is connected; if it wasn't actually connected, then we're imagining the smallest ball/neighborhood which contains all of the pieces and is connected, but technically we should only be allowed to go one-way on this. When we go from {mu'e} to {nu}, we forget connectedness.

Next, {pu'u}, which breaks events into stages. Obviously, I am biased about how rich a composition of stages should be, but for starters, let's imagine serial algorithms. pu'u2 would merely be a sequence of component events which, when composed in order, yield the entire event. So, with processes, we're talking about events which are decomposable, regardless of whether or not they're connected. But, also, they're composed in an order. Spacetime's events are only partially ordered, so we're asserting that these particular components are actually causally related. Putting this all together, pu'u2 is a totally ordered sequence of events, and pu'u1 is the smallest neighborhood which contains them.

Guh, that one was tough. But {za'i} is much easier. CLL says that continuous states have sharp boundaries. So their neighborhoods also have boundaries.

Finally, we have {zu'o}, for activities. An activity recurs many times within its neighborhood, and although each zu'o2 action is clear, the entire zu'o1 might not be. To give an example, imagine stirring a mixture. A zu'o2 would be a full rotation of the stirrer, while a zu'o1 might contain multiple incomplete rotations. Just like with {pu'u}, zu'o2 is an ordered sequence; the activity of walking consists of two symmetric, but chirally distinct, actions, for example.

CLL 11.11 explains that event contours aren't available for all subtypes of event. The only one always available might be {ca'o}. We also should be able to zoom out and get {co'i}. Imagining a sheaf, we might expect that the subtypes have more contours. {pu'u} has all contours, while {mu'e} adds only {pu'o} and {ba'o}; CLL forbids {ca'o}, but if we can zoom out, then we can zoom in.

Finishing up, both {za'i} and {zu'o} allow {pu'o}, {ba'o}, and {ca'o}, and {za'i} also has {co'a} and {co'u}.

Minor abstractors: {li'i}, {si'o},

CLL lumps these in a "minor" page, and I guess I will too. {li'i} is a subjective {nu}; li'i2 is the experiencer of the event. Not much more to say for now; we'll have to get to subjective experiences for this to be useful.

{si'o} is similar, but vague. si'o2 is an agent who is imagining a bridi. Can {ce'u} appear underneath? Nobody knows.

{su'u} is theoretically essential for constructing abstractors, but CLL doesn't give us enough information for how to wield it. It's not even clear whether {ce'u} are bound, although many folks believe so.

Summary of Abstractors

Adjunctions

There are several spots where Lojban has adjoint operators.

Abstractor adjunction: {jai},

The general idea is {da jai broda} <=> {tu'a da broda}.

Mekso adjunction: {na'u},

{na'u} sends mekso operators to selbri, and {nu'a} sends selbri to mekso operators. In both cases, arity is implied.

We get several rules from this. First, for selbri like {sumji}, we have a bijective correspondence between the selbri and the operator:

ro da ro de ro di zo'u:

  da sumji de di
================== (su'i-na'u)
da na'u su'i de di

And since it's a bijection for each individual operator, we get a cancellation rule as well:

ro bu'a zo'u:

na'u nu'a bu'a
============== (na'u-adj)
     bu'a

Note that there's additional structure here which we'll have to explain in mekso; {su'i} is n-ary (binary minimum?) but {sumji} is always binary.

Table of VUhU operators and selbri

Not listed:

• cu'a
• ju'u
• ne'o
• pa'i
• re'a
• pi'a
• sa'i

Equivalence Relations

• dunli
  • Insists that it is not simsa
  • Could be the gismu version of du, somehow
  • Could be entailed by zmadu + mleca
  • Could entail both zmadu and mleca
• mintu
  • Comes with several axioms which we can take for now
    • x du y <=> x mintu y pa ka ce'u du ce'u
      • ...might have misunderstood, might be: pa ka ce'u du
      • "no standards place"
  • Might generalize to equivalence relations
    • Given equiv broda, x broda y <=> x mintu y pa ka broda
  • Shows up in gismu.txt!
    • x lazmi'u y <=> x mintu y pa ka ce'u cmima da poi lanzu
    • Note: lanzu1 is therefore set, not mass!
    • This is unary {ka}; I would have used {simsa} instead of {mintu}
      • Maybe {mintu} is the right choice for binary {ka}?
• mapti
  • Still no real confidence in what's going on, mapti3 usually omitted
  • Best guess: bijection!
    • x mapti y pa ka ce'u broda ce'u <=> x broda y, also broda is a bijection
  • Suggests that lots of casual usage of mapti should actually be ckini
    • Because x mapti y z => x ckini y z
  • Similarly, la xorxes' definition of mapti implies ^^

Discursive Logic

On top of the formal ingredients, we should imagine that most conversational Lojban takes place in a discursive modal logic, not Loj or Selb. This is where words like {lo} and {le} can be properly defined. Consider:

lo mlatu ku mlatu

This bridi does not have explicit quantifiers. Whether it is true depends on which universe of discourse we use to interpret it. For example, the empty universe should, in some sense, not satisfy it, because {lo mlatu} should refer to something which the speaker doesn't have in mind yet but which still exists. The act of clarifying referents leads to argument over the contents of the universe of discourse, and so deserves its own treatment apart from mathematics and hard sciences.

Restrictive and non-restrictive clauses

It's not clear what the difference between {noi} and {poi} is, but it is a discursive difference: there is no change in logical content, but something is denoted to listeners.

0: Endorelational gismu

We cover some essential relational properties of the baseline gismu. We'll use the notation x R y to indicate relation R relating elements x and y.

We'll focus on binary relations where both elements of each pair are drawn from one single underlying set. This lets us consider equality on related elements.

Reflexivity

A reflexive relation contains at least, for every element x in the underlying set, x R x.

I don't know of any gismu which are reflexive but not equivalence relations. Still, were there any, they'd get the following formal rule.

ro da ro de zo'u:

 da du de
----------- (broda is reflexive)
da broda de

For any gismu which is reflexive, just substitute into the above rule.

Irreflexivity

An irreflexive relation omits any pair which a reflexive relation would be required to have. For every element x in the underlying set, x ~R x. Since we only care about endorelations, we won't mention relations like {mlatu} which would otherwise trivially be irreflexive.

ro da zo'u:

da na broda da (broda is irreflexive)

Examples of irreflexive relations:

• {frica} for some (currently poorly-understood) frica3
• {drata} for any particular drata3

Transitivity

A transitive relation turns chains of related elements into transitive closures, which are subsets of the underlying set characterized by the heads of the longest chains. For any three elements x, y, and z, if x R y and y R z then also x R z.

ro da ro de ro di zo'u:

da broda de .ije de broda di
---------------------------- (broda is transitive)
        da broda di

Examples of transitive relations:

• {zmadu} for any particular zmadu3 metric and zmadu4 value of the metric between zmadu1 and zmadu2
• Similarly, {mleca} for any particular mleca3 and mleca4
• {barda} for any particular barda2
• {cmalu} for any particular cmalu2
• {diklo} for any particular diklo3
• {nenri}
• {nibli} for any particular nibli3
• {rinka} for any particular rinka3

An example of a not-quite-transitive relation is {dzena}, because dzena3 needs to be composed during each transitive step. This is a common failure, indicating a need for composition in order to build the implied transitive structure. Or perhaps just {dzena fi zi'o}, not sure.

Symmetric

A symmetric relation freely interchanges the elements in its pairs; whenever it is the case that x R y, it is also the case that y R x.

ro da ro de zo'u:

da broda de
=========== (broda is symmetric)
de broda da

The rule for symmetric relations is also symmetric, which I find pleasant.

Note that symmetric relations are like involutions, in that when composed with themselves they yield the identity relation {du}. However, they need not be functions.

Examples of symmetric relations:

• {fatne}
• {dukti} for any particular dukti3
• {rimni} for any particular rimni3 and rimni4
• {darno} for any particular darno3
• {jibni} for any particular jibni3
• {jorne} for any particular jorne3
• {sepli} for any particular sepli3
• {sirji} for any particular sirji1
• {cabna}
• {cinba} for any particular cinba3
• {cripu} for any particular cripu1 and cripu2
• {natfe} for any particular natfu3

Antisymmetry

An antisymmetric relation is like a symmetric relation, but degenerates whenver elements overlap. Specifically, if x R y and also y R x, then in fact x = y, x R x, and y R y.

ro da ro de zo'u:

da broda de .ije de broda da
---------------------------- (broda is antisymmetric)
          da du de

Antisymmetric relations need not be reflexive, but in that case their graphs will not have cycles.

Antisymmetric relations can be symmetric too, but they will always degenerate to diagonal relations in that case.

• {balvi}
• {purci}

Equivalence relations

Any relation which is reflexive, transitive, and symmetric, is an equivalence relation.

Every equivalence relation creates a partition on the underlying set, called the partition into equivalence classes.

{dunli} indexes the equivalence relations; dunli3 (ka) is a binary relation which sends both dunli1 and dunli2 to some unseen comparison key, and witnesses that they would be in the same equivalence class if quotiented by dunli3.

What's the difference between {dunli} and {simsa} and {mintu}?

Examples of equivalence relations:

• {du}
• {dunli} for any particular dunli3
• {panra} for any particular panra3 and panra4

Partial order

Any relation which is transitive and antisymmetric is a partial order.

Examples of partial orders:

• {lidne} for any particular lidne3

It is possible that {lidne} is defined as "there is an arrow from x1 to x2 in partial order x3", which would be a remarkably powerful and general relation. Similarly, {porsi} might be "x1 (poset) is the partial order arising from order x2 (binary ka) upon set x3".

Connectedness

A relation is connected if, for all pairs of values x and y, either xRy, yRx, or x=y. Equivalently, x≠y => xRy / yRx.

Serial relations

A relation is serial if it is irreflexive, transitive, and connected.

Well-founded

A relation is well-founded if it contains no infinite descending chains. Equivalently, every non-empty subset of the domain has a minimal element.

Well-order

A relation is a well-order if it is transitive, antisymmetric, connected, reflexive, and well-founded.

moi3 needs to be a well-order so that its domain moi2 can be given an order type. Or, put another way, moi2 is shown to have order-type moi3 (given as an expression for a binary relation).

Lesniewskian

A relation is Lesniewskian if it is transitive and also:

da broda de
-----------
da broda da

And:

da broda de & de broda di
-------------------------
       de broda da

1: (Lack of) Basis

Lojban has multiple possible bases in the baseline gismu. This is okay! It means that some gismu are interexpressible in terms of one another. We should both celebrate and document it.

Exponentials & Logarithms

Both {tenfa} and {dugri} have exactly the same terbri, just in different orders. Both relations are the same as Sanderson's Triangle of Power; they relate a base, an exponent, and a power.

Trigonometry

Can {sinso} be replaced with {tanjo}?

The community lujvo {dutsinso}, for cosine, could be defined in terms of {sinso} sine.

Size relations

{barda} and {cmalu} are inverses.

2: Posetal logic

We now focus on relations which have posetal inner structure.

Suppose, for some two {broda} and {brode},

ro da ro de zo'u:

da broda de
----------- (rule)
da brode de

By some rule. The quantifiers need to be {ro}, but they can be typed/restricted with {poi}. Then, there is an inner implication, which I'm calling the posetal implication, from {broda} to {brode}. These implications are called "posetal" because they are structured like posets (WP, nLab):

• Chained implications are like transitivity
• Equivalences are like antisymmetry
• Conjunction and disjunction work like in posets
• The top and bottom relations are the trivially true and false relations

This structure, interacting with the normal relational logic, is what produces our categorical allegory structure.

Now, without further ado, let's introduce a two-dimensional rule for this inner logic. We recall {kairni'i} from set theory; the posetal logic is exactly the logic of the lattice of relations that we introduced earlier. Here, rather than using the lattice properties to build functional properties, we'll focus on the poset properties.

ro da ro de zo'u:  ||
                   ||
da broda de        || pa ka ce'u broda ce'u kei kairni'i pa ka ce'u brode ce'u (rule is posetal)
----------- (rule) ||
da brode de        ||

On the left, standard one-dimensional rules of the sort we've been working with let us proceed in standard deductive style. On the right, we have axioms which let us start proofs with posetal facts.

We can remove typed restrictions from the LHS's prenex as long as they're removed from both the top and bottom.

Notation: Posets

Throughout the rest of the book, we will use graphical syntax for posetal relations. When we write a diagram like:

We mean that {brode} and {broda} are both binary relations which are related by {kairni'i}:

ro da ro de zo'u:

da brode de
----------- (brode => broda)
da broda de

Families

Many selbri naturally exhibit posetal structure, particularly the saske valsi, which have a dedicated upcoming chapter. The structures are useful for classification, comparison, and theorizing. A posetal family is a collection of (at least two) selbri which are connected by posetal structure.

A good example of a posetal family would be {danlu} and its subrelations. Each member of the family gives a rule like:

ro da ro de zo'u:

da mlatu de
----------- (mlatu => danlu)
da danlu de

I give the entire family of animals in the appendix; here is a small slice:

Notation: Restricted Arity

A student of the baseline will notice that {tirxu} is defined with three places. By "tirxu/2" we mean that the third and following places are filled with {zi'o}, as previously discussed. We could more explicitly write:

This is often useful in smoothing out the baseline gismu. If places need to be permuted first, then an explicit {se} conversion will be given.

Functional Properties

Recall the four functional properties of univalence, totality, injectiveness, and surjectiveness, as well as bijections, which are both injective and surjective. Now, let's try to find these properties within the baseline!

The family of animal selbri mentioned above all follow the basic pattern of being surjective functions from danlu1 to danlu2.

3: Common places

There are some places which are common to many gismu.

"Orbital parameters" are found in:

• mluni4
• plini4

"Gravity wells" (sometimes just "gravity") are found in:

• cpana3
• farlu4
• gapru3
• lafti4
• pinta2
• sraji2

"Reference frames" or "frames of reference" or "frames-of-reference" or etc., but not including gravity, are found in:

• berti3, snanu3, stuna3, stici3

"Epistemology" places are found in:

• djuno4
• jetnu2, jitfa2
• jinvi4
• zasti3
• jei2

These places seem to want selbri which each have a {du'u} place, specifically:

• jijnu, with jijnu2
• smadi, with smadi2
• sruma, with sruma2
• xusra, with xusra2

These all have an x1 for the epistemic agent.

Is {milxe} like a fuzzy {ckaji}? Is {prani} a maximum of fuzzy membership?

{jbini} says that jbini3(jbini1) is within the bounds laid out by jbini3(jbini2), and also jbini1 is in jbini2.

{ralju} says that ralju3(ralju1) is the greatest of all ralju3(ralju2), and also that ralju1 is in ralju2.

{traji} says that traji2(traji1) is the greatest (using traji3 for comparison) of all traji2(traji4), and also that traji1 is in traji4.

{bancu} says that bancu4(bancu1) and bancu4(bancu3) are separated by boundary condition bancu2.

{jibni} says that jibni3(jibni1) = jibni3(jibni2) + o(e) for some small e.

{zmadu} says that zmadu3(zmadu1) = zmadu3(zmadu2) + zmadu4, more or less.

{mleca} says that mleca3(mleca1) = mleca3(mleca2) - mleca4, mirroring {zmadu}.

match as in [measurement/match]

CLL measurement gismu always have x1 with the measured object, and x2 {li}. This rhymes with {ni}.

4: Space & Time

General issues:

• What is a frame of reference, exactly? If it's manri1, then what's the rest of {manri}? Are there default frames of reference?

Space

2D Euclidean

The flat plane should be addressible with two dimensions. We have four words:

• berti: north
• snanu: south
• stici: west
• stuna: east

These words all have a nice Euclid-like property; they are all defined as something like "x1 is translated in [the opposite of] one of the basis vectors relative to x2 in frame of reference x3", where a frame of reference is something like an origin and choice of three axes forming a unit basis.

These words are all relative:

da berti de di <=> de snanu da di
da stici de di <=> de stuna da di

There is a note that {berti} should accord with right-hand rules; given a 3D space and a vector, we should use the right-hand rule to address the 2D bivector which spans the obvious subspace (that is, the flat plane which is perpendicular/tangent to the given vector.)

These words should generalize to any locally-Euclidean manifold, including physical approximations. The obvious desire is to have them work on Earth, where a frame of reference is a choice of (north) pole, and the right-hand rule then gives the traditional meanings of "north", etc.

Other Words

• The cmavo: be'a, ne'u, du'a, vu'a

3D Euclidean

Similarly, flat space should be addressible with three dimensions. We should have six words:

• crane: forward
• trixe: backward
• zunle: leftward
• pritu: rightward
• gapru: upward
• cnita: downward

With axioms of relativity:

da crane de di <=> de trixe da di
da zunle de di <=> de pritu da di
da gapru de di <=> de cnita da di

Other Words

• The cmavo: ca'u, ti'a, zu'a, ri'u, ga'u, ni'a
• dizlo?

Spacetime

Spacetime might have to be defined with a compound of some sort.

There are four tenses. They have no frames of reference; instead, they are defined using relativity, by considering regions of Minkowski spacetime which are (naturally) invariant (up to Lorentz transformations between inertial viewers). This invariance means that we don't have "x1 is temporally related to x2 according to frame of reference x3", but instead "x1 is spatiotemporally related to x2 (regardless of frame of reference)".

• balvi: futureward
• purci: pastward
• cabna: here and now
• xlane: elseward

We'll construct events in a moment, but first consider points. If we only acted on points, then the causal structure implies that either one point causally occurs before the other, or the two points are clearly disjoint, or the points are nearby each other and possibly equivalent or equal depending on topological axioms. We'd like for this to be a strict disjunction, and it is — for points. We can at least note that spacetime diagrams can be turned upside down:

da balvi de <=> de purci da

Lorentz transformations preserve inaccessibility:

da xlane de <=> de xlane da

Equivalence is symmetric:

da cabna de <=> de cabna da

Finally, physical causation is always of the spatiotemporal variety:

da rinka de ... => da balvi de

Events

So, now let's crack open the table of event abstractors. We'll start with very simple cases: connected regions of spacetime with boundaries. Such regions can overlap and also be large enough to span multiple portions of a spacetime diagram, which complicates our reasoning. We have some hints from baseline definitions; {balvi} and {purci} both indicate that they are aorist in that they do not exclude each other, and {cabna} does not exclude either of them either.

But now we get into nuanced questions. Suppose {da balvi de} and {da purci de}. Does it follow that {da cabna de}? Well, no. But if {da} is connected, then either {da cabna de} or {da xlane de} (or both), because there has to be some path from past to future, either through the present or elsewhere.

Open Questions

But what is rinka3? Conditions?

CLL 10.7 says VIhA series {vi'i}, {vi'a}, {vi'u}, {vi'e} correspond to "cognitive" or "essential dimensionality", and specifically it sounds like a generalization of manifolds and projections. A {vi'i} action is 1D, but it occurs in 3+1D spacetime; {vi'i} indicates that the data of the action is linear. Even curves (CLL gives walking on a mountain) can still have low-dimensional data.

CLL 10.7 says that FAhA could be augmented with "pastward" and "futureward" directions.

Fourth tense PU is {xa'ei}, VA is {xa'e}, SELBRI is {xlane}, all experimental.

{ta'e} requires agentivity. The other three can be explained in terms of the event covering its spacetime interval.

CLL 10.23 clearly enunciates two sets of equivalent bridi families. The first are using BAI tags:

X .i BAI bo Y <=> BAI gi Y gi X <=> X BAI le nu Y

The other, spelled out in CLL 10.16, is used for TENSE, which are PU, ZI, FAhA, VA, or ZAhO. In all of those cases:

Y .i TENSE bo X <=> TENSE gi X gi Y <=> X TENSE le nu Y

I think that, in both cases, the final form {X do'e le nu Y} is most primitive. This implies that {le nu} or similar is primitive.

But also, CLL 10.17 uses {.i ... bo} to glue logical connectives to BAI and TENSE, with e.g. {.ibabo} akin to {.ijebo}. So, uh?

Story Time

Conversationally, Lojban bridi refer to events. The story-time convention connects those events spatiotemporally. The utterance {broda .i brode} implies something like {lo nu broda ku purci lo nu brode}.

BAI Modals

The BAI must be irregular overall; there's no single consistent pattern to them. But perhaps there's some families of behavior.

Column deletion can't work like with normal places. Suppose we have {broda bai zi'o}; then we have no choice but to imagine it {broda} in its rows. But does that imply that {broda} normally carries a {bai zo'e} after it? Hopefully not! We need another part of our zo'e convention to handle this.

Compounding the difficulty, some standard places are identified using BAI. For example, tavla4 is effectively {bau}. How do we unify these places correctly while minimizing irregularity?

I think that there can't be general semantics for {fi'o}. la xorxes' definition merely says that somehow it adjoins one selbri onto another, without regard for the implicit unification that happens in non-trivial examples.

Specifying selected BAI

ckaji

A nice warmup to understand what we're about to do.

ro da zo'u:

  da broda
------------ (kai-intro)
broda kai da

     broda sekai da
======================= (sekai-intel)
lo nu broda ku ckaji da

I am confused and frightened. I am not really enjoying this. But okay.

ckini

Similarly,

ro da ro de zo'u:

da broda de
-------------
broda ki'i da

...Hm. I think that this is all wrong. The pattern had looked good before, but now we're dropping data. That's no good.

dunli

ro da ro de zo'u:

 da broda de
-------------
broda du'i da

What's even going on.

Classes of gismu

Many gismu are related to each other in the sense that they address representatives of an open class: they all belong to a set, and there may be additional members of the set not yet known. We will consider open classes which are exhaustively enumerated from the baseline, but open to experimental gismu; this allows us to confidently categorize the baseline while allowing extension from the community.

Classes of n-ary relations are slightly more complex, and instead of a parametric presentation, we will use a schematic presentation. A class schema is a diagram textually represented as multiple lines of the following form:

broda*k*: brode*l*

Asserting that every element of the k-th place of {broda} is an element of the l-th place of {brode}:

ro da poi fa*k* broda zo'u: fa*l* brode

Or the following form:

broda*k*: *x*s

Asserting that there is an open class x which contains every element of the k-th place of {broda}. Note that this second form is not formalizable, but semantic; it indicates when an open class is primitive with regard to Lojban's semantic space.

Anatomy

In sufficiently complex multicellular life, some structures are discernable and categorized by function. I'm not going to write a paragraph on each one.

rango

These are all rango1.

• besna: brain
• betfu: abdomen, belly, lower trunk, midsection
• bongu: bone, ivory
• calku: shell
• canti: guts, entrails, intestines, viscera, innards, digestive system
• ciblu: blood
• cidni: knee, elbow, knuckle, hinged joint
• cnebo: neck
• cutne: chest, thorax, upper trunk
• degji: finger, digit, toe
• fepri: lung
• flira: face
• galxe: throat, gullet
• jamfu: foot
• kanla: eye
• kerfa: hair, fur
• kerlo: ear
• livga: liver
• nalci: wing
• pimlu: feathers, plumage
• risna: heart
• stedu: head
• tamji: thumb, big toe
• tance: tongue
• tuple: limb
• xance: hand
• xedja: jaw

Misc

• skapi: pelt, leather

Biology

Classes

clade1: specimens
clade2: species

grute2: clade2

A clade is a monophyletic rooted tree; the root is known as the most recent common ancestor. Note that not all collections of animals or plants form clades, and also note that horizontal gene transfer does not invalidate membership within a clade.

Some non-animal non-plants, particularly viruses and bacteria, can also form clades.

Issues

It's not clear whether cladistics are required relationally. In terms of implication, {tricu} is a subrelation of {spati} but trees don't form a clade. Also, e.g. {ckunu} is arguably a subrelation of {tricu}, depending on whether all conifers are trees; all conifers are woody, which may suffice.

Animals

Animal clades are nested according to the za'a diagram.

Fungi

• clika: moss
• gumri [archaic]: mushroom
• mledi: mold, fungus, mushroom, truffle

For archaic words, see here.

Plants

Species

Clades

• bambu: [exp] bamboo, Bambuseae
• cindu: oak
• ckunu: conifer, pine, fir
• lelxe: [exp] lily, Lilium
• marna: Cannabis
• nimre: Citrus
• poplu: [exp] poplar, aspen, cottonwood, Populus
• rozgu: rose
• sluni: onions, scallions, Allium
• srasu: grasses
• tujli: tulip
• xruba: buckwheat, rhubarb, sorrel grass, Polygonaceae

Non-cladistic Families

• kobli: lettuce, cabbage
• latna: lotus
• palma: [exp] palm tree, Palmae, Arecaceae

Fruits

• badna: banana, plantain
• figre: fig
• guzme: melon, squash
• perli: pear
• plise: apple
• smela: [exp] plum, peach, cherry, apricot, almond, sloe, Prunus
• tamca: tomato

Leaves

• tanko: tobacco

Roots/Bulbs

• patlu: potato
• samcu: cassava, taro, manioc, tapioca, yam
• sunga: garlic

Seeds/Grains

• bavmi: barley
• cunmi: millet
• mavji: oats
• maxri: wheat
• mraji: rye
• rismi: rice
• sodbe: soya
• sorgu: sorghum
• zumri: maize, corn

Related Words

• grute: fruit

• tsiju: seed

• dembi: seeds of bean, pea, legume

• pezli: leaf

• xrula: flower, blossom, bloom

• narge: nut

• genja: root

• tricu: tree

• jbari: berry

• fusra: rot, decay, fermentation

• birje: beer, ale

• jikru: liquor, spirits

• vanju: wine

• xalka: alcohol

• cakla: chocolate, cocoa

• ckafi: brewed coffee

• tcati: brewed tea

• stagi: edible plant, vegetable

• korki: cork, harvested tree bark

• gurni: grain, cereal

• mudri: wood, lumber

• jalna: starch

• fibra: [exp] fiber

Issues

{kobli} refers to both lettuce (Lactuca, milky sweet, also asparagus and chickory) and cabbage (Brassica, alkaline savory, also broccoli and many more). This is probably a mistake; the gloss conflates them as "leafy vegetables" despite many cultivars (asparagus, broccolini, etc.) which are not especially leafy. Similar issues plague {guzme}.

{latna} refers to Lotus, Nymphaea, and Nelumbo. Probably Nymphaea, because the definition emphasizes religious use within particular cultures. This is curious because {marna} doesn't have the same places, and only refers to Cannabis specifically.

Some cultures pair roses and lilies symbolically. For that reason, {lelxe} was proposed to complement {rozgu}. I have nothing against this one, and am tempted to include it as a nod to la lelxe.

{smela} is the sort of gismu that I want to fix while it's still experimental. Right now it refers exclusively to the fruits of Prunus, rather than the trees; it should be more flexible, like {nimre}. {plise} and {perli} are similarly weird and possibly worth fixing. However, it might not be feasible to fix them and instead we will need a class for fruiting plants.

What is {jbari}? Are all {guzme} also {jbari}?

It is not clear whether {gurni} refers to processed products only. Presumably the unprocessed kernels are {tsiju} instead.

Colors

Colors are described by the following class schema:

skari1: physical objects
skari2: colors
skari3: photoreceptors
skari4: physical environments

xinmo2: skari2

A color is a ratio of red, green, and blue. Exact ratios are yet to be decided, but there is a good survey of colors for future folks to incorporate. Extensionally, colors are the sets of all physical objects which can appear to have that color; using {blabi} as an example:

da blabi <=> su'o de su'o di zo'u: da skari pa ka ce'u blabi kei de di

Note that as a result, {skari} implies {ckaji}, and vice versa when {ckaji2} is a color:

da skari de di da4 => da ckaji de

The baseline contains the following colors:

• blabi: white
• blanu: blue
• bunre: brown, tan
• cicna: cyan, turquoise, green-blue
• crino: green, verdant
• grusi: grey
• labyxu'e: rose
• narju: orange
• nukni: magenta, fuchsia, purple-red
• pelxu: yellow, gold
• xekri: black
• xunblabi: pink
• xunre: red, crimson, ruddy
• zirpu: purple, violet

The physical environments include nothing at all (blackbody radiation), electric fields (fluorescence), temperature (incandescence), etc.

Related words

• kandi
• carmi
• xinmo

Elemental Chemistry

Here, we will explain chemistry in terms of elements and molecules.

Class of Elements

The following schema organizes elemental atoms and molecules:

ratni1: atoms
ratni2: atomic numbers (number of protons)
ratni3: mass numbers (number of nucleons)

rakle1: atomic numbers (number of protons)
rakle2: groups
rakle3: periods (number of full electron shells)

groups1: atoms
groups2: ???

xukmi1: physical objects
xukmi2: molecules
xukmi3: purities (0, 1]

Note that ratni3 is always at least ratni2.

Note that {rakle} has two more places which we are ignoring; rakle4 is a shadow of rakle2, and rakle5 is fixed by the Standard Model.

Groups should probably be indexed by natural numbers. Currently, there are experimental lujvo for individual elements within a group, but those would only be useful as indirect labels.

Note that membership in {xukmi} is inherently fuzzy, with xukmi3 as the fuzziness. Also note that 100% purity is physically unlikely but legal for textbook examples.

One open question is how atoms form molecules. Something with the structure:

x1 (molecule) has underlying graph x2 (graph) where x3 (atom) is assigned to vertex x4

For now, we suggest a sharp barrier between atoms and molecules.

One open question is whether molecules in dynamic equilibrium are always present, probabalistically present, or conditionally present; we assume the former. For example, in the equilibrium reaction for water:

2 H₂O <=> H₃O⁺ + HO⁻

Do we say that DI water is 100% H₂O? 50% HO⁻? Does it have more exotic species? Perhaps it depends on laboratory conditions. In this particular case, there is a solid argument that water is H₂O by default, because it only self-ionizes about once per 10 hours (per pair of molecules) and self-neutralizes about 1 picosecond later, yielding an average purity of 15-16 nines.

Molecule gismu are extensionally identified with sets of physical objects composed of those molecules. This includes gismu which cover multiple molecules, as noted below.

Note that the logic of chemical reactions, stoichiometry, is a linear logic which is not generated from the posetal logic of Selb or the deductive logic of Loj. Instead, given any family of stoichiometric equations which holds parametrically over a relation of elements, Selb has a posetal logic generated by its subrelations. For example, all halogens have hydrogen halides; for halogen x, there are environmental conditions where the stoichiometric equation holds:

H₂ + x₂ => 2 Hx

The corresponding posetal logic is generated by subrelations of {kliru}.

Groups of Chemical Elements

These gismu refer to entire columns of the periodic table.

• sodna: group 1, sodas, alkali metals; lithium, sodium, potassium, rubidium, caesium, francium
• kliru: halogens; fluorine, chlorine, bromine, iodine, astatine, tennessine
• navni: noble gasses; helium, neon, argon, krypton, xenon, radon, oganesson

Hydrogen should also get {cidro}, perhaps? It ought to get its own group, as too many stoichiometric families of group 1 metals exclude it.

Elements

These gismu refer to elements.

• cnisa: lead
• margu: mercury
• nikle: nickel
• rijno: silver
• solji: gold
• sliri: sulfur
• tinci: tin
• tirse: iron
• tunka: copper
• zinki: zinc

These gismu are ambiguous about whether they refer to atoms or molecules.

• kijno: oxygen, ozone
• tabno: carbon; graphite, diamond, charcoal
• trano: nitrogen; ammonia, nitrates

Elemental/Molecular Families

• djacu: water (H₂O)

Alloys

• gasta: steel (iron, carbon)
• lastu: brass (copper, zinc)
• ransu: bronze (copper, tin)

States of Matter

• litki: liquid

• gapci: gas

• jinme: metal

• bisli: ice, crystal

• sligu: solid

• dunja: freeze, gel, solidify

Composite Substances

• kolme: coal, peat, anthracite, bitumen
• tarla: tar, asphalt
• kunra: ore
• romge: polished metal surface
• bakri: chalk

Chemical Reactions

• slami: acid
• jilka: alkaline

Other valsi

• runta: solute in solvent
• pulce: precipitate
• curve: pure, unadulterated, unmitigated, simple

Perhaps {curve lo tabno} "pure carbon", for example.

Oxidizers

{fagri}'s third place takes an "oxidizer." This could be oxygen, air, hydrogen peroxide, or something else.

Families

Structures

• lanzu

lanzu1 is a set, not a mass. The baseline definition of lazmi'u makes this clear; it uses cmima. So:

da lanzu de di => de cmima da

lanzu3 is not clear. We will explore several standard biological concepts of family, but we are aware of the immensely polysemous and metaphorical weight placed on "family" by English.

Binary gender

• bersa: son
• bruna: brother
• mamta: mother
• mensi: sister
• patfu: father
• tixnu: daughter

Other words

Perhaps fetsi and nakni can be defined in terms of taking on various binary gender roles, since mamta/patfu need not be biological.

Non-binary gender

• dzena: elder, ancestor
• famti: aunt/uncle
• panzi: offspring
• rirni: parent
• rorci: procreation
• tamne: cousin
• tunba: sibling

Issues

Is rorci symmetric in x1 and x3? Can it be generalized in practice, x4, x5, etc. for multi-parent sexual reproduction?

Geometry

Abstracta

• {canlu}: x1 is 3+D space contaning x2
• {diklo}: x1 is within a ball centered at x2 and with radius x3
• {jganu}: x1 is the angle with corner vertex x2 and subtending line/curve x3
• {kubli}: x1 is a polytope with dimensionality x2 and surface/sides x3
• {kurfa}: x1 is a shape with all right angles, defined by corners x2 (set), with dimensionality x3
• {linji}: x1 is a line containing points x2 (set)
• {mokca}: x1 is a point in space x2
• {plita}: x1 is a 2D plane defined by points x2 (set)
• {sefta}: x1 is a face of object x2, side x3, edges x4

Issues

diklo3 should be a "range", not a radius; but I can't find good examples of usage.

kubli2 defaults to 3 and kubli3 defaults to 6, so kubli defaults to 3D cubes.

kurfa3 defaults to 2, so kurfa designates rectangles by default.

mokca2 is "in/on/at time/place", which seems polysemous.

linji2 cardinality is at least 1, but plita2 cardinality is at least 3. This is because plita1 is fixed by plita2; linji1 is "a line", but plita2 is "the plane".

Physical

• {bliku}: x1 is a 3D rectangular prism (cuboid) of material x2
• {bolci}: x1 is a sphere of material x2
• {boxfo}: x1 is a 2D plane flexible/crumpled in 3D of material x2
• {cukla}: x1 is a 2D disk/ring
• {djine}: x1 is a 2D annulus of material x2, inner diameter x3, outer diameter x4
• {jipno}: x1 is a 0D point on object x2 at locus x3
• {karda}: x1 is a thin 3D object of material x2 approximating 2D shape x3
• {kojna}: x1 is a 3+D corner with interior angle on object x2 of material x3
• {konju}: x1 is a cone of material x2 with apex point x3
• {tanbo}: x1 is a 3D long flat rectangle of material x2
• {tapla}: x1 is a 3D prism of material x2, extruded 2D shape x3, and thickness x4 in the third dimension

Implications

{tanbo} is a subrelation of {bliku}, ignoring bliku3.

{karda} is a subrelation of {tapla} as tapla4 shrinks towards zero.

Issues

bliku3 is supposed to enumerate the "number, size, and shape" of the "sides/surfaces" of the cuboid.

bolci has unclear dimensionality.

cukla is very generic, and conflates disks (filled-in) with rings (hollow boundaries), although notes say that it's "normally used for a filled-in circle/disk."

djine3 and djine4 are diameters, not radii.

SI Units

• delno: candela
• mitre: meter
• snidu: second
• kilga [exp]: kilogram
• xampo: ampere
• kelvo: kelvin
• molro: moles

General form is "x1 is x2 $UNITs in length (default 1) by standard x3".

Derived units:

• grake: grams
• mentu: minutes
• cacra: hours
• paska [exp]: pascal

Issues

mitre has weird structure: "x1 is x2 meters in length (default 1) measured in direction x3 by standard x4".

We need to be able to multiply and divide units. It would be enough to have some sort of tensor-product operation on selbri; e.g. {paska} needs to be in kg/m/s².

Sets, not Masses

This work uses sets, not masses.

Why sets? Sets are free over a universe of individuals. While they may not have the ultimate expressive power, they are therefore an inevitable structure which can be used for logic. The other free gadgets are vector spaces, and we leave that treatment for future work.

Why not masses? Masses can be expressed using plural logic; see la guskant for a complete foundation, including metaphysics. However, plural logic is equiconsistent with monadic second-order logic, given a predicate for masses. Since we treat the full semantics of second-order logic, we see a commitment to masses as simultaneously vague and limiting. That said, there are important use cases to address, and I propose discursive logic as a way to build a form of plural logic on top of standard set-theoretic foundations. I also give the axioms for mereology, using {pagbu} as the main predicate.

Non-first-order-izability (NFO)

One of the curious phenomena of second-order logic is that some sentences cannot be translated from second-order to first-order logic, even when both logics agree about set theory. In a certain sense, second-order logic is more expressive than first-order logic, and also more abstractive. Specifically, it is more Felleisen-expressive and Shutt-abstractive.

Identity

As a classic and powerful first example, we can give a redefinition of {du} in NFOL terms.

ro da ro de zo'u:

         da du de
========================== (id-def)
ro bu'a zo'u da .o de bu'a

This rule is a second-order definition; such rules are not possible within first-order logic. There are many reasons to justify this sort of explanation as a definition, but the primary reason is that they could be entered into Lojban dictionaries. For example, we could define {du} as:

ro bu'a zo'u x₁ .o x₂ bu'a

And give any tautology, like (id-refl), as an example:

ro da zo'u da du da

Once so defined, {du} is technically not in terms of any particular selbri; rather, it is a global property of all selbri!

Natural numbers

We can give the induction principle for natural numbers with SO quantifiers.

ro bu'a zo'u:

ge li no bu'a gi ro da su'o de zo'u da na.a de bu'a .ije da kacli'e de
---------------------------------------------------------------------- (kacna'u-ind)
                  ro da zo'u da kacna'u nagi'a bu'a

Nonce valsi

Some valsi used in this work do not appear elsewhere in Lojbanistan; they were purpose-crafted.

Overlap and Underlap

In mereology, the concepts of overlap and underlap are built from parthood. We could choose to use {pagbrjonlapi} and {pagbrkuclapi} for this, but instead we introduce the shorter lujvo {jompau} (from {jo'e pagbu}) and {kuzypau} (from {ku'a pagbu}) for brevity and ease of pronounciation. These lujvo are not jvajvo, because they have components from JOI. They have a simplified place structure which only uses the first two places, in line with standard formal mereology:

jompau:
x1 and x2 underlap

kuzypau:
x1 and x2 overlap

Lattice of Relations

To express bicategorical relational logic, we need gismu which are similar to {nibli} in structure. {nibli} only operates on {du'u}, though, and we would like to operate more directly on {ka} selbri. To facilitate this, we take -ki'i- from {ckini} and use it as a modifier, forming {ki'irni'i}, {ki'irvlina}, and {ki'irkanxe} with the following place structures:

ki'irni'i:
x1 (binary ka) lattice-implies x2 (binary ka)

ki'irvlina:
x1 (binary ka) is the lattice-join/supremum of x2 (binary ka) and x3 (binary ka)

ki'irkanxe:
x1 (binary ka) is the lattice-meet/infimum of x2 (binary ka) and x3 (binary ka)

These lujvo are not jvajvo, and a jvajvo approach probably isn't possible given the baseline alone, since {du'u} are like nullary {ka} and {ka} of different arity aren't interchangeable.

Metavariables

In Lojban

Lojban has metavariables for various semantic objects:

• sumti: {ko'a}, {fo'a}, etc.
• selbri: {broda}, etc.

Lojban also has quantified bound variables:

• first-order: {da}, etc.
• second-order: {bu'a}, etc.

In Metamath

Metamath cannot substitute a grammar production without designated metavariables. Thus, we have embraced many experimental cmavo in order to make our logic more flexible, and restricted semantic metavariables to serve as specific portions of syntax.

The current mapping is as follows:

• sumti: {ko'a}, etc.
• selbri: {bu'a}, etc.
• brirebla: {bo'a}, etc.
• bridi: {broda}, etc.
• numbers: {ku'i'a}, etc.

Loj

Loj is a category formed from Lojban syntax. Specifically, it is the poset (WP, nLab) whose:

• objects are equivalence classes of closed well-formed bridi, and
• arrows are implications from one bridi to another.

To read Metamath theorems as statements about Loj, encode:

• objects as members of the {broda} series
• arrows from X to Y as {ganai X gi Y}

Table of proofs

To Do

• Implication should form a partial order; we're missing antisymmetry
  • {ganai broda gi brode} & {ganai brode gi broda} => {pa du'u broda kei du pa du'u brode}
• Implication, conjunction, disjunction should form a lattice
  • Missing ge-ind: deductive form of ax-ge-in
  • And also a distributive lattice?
    • {ge broda gi ga brode gi brodi} => {ga ge broda gi brode gi brodi}
  • Easy implications of being a lattice:
    • Idempotence: {ge/ga broda gi broda} => {broda}
    • Commutativity: {ge/ga broda gi brode} => {ge/ga brode gi broda}
    • Associativity: {ge/ga broda gi ge/ga brode gi brodi} => {ge/ga ge/ga broda gi brode gi brodi}
    • Absorption: {ge/ga broda gi ga/ge broda gi brode} => {broda}

Relations and Selb

Selb is a locally posetal dagger-category formed from selbri. Specifically, it is the bicategory of relations over sumti, whose:

• objects are classes ("collections", "sets", "masses", etc.) of sumti
• arrows are selbri
• transformations are inclusions/subrelations between selbri

Summary

Here is a high-level summary of our analogy between logic and Lojban:

What is a relation?

Mathematically, a binary relation R : X -> Y between two collections of objects X and Y is a collection of ordered pairs of objects (x, y) in (X, Y). In most cases, it will be useful to imagine that the collections are sets, so that x and y are elements of sets X and Y respectively.

Please, pause for a moment and be sure that you understand the above paragraph. This is how all finite selbri behave. For example, {mlatu} addresses the collection of all cats and cat species, containing ordered pairs of cats and species.

Properties of relations

Okay, let's continue. Immediately, the most important feature is the reversibility of the relation; for every R : X -> Y there is an R† : Y -> X, called the dagger of R, which is the same relation but backwards. Where R has pairs like (x, y), R† has corresponding pairs (y, x). Note that R†† = R; swapping a pair twice is the same as not swapping it at all.

Another important feature is that we can ask whether a given pair (x, y) is in R, and this leads to the characteristic function for R, which returns the Boolean truth value, true or false, indicating whether the pair is in the relation. We'll write this characteristic as R(x, y). Not all relations have a characteristic; we'll say that a relation is decidable when it does. Decidable sets also have characteristic functions; these relate sets to their subsets. We cannot ask whether x is in X, but if we know that S is a subset of X and x is in X, then we can ask whether x is also in S.

We can also ask about how many pairs are in R, and we'll write this as |R| and call it the cardinality. We'll say that R is satisfiable when it has nonzero cardinality. Again, cardinality for sets is also defined; the cardinality of a set is the number of elements.

While binary relations are the most common kind, relations can come in any arity, and we might see unary relations (which are just subsets) or ternary relations or any arity.

Okay! Take a breath.

Relations in Lojban

Now, Lojbanically, every selbri has an underlying relation, and its sumti have underlying sets. When we write {da bu'a de}, we are indicating that the pair (da, de) is within some collection of pairs referenced by the relation bu'a : abu -> ebu. The intermediate Lojbanist will immediately recognize that {de se bu'a da} is the same utterance, but rearranged; {se} acts as a dagger operator. (XXX axiom reference here for sei!) Similarly, the selbri {jei da bu'a de} is syntax for the characteristic function; we are applying the selbri {bu'a} onto the pair (da, de) and seeing whether it is present in the relation. The selbri {ka ce'u bu'a ce'u} allows us to capture the selbri {bu'a} itself as a relation bu'a and range over many different pairs of values (ce'u, ce'u) which bu'a relates.

While I will try to keep this terminology straight, I may occasionally abuse words to say that some sumti are in a selbri, by which I mean that the referent objects of each sumti, taken as a tuple, belong to the relation referred to by the selbri.

Second-Order Logic

We're not quite done with our ontology. Sets can have things for elements, and so relations will have pairs of things as elements.

Are there restrictions on the range of relations? No. A relation like {mlatu} can range over anything whatsoever. To restore our normal expectations, we will define sets like mlatu1 in terms of mlatu : mlatu1 -> mlatu2; in la brismu, a cat is something which is related to its species.

For logicians: If we require {da} to always be restricted when introduced, then we'll end up with Henkin semantics, equivalent to many-sorted FOL; if we allow it to range freely, then we'll need full semantics, which is genuine SOL. We want SOL, so we will work without typed first-order variables.

Either way, {bu'a} really does range over all relations in the universe. Note that, metatheoretically, we may allow ourselves to be convinced of the existence of relations which aren't in the universe; this is just a standard effect of Gödel's Incompleteness, in that we expect to find a few unprovably-extant large objects lurking outside of our formal reach.

Once we agree to embrace SOL, then we can consider the NFO concepts, like identity as equality, graph connectivity, the Archimedean property, and Geach-Kaplan sentences.

Negation

Take a set. We may consider all of the things in the universe which aren't in that set; first, consider all of the things, then subtract our set. Except, for better or worse, it happens that we don't necessarily get a set back. Why not? Because the collection of all things in the universe doesn't appear to form a set from inside Lojban, thanks to Russell's paradox. As a result, we can't see that this operation defines a set, either.

So, if we want to use negation, then we will need another justification for it. The typical approach is to use the Law of Excluded Middle, a non-constructive axiom which insists that every bridi is either true or false. Recall that a characteristic function always returns true or false. Thus, the Law of Excluded Middle says that every selbri has a characteristic function. We can build negation from characteristic functions; the negation of a relation doesn't have a collection of pairs, but it can ask the original relation whether a pair is related, and then negate the response.

If we want it, then we must take it as an axiom as to whether the law of the excluded middle is available. It can't be derived as a theorem.

I'm going to not give the axiom, even though it appears in CLL. I'm also going to avoid CLL's version of De Morgan's laws and contraposition, as a result. Later, I'll note when the Axiom of Choice -- which implies the Law of Excluded Middle -- first appears. The bitter truth is that the law of excluded middle is an addition that we optionally use to collapse a rich open world of possibilities into a black-or-white closed world which has many blind spots.

Interpreting natural deduction

Each logic in natural deduction can be used to give judgements, like "P is true." Wikipedia lists "P is possibly true," "P is always true," "P is true at a given time," and "P is constructible from the given resources," as other examples in other logics. What does relational logic give us? Relational logic judgements are of the form "P is true at least once;" we can imagine that a bridi is not just true or false, but true for each of the many possible values that are being related, and that there may be multiple worlds which provide a context in which a statement is true.

Bibliography

This is an ad-hoc bibliography while I try to figure out how to make mdbook-bib cooperate.

• CLL or also here
• the BPFK Sections
• The proposed fourth tense in Lojban
• Relational Set Theory, Kawahara 2006
• Set theory for category theory, Shulman 2008
• Rethinking Set Theory, Leinster 2012
• Five Stages of Accepting Constructive Mathematics, Bauer 2016
• Knowledge Representation in Bicategories of Relations, Patterson 2017

Informal Lojban

Some parts of Lojban are forever unformalizable with the current structure of la brismu. By formalizing the syntax, we embrace all of the responsibility of parsing, and Lojban is known to be difficult to parse. Thus, we readily concede that some valsi will not be defined in this current project.

This listing comes from the Lojban wiki article, "magic words in Lojban".

Magic valsi

Additional Posets

danlu

The following baseline gismu are related by {ki'irni'i}.

Definitional Dependencies

The following selbri can all be defined in terms of each other; one selbri points to another when it can be defined in terms of that selbri.

Size issues

What are things? What are we talking about? We have a (Grothendieck) universe filled with many things. What does that mean? Some of the things are sets. Sets may have elements, which are also things. Any two things can be put into a set which contains just the both of those things. Given any set, we can also have its power set, which is just the set of its subsets. And finally, given any set of sets, we can take its union.

This is enough to be able to talk about most sorts of infinite objects that the layperson might dream up. We have enough sets for not just every particle in the observable natural universe, but every natural number, and indeed we can have the set of natural numbers, a set of real numbers, etc. We can also have some objects that are much larger than these "small" sets, such as a category whose objects and hom-sets are small sets and functions. Such a category can still be made out of sets, and so it would just be another thing; indeed, because of this, it would be the category of sets and functions, Set. We also have working Yoneda, with presheaves taken over small functors rather than all functors.

Formally, we're going to do all of this by assuming some nice 4-category, choosing a free 3-category which will let us do our setup, explicitly designating a 2-category as our topos using ETCC, fixing some inaccessible cardinal K, fixing some Grothendieck universe U=V_K, and then setting up second-order logic inside U and walling ourselves in. We cannot access K or U directly, let alone any of the higher-order categorical structure, but we don't really need to, either; we can quantify over all of U's things, and that is enough.

For the future: We still can access most n-categorical tooling, as long as we're gentle and only work with diagrams. In particular, we can still have opetopes of any finite order; I'm not sure if suspended opetopes are available, but probably.

Consider the following theorem:

ro da zo'u da du da

In the framing we've introduced, this is read as, "for all things X in the universe, X=X". But, since {du} must be a small relation, a more careful reading is, "for all small things X in the universe, X=X". A casual reader might think that this is trivial or that we are not talking about objects of consequence, but for example, the set of all natural numbers is a small thing, as is any set of real numbers, or the category FinSet whose arrows are total functions on finite sets.

Frequently Asked Questions

Where can I learn Lojban?

The following tutorials are all adequate:

• la karda
• the Crash Course
• the Wave Lessons

Why not just add new words?

Often times, folks ask why I can't just add words for the correct mathematical objects to Lojban, and then work solely in those words. This doesn't help clarify the rules surrounding already-established logic!

I've added new words where there's really no other option, and I've clearly indicated that I don't want to recommend my words when there are community-supported alternatives already.

Why are you doing this?

The main reason is that any logical language ought to have its logic clearly documented and explained. I'll help do this for Toaq and Xorban and others, but only once folks start to grok what I'm explaining about Lojban, which is the best-understood loglang.

What was so lacking about CLL? Aren't the BPFK reforms sufficient?

CLL doesn't directly explain the underlying axioms. BPFK gave some axioms, but they are sometimes incomplete and sometimes inconsistent. Both CLL and the BPFK sections are cited as sources in the bibliography.

Why don't you work with LFK?

No LFK members have indicated an interest in pursuing this work. They did provide many fruitful conversations about logic and Lojban lore.

Can't I just learn logic by learning Lojban?

That has not worked in the past, and it probably won't start working now. I recommend studying a basic introduction to first-order predicate logic in your native language, and then hopefully an introduction to relational algebra. For English-speakers, I recommend Peter Smith's An Introduction to Gödel's Theorems, the "Gödel book," which covers every relevant feature of first-order logic and also several tangents which are relevant to formalization.

Isn't this futile, since words can change in meaning?

Many Lojbanists have encountered the following collection of themes in philosophical discussion:

• "Lojban is not a relex": Aside from Lojban itself being forked from Loglan, Lojban is not merely a borrowing of semantics precisely established and defined in some natural language.
• Limited words can still blanket semantic space by being vague. We can use tanru to carefully describe observed objects in only certain ways, without committing to imprecision or incorrectness.
• The grue/bleen problem prevents us from fixing any absolute meaning to any word over time.

However, rather than give each word a meaning on its own, we use categorical logic and reasoning to build up structural meanings for Lojban. We don't merely attach meanings to individual words, but relate those words to each other, creating non-trivial theorems.