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:

Name	Statement
df-nomei	naku zo'u ko'a cmima le nomei ku
df-ce	go ko'a cmima ko'e ce ko'i gi ga ko'a du ko'e gi ko'a du ko'i
df-johe	go ko'a cmima ko'e jo'e ko'i gi ko'a cmima ko'e .a ko'i

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

Name	Statement
df-zilcmi	go ko'a zilcmi gi ga ko'a du le nomei ku gi su'o da zo'u da cmima ko'a

Subsets

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

Name	Statement
gripau-refl	ko'a gripau ko'a
gripau-trans	ko'a gripau ko'e & ko'e gripau ko'i ⇒ ko'a gripau ko'i

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.

Note

Readers acquainted with category theory may find the terminology curious. Note that the internal hom in Loj is the trivial syntactic one over {ganai} and {ge}, with its curry witnessed by theorems cur and uncur. The internal hom described here is for the logic of selbri: Selb.

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

Name	Statement
df-ckaji	go ko'a ckaji pa ka ce'u bo'a kei gi ko'a bo'a
df-ckini	go ko'a ckini ko'e pa ka ce'u bu'a ce'u kei gi ko'a bu'a ko'e

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

Name	Statement
df-steci	go ko'a steci ko'e ko'i gi ge ko'e ckaji ko'a gi ko'e cmima ko'i
df-mupli	go ko'a mupli ko'e ko'i gi ge ko'a ckaji ko'e gi ko'a cmima ko'i
df-simxu	go ko'a simxu ko'e gi ro da zo'u ro de zo'u ganai da .e de cmima ko'a gi da ckini de ko'e
df-kampu	go ko'a kampu ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u da ckaji ko'a

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

Name	Statement
df-fatci	go pa du'u broda kei fatci gi broda
df-nibli	go pa du'u broda kei nibli pa du'u brode kei gi ganai broda gi brode
df-sigda	pa du'u ganai broda gi brode kei sigda pa du'u broda kei pa du'u brode kei
df-tsida	pa du'u go broda gi brode kei tsida pa du'u broda kei pa du'u brode kei
df-kanxe	pa du'u ge broda gi brode kei kanxe pa du'u broda kei pa du'u brode kei
df-vlina	pa du'u ga broda gi brode kei vlina pa du'u broda kei pa du'u brode kei
df-nalti-ana	pa du'u broda kei nalti pa du'u naku zo'u broda kei
df-nalti-kata	pa du'u naku zo'u broda kei nalti pa du'u broda kei

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.

Name	Statement
subid	go [ da / da ] broda gi broda

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.