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 has multiple pieces:

• a formally-verified collection of proofs about Lojban syntax written mostly in Metamath, a system for formalizing symbolic logic and proving theorems
• a pile of mostly-English notes and prose, organized loosely into chapters, which informs that formal system's axioms and grammar
• formal definitions of categories Loj and Selb which are suitable for foundational and high-level logical reasoning
• a vlaste which logically defines valsi in terms of other valsi

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; the purpose of this book would then be to show that a Lojban-style project can be rigorously formal.

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 gadri (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
• la latros

Praise from Lojbanists

"alien language" -- la gleki

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

"no one cares about formalism" -- la xaspeljba

Introduction to Logic

In our daily lives, we are often told to be logical. However, it is rare for us to be told what logic is. As a result, many of us stumble through life with a vague sense of syllogism without formality.

Syllogisms

A syllogism (WP, nLab) is a foundational form of deductive proof. It operates according to the following schema:

1. If P, then Q.
2. If Q, then S.
3. Therefore: If P, then S.

Here P, Q, and S are statements made out of words. This is the first principle of logic: we are oriented around words and rules which manipulate them, not the meanings of the words. As logicians, we recognize that natural usage of language does not always respect logical rules, which means that we cannot let P, Q, or S be arbitrary statements; instead, they must be constructed according to logical rules. We will revisit this later, but first let us consider syllogisms in Lojban, which have the following schema:

1. {ganai broda gi brode}
2. {ganai brode gi brodi}
3. Therefore: {ganai broda gi brodi}

For now, the logical rules are easy to state: broda, brode, and brodi must be grammatical bridi with valsi drawn from a basis set. The basis set contains valsi like {ganai} and {gi} which are necessary to state the logical rules themselves; if we didn't choose a basis, then we wouldn't be able to define our logic! However, the basis set will not contain discursive connectives, so it may seem like a restricted way of using Lojban at first. We will see later how to define new valsi in terms of the basis set.

modus ponens

Modus ponens (WP, nLab) is the most common name for the following schema:

1. Suppose: P.
2. If P, then Q.
3. Therefore: Q.

To be direct with the reader: "modus ponens" or "MP" is one of those few names that you must memorize in order to read English prose about logic; it occurs too frequently in Anglophone literature and is too fundamental to not be understood by readers. I apologize and wish it had a better common name.

In Lojban, there are several schema we might consider. Here is one classic schema:

1. Suppose: {broda}
2. {lo du'u broda cu nibli lo du'u brode}
3. Therefore: {brode}

We will eventually build variations on this, but it turns out to be untenable for deep reasons. Instead, the schema used throughout la brismu is:

1. Suppose: {broda}
2. {ganai broda gi brode}
3. Therefore: {brode}

Compare and contrast with the fully-formalized axiom statement, ax-mp. This schema is compatible with the syllogism schema. Both schemata have a bridi of the form {ganai broda gi brode}. Considering this more deeply leads to…

Categorical logic

Categorical logic (WP, nLab) is a way of studying logic by studying the properties of structures generated by systems with modus ponens, like the "if"/"then" of English or {ganai}/{gi} of Lojban. This lets us study the ontology of a logic (what a logic can construct) without doing metaphysics (what a logic thinks is real.)

To gently introduce the concept, we can arrange our structure as a graph. For here, a graph is

• a set of abstract objects, known as vertices, along with
• a set of connectors between objects, known as edges, such that
• each edge connects from one vertex to another vertex, and
• every vertex has an edge which connects it to itself.

Assign a vertex to each bridi. A path in a graph is a sequence of edges with each edge following the other. In our running example, a path from {broda} to {brodi} might consist of two edges, one from {broda} to {brode} and another from {brode} to {brodi}. We'll let {ganai broda gi brode} represent a path from the {broda} vertex to the {brode} vertex. An application of modus ponens to a path is merely a traversal along the path. A syllogism is a composition of paths; path (1) ends where path (2) begins, constructing path (3).

At this point, the reader is encouraged to let this concept settle. Categorical logic is important for understanding the overall direction of the database of theorems, for justifying some of our axioms, and for explaining the structure of Lojban in a mathematically satisfying fashion. It is not important for understanding individual portions of la brismu or carrying out the rules of logic. We will merely note that there is a category-theoretic justification to add {ge} to our basis set.

There are actually two structures worth studying here. One structure uses {ganai} and the other uses {go}. We may always weaken {go} to {ganai} in either direction; it is as if the edges of the graph for {go} are undirected, while the edges of the graph for {ganai} are directed. These structures are known as Loj and Core(Loj) respectively. The main reason to include {go} is…

Definitions

We don't want to add every valsi to the basis set. Ideally, we want to define some valsi in terms of others. Since this effectively extends the basis set with new valsi, it is known as extension by definitions. We will follow a sort of schema:

1. Suppose: {broda}
2. {go broda gi brode}
3. Therefore: {brode}

This is merely modus ponens for {go}, and indeed it is a theorem, bi. However, let us be more specific:

1. Suppose: {ko'a bu'a}
2. {go ko'a bu'a gi brode}
3. Therefore: {brode}

Then we might say that the unary selbri {bu'a} is defined in terms of {brode}. It is possible (and likely) for {ko'a} — which is really just a placeholder, or metasyntax, for some terbri — to appear in {brode}, but not required. The idea is that we may treat any occurrence of {bu'a} as equivalent to {brode} and vice versa, so if everything in {brode} is already defined in terms of the basis set, then {bu'a} is defined in terms of the basis set too.

Ironically, we cannot define {go} and {ge} fully in terms of themselves, and this is the best way to understand why they are in the basis set. However, once they are established, we can define {ga}, {gonai}, and many selbri.

Logical Connectives

We now tour the Metamath axioms and theorems.

Sentential Logic with SKI Combinator Calculus

The axioms begin with ax-mp and two other axioms which we call ax-k and ax-s. Here is how we phrase them in Metamath:

Where do these axioms come from? These are the rules of SKI combinator calculus (WP, nLab, esolangs), a combinatory logic with some nice properties. A combinator is an abstract operation which takes some objects and arranges them into an applicative tree. Those other objects are usually also combinators, and application is ax-mp, so a combinator is ultimately some sequence of applications of ax-k and ax-s.

What are the nice properties of SKI combinators? Well, first, note that K and S are both tautologies (WP, nLab): if we test whether each bridi is true or false, and write out a truth table, then both K and S are always true. They're also admissible in intuitionistic logic, which means that if we imagine each bridi to refer to (classes of) things, then we always obtain more (classes of) things as a result of applying them.

Note that we don't have the identity combinator as an axiom. That's because it can be proved as a theorem, id. This is a nice example of the last nice property of K and S: they are complete for combinatory logic, which means that any other combinator can be built from them. Because of the way we set up Metamath, we can also prove the syllogism form of modus ponens, syl, as its own theorem.

The Five Connectives

We need to set up the five logical connectives in a specific order:

1. {ganai}
2. {ge}
3. {go}
4. {ga}
5. {gonai}

This is a sort of bootstrapping process which allows us to define new valsi in terms of old valsi. In general, once this is set up, a definition will be a {go} bridi which uses the valsi being defined in its left-hand component but not its right-hand component. For example, here are two definitions from this section of the database:

However, we can't use that for the connectives themselves. We don't define {ganai} at all! It's part of the basis. We add the following axioms, as well as a suspicious pseudo-definition df-go, in order to achieve our bootstrap:

But once this is done, we can define our final two connectives:

Negation

It is convenient to define negation alongside {gonai}. We define experimental valsi {cei'i} and {gai'o} for vacuous truth and falsehood respectively, along with {naku} for negating entire bridi at once:

We also define two essential axioms of negation. ax-sdo defines self-defeating objects and ax-efq is the principle of explosion, also called ex falso quodlibet (WP, nLab).

And we also prove several classical tautologies:

Other Axioms

This section includes several axioms whose full potential is not yet unlocked, but whose inclusion couldn't be postponed to the discussion on non-logical connectives. There are axioms of first- and second-order universal quantification:

Non-Logical Connectives

This section is about set theory, which we will frame as the study of {cmima}. {cmima} is our first example of a non-logical connective; it is a way of assembling bridi which cannot be reduced to mere definitions and so cannot be defined purely as a relation between logically-defined bridi.

Traditionally, set theorists study elementhood, which we express with {cmima}. There is also the notion of subset, expressed in our database with the CLL-era irregular lujvo {gripau}, which is more amenable to structural study.

Elementhood

First, we mention elementhood, traditionally studied through a collection of axioms known as ZF (WP, nLab). ZF is often combined with an Axiom of Choice, which we will discuss later; the reader is advised to carefully note the distinction between "ZF" and "ZFC". We study two selbri, {cmima} and {zilcmi}, which represent inhabited sets and all sets respectively.

We present the following subset of ZF, containing Axioms of Empty Set, Pairing, and Union:

And also extensionally define a fair number of selbri in terms of {cmima}:

Subsets

Next, we consider subsets. By defining subsets in terms of elementhood, we can establish that the subset relation is reflexive and transitive.

Internal Homs

This section is also the earliest that we can define the first Lojban abstractor, {ka}, which relates a selbri to the various terbri which combine with it to form a complete bridi. This is essential for building the so-called internal homs (WP, nLab), which will allow us to treat selbri as terbri.

We use this to define many classic gismu. Here are some examples:

And we can combine those with {cmima} to define more gismu:

This section also includes a definition of {du'u}, which further internalizes logic by allowing us to treat bridi as terbri.

At this point we can explain the main issue with using abstractors as our basis: terbri cannot be manipulated as generic syntax. It's not obvious how to do manipulations with gismu like {nibli} which operate upon {du'u} abstractions. As such, we prefer {ka} abstraction over {du'u} abstraction when manipulating syntax. The situation is not dire, merely unclear and difficult; theorems like nibli-refl have been proven without any fancy techniques. But we will need some fancy techniques, like…

Proper Substitution

Manipulation of bridi is getting tiresome, so we introduce the first — and hopefully only — genuinely new metasyntax in all of la brismu: proper substitution. It is a fairly weak mechanism that only allows us to replace any first-order quantified variable, like {da}, but we may replace it with any grammatical {ko'a}. Theorems about proper substitution are extremely powerful but take effort to prove; our listing of them is currently fairly short.

Not-Free Quantification

We also include a quantifier not in baseline Lojban, {na'a'u}, which asserts that a quantified variable is irrelevant to the bridi over which it scopes. It is not a common feature of most logics, but is used in other Metamath databases to ease the implementation of proper substitution. A noteworthy theorem here is ceihi-nf, which demonstrates that {cei'i} really is a nullary relation in semantics and not merely an aesthetic choice of our syntax.

Natural Numbers

We will pay special attention to the definition of natural numbers because it will be our foundation for number theory. Our axioms are chosen based on second-order arithmetic, following Robinson's axioms for numberhood and Frege's axioms for cardinality.

Numberhood

Zero is a natural number. In fact, the natural numbers are zero and the successors.

Zero is not a successor. Combined with the above axioms, this constrains the natural numbers to a single tower of successors above zero.

While many results do not require it, we also have the Axiom of Successors, which states that the operator/function taking each natural number to its successor is injective.

Induction over natural numbers is definable in second-order logic.

Addition

Addition is given via standard axioms.

We have not proven many arithmetic results yet.

Multiplication

Multiplication is also given via standard axioms.

Ordering

The natural numbers are totally ordered. This order is not realized on its own, but defined recursively.

Cardinality

We also have some axioms of Fregean cardinality.

Mereology

Mereology (WP, nLab) is the study of parts and wholes. It is closely related to set theory, in the sense that subsets are parts of whole supersets, but is studied independently.

Axioms

We present System M, the simplest possible collection of mereological axioms. System M asserts that parthood is reflexive, antisymmetric, and transitive: a partial order. We augment System M with two additional axioms, the Axioms of Top and Bottom, which assert that the universal and null objects exist.

Note that {pagbu} is a primitive symbol and cannot be defined as an extension of the basis. However, given {pagbu}, we can extend the resulting basis with a few more definitions:

Bridge to Set Theory

While it is not currently part of the database, set theory can be seen as a special case of mereology:

ganai da gripau de gi da pagbu de

This axiom is only absent because no use case has been found for it so far. This parallels the development of set theory as a finer-grained and more powerful mereology which is able to not only distinguish parthood but also elementhood.

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.

Modals

Historically assigning any semantics to {fau} is difficult; what is the difference between this utterance:

broda fau lo nu brode

And this utterance:

broda .i lo nu brode ku fasnu

We cannot rely upon any open sumtcita to help, since {fasnu} is unary. Perhaps there is a discursive difference; perhaps the former utterance also implies some connection or relevance between the two bridi. To be clear, the latter utterance also has an implied connection, the "story-time convention", as manipulated with {ki}.

Signs: sinxa, la'e, lu'e, lu'i

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

Ellipsis: zo'e, co'e, do'e

An ellipsis represents a selbri or terbri which the speaker has not yet uttered. As such, they should be registered as discursive evidence, rather than given semantics like {zi'o}.

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? We should take the convention offered here.

{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

0: Endorelations

Endorelations are binary selbri which relate a set to itself.

Reflexivity

Examples

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

Examples

• {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

Examples

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.

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

Euclidean

Groups

gismu: dukni

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.

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

Notes

Arrows of Time

Some philosopher-physicists argue in favor of "entropic time": all arrows of time are generated from the second law of thermodynamics. Sean Carroll gives examples:

• Biology: individuals age
• Genetics: evolution occurs
• Psychology: memories are into the past
• Causality
• Electromagnetism: energy flows along paths

The argument is that they are all oriented along the same broken symmetry of low entropy as the universe's own physical entropy. As Nick Lucid puts it, "All will follow the gradient. The gradient is inevitable."

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

Clades

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; however, their treatment is not required for the baseline.

The following tables include PhyloCodes which have been registered at RegNum. A PhyloCode is a registered taxon denoting a clade for international biologists.

Exact Clades

The following cladistic assignments are sufficiently on-the-nose that we ought to define these selbri using the clades. In this sense, the precise definitions of these clades are given by scientific consensus among biologists rather than by some specific listing of genes or apomorphies.

The following inclusions definitionally follow:

Approximant Clades

The following cladistic assignments aren't tight; there may be members of the clade which aren't members of the species in the {fe} slot. Nonetheless we can still do a bit of pointless topology on them: whenever {bu'a} has exact clade X, {bu'e} has approximant clade Y, and Y is in X, then {bu'e} is included in {bu'a}.

The following inclusions definitionally follow:

Non-clastistic Animals

• curnu: worm, invertebrate
• danlu: animal
• finpe: fish
• jalra: cockroach, orthopteran, termite
• jukni: spider, arachnid, crustacean, lobster, crab
• spati: plant, herb, greenery

Non-clastistic Plants

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

Species

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.

{dembi} and {debyspa} are not great. It turns out that Leguminosae (PhyloCode 60) has very hard edges due to the way that legumes grow; their aggressive and reliable production is due to nitrogen-fixing behavior not found in other fabids. ("Fabid" just means "bean-like plant". Legumes have been farmed since prehistory for the nitrogen fixation, leading to lots of historical names.) So, if only we had a proper lujvo for legumes, we could assign it an exact clade.

Other Issues

What is {jmive}? The Anglophone approach is near-useless because the following objects are all-or-nothing on {jmive}:

• Galaxies
• Stars
• Biomes
• Forests
• Lithotrophs
• Viruses

So the Anglophone approach might be to give up and say that {jmive} is Earth-centric: life is "homeostatic arrangements of organic chemicals in thermal non-equilibrium," quoting la korvo.

la gleki points to the Russophone approach, in particular the axioms of B. M. Mednikov, and proposes the valsi {mednikovo} which indexes them. This approach includes the following characteristics of life:

• Homeostasis
• Organization
• Metabolism including an anabolic and catabolic component
• Growth
• Adaptation
• Response to stimuli
• Reproduction or autocatalysis

And of non-life:

• Cessation of brain function ({co'u})
• Divergence of homeostasis
• Cessation of metabolism

la gleki gives a translation from Russian to English of Mednikov's axioms:

"mednikovo li 5". x1 is the organism that shows repeatedly amplified changes in the body's genetic programs being subject to selection by environmental conditions (Charles Darwin axiom)

"mednikovo li 3": x1 is the organism showing its genetic program transferred through generations having random non-directional changes (successful only in given environment) as a result of various reasons (Charles Darwin axiom)

"mednikovo li 2": x1 is the organism that shows taking genes of its parents for forming its offspring (N.K. Koltsov axiom)

"mednikovo li 1": x1 is the organism that shows the unity of its phenotype and the program for its construction (genotype) inherited from its ancestors (Weissman axiom)

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

Cultures

There are many cultural gismu allocated. They are extremely divisive, partially because they aren't well-defined and partially because people have strong political opinions as well as emotional attachments to gismu.

There's also the concept adopted by some speakers that the cultural gismu are only usable as rafsi, which precludes a single canonical definition of the gismu without spoiling all of the relevant rafsi. These speakers use cultural gismu to decorate lujvo with cultural origin, a Lojbanic adaptation of a longstanding and widespread practice in many cultures.

That said, we acknowledge the main critiques of cultural gismu:

1. They unfairly privilege some cultures over others in the baseline.
2. They are not phonetically faithful to how members of some cultures refer to themselves.

As a result, we will not endorse any particular cultural gismu, nor insist that the baseline is correct, but give a path for adapting any set of cultural gismu to fit within a single unifying framework.

Classes

There should be a class for kulnu1:

culture1: events
culture2: observations

prenu1: people

kulnu1: cultures
kulnu2: prenu1

natmi1: nations
natmi2: kulnu2

rutni1: artifacts
rutni2: kulnu2

turni1: prenu1
turni2: prenu1

tutra1: territories
tutra2: turni1

jecta1: governments
jecta2: tutra1

gugde1: countries
gugde2: kulnu2
gugde3: tutra1

This defines a template for all of the cultural gismu, as well as {rutni}.

TODO: this implies xamgu1 are events! A longstanding puzzle solved!

It should include the cultural gismu. It should also be in the upcoming "multiverse" feature, using a multiverse, because the baseline definitions should be culturally neutral.

What's the difference between {jecta} and {se tutra}? {jecta} doesn't imply {turni}; a government is a sort of organized group of people (a {stura} perhaps?) which claim to be {turni}, but turni1 are the violence-monopolists who physically occupy and oppress their subjects.

However, {kulnu}'s definition requires kulnu2 to be plural masses. The English says, "culture is what is shared among people and is not an individual trait," but this is a misunderstanding of relational logic. Logically, {kulnu} relates a set of people -- a subset of all kulnu2 -- to individual cultures in a many-to-many relationship. So, we're going to politely say that the baseline definition is misleading, and allow both rutni2 and kulnu2 to be individuals.

This class also implies that cultures, e.g. {merko}, should be conjugated instead of filled directly by individual people. Instead of {mi merko}, perhaps we should say {mi jai merko} for short. Putting the above classes to work, we might formally say:

mi se kulnu pa ka merko

Axioms

We should be able to define {turni} with something like:

da turni de <=> su'o gy ty zo'u: ty tutra da gi'e te gugde de gy

Why is {rutni} here? Its definition specifies that rutni2 are kulnu2, from which we may claim the following axiom:

da rutni de => su'o di kulnu de

Perhaps kulnu2 => cecmu2?

Related words

• {cecmu}

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.

• spisa: piece, portion, lump, chunk, particle (substance)

Perhaps {spisa} => {pagbu}.

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

Spaces

• {nicfa}: x1 is displacement between vectors x2 and x3 in affine space 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".

nicfa4 and nicfa5 aren't useful to us here. I'm replacing nicfa4 and folks can put {la brismu} for nicfa5 to indicate that they're using our definition instead.

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.

Measurements & Units

We start with the open-class structure of {merli}:

sanji1: observers
sanji2: observables

sidbo1: abstractions of at least one open {ce'u}
sidbo2: anything
sidbo3: sanji1

merli1: sanji1
merli2: sanji2
merli3: numbers
merli4: sidbo1 of at least two open {ce'u}
merli5: intervals

The intended selbri for the abstractions are the mreselbri:

msb1: observables
msb2: numbers

The central connection between these gismu is given by:

{ko'a sanji ko'e} & {ko'a merli ko'e ko'i pa si'o ce'u bu'a ce'u kei}
=> {pa si'o ce'u bu'a ko'i kei sidbo ko'e ko'a}

The core idea is that we do science via epistemic measurements, where an observer interacts with an observable and quantifies the interaction on a scale. By doing this, the observer comes to have a belief about a property of the observable.

The consensus approach is that only mreselbri are allowed in measurements, and that they can only be combined according to the rules of a free Abelian group. In English, these are often called "units" and the rules for manipulating them are known as "dimensional analysis".

In the baseline, the general form of mreselbri is "x1 is x2 $UNITs in length (default 1) by standard x3". We're going to ignore x3 and occasionally x4 for now; we might revisit them when talking about frames of reference. We will also ignore that {mitre} has a bad x3.

Combining Units

Following this wiki page, dimensional multiplication can be done with {pi'ai}. For inverses, {fei'u} is available; for repeated dimensions, {te'ai} is available.

SI Units

There are seven "SI base units" which generate the Abelian group of units considered in the hard sciences:

There are also "SI derived units" which are merely certain elements of that group:

And particular derived units which are scalar multiples of other units:

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.

Examples

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}
• pasting diagrams as applications of ax-mp
• Isomorphisms from X to Y as {go X gi Y}

Note that while Loj is thin, its formal verification in Metamath is non-thin. This is not a serious issue.

Table of proofs

To Do

• 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:
    • 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}

Core

The core of a category is the groupoid which includes all of its isomorphisms. The core of Loj, written Core(Loj), is the groupoid whose:

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

To read Metamath theorems as statements about Core(Loj), encode:

• objects as members of the {broda} series
• arrows from X to Y as {go X gi Y}
• pasting diagrams as applications of bi

Table of proofs

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:

Formal Proofs

Via 1Lab

The 1Lab module Cat.Allegory.Base defines allegories and proves several of their properties. By proving its axioms, we show that Selb is an allegory relative to 1Lab's foundations (cubical type theory within homotopy type theory.) We translate as follows:

Note that hom-sets and types are both simplified to bridi. Also note that Metamath is uncurried and Agda is curried, so Agda arrows can be either conjunctive or deductive. We do not include the is-prop assumption because Metamath's deductive systems usually give non-thin categories. We aren't especially worried about h-levels, so this is not a serious issue.

We also reprove the following theorems:

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," "P is justifiably believable," "P is provable," 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 that provide a context where a statement is true.

Definitional vlaste

This is a vlaste: a dictionary of Lojban valsi. Unlike typical dictionaries, which define words by evoking the associative notions of other words, this vlaste only contains formal logical definitions which extend the underlying basis.

Definitions are given in dependency order: a definition will only use valsi which have already been introduced. For technical reasons, some transitive dependencies are omitted from this table; a complete diagram of the dependencies between definitions is included in an appendix.

Note the following brismu conventions:

• All definitions are schematic: free metavariables are universally quantified and may be substituted with any grammatical fragments whatsoever. Bound metavariables are bound existentially, universally, etc. as indicated.
• The default article for {ka} and {du'u} is {pa}, not {lo}, reflecting syntactic capture rather than semantic capture.
• {broda} and friends refer to filled-in bridi; {bu'a} and friends refer to selbri, potentially including brirebla.
• {ku'i'a} and friends are metavariables for the PA class of cmavo.

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
• 1Lab, the 1Lab development team 2021
• Arithmetic Without the Successor Axiom, Boucher 2006

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.