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

Axioms of Extension, Empty Set, Singleton, and Collection:

Name	Statement
ax-cmima-ext	ganai ro da zo'u da cmima ko'a .o ko'e gi ko'a du ko'e
ax-pamei-cmima	ganai ko'a pamei ko'e gi ko'e cmima ko'a
ax-cmima-nul	su'o da zo'u ro de zo'u naku de cmima da
ax-cmima-coll	na'a'u da zo'u broda ⇒ ganai ro de poi ke'a cmima ko'a ku'o zo'u su'o di zo'u broda gi su'o da zo'u ro de poi ke'a cmima ko'a ku'o zo'u su'o di poi ke'a cmima da ku'o zo'u broda

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 broda kei
df-nalti-kata	pa du'u naku 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.

ETCS

And now for something completely different. Consider the following ten axioms:

Composition of functions is monoidal; identity functions exist.
There is a set with exactly one element.
A function is determined by its effect on elements.
There is a set with no elements.
All Cartesian products exist.
For any two sets X and Y, there is a set of the functions X → Y.
For all X → Y and all elements in Y, the preimage is a set.
The subsets of any set X correspond to the functions X → 2.
There is a set of natural numbers.
Every surjection has a right inverse.

These are the axioms of ETCS, a theory as strong as ZFC for most purposes. It neatly decomposes; axiom 10 is Choice and axiom 9 is Infinity. To set up ETCS, we require the following syntax:

selbri	primitive concept
zilcmi	z1 (set)
fancu	f1 : f2 → f3 is a function defined by restricting f4 (ka) to f2 × f3
lutfancu	l1 (fancu) is the composite of l3 (fancu) followed by l2 (fancu)
dubyfancu	d1 : d2 → d2 is the unique identity function on d2 (zilcmi)

We'll later need:

selbri	primitive concept
fatfancu	f1 is an inverse of f2
zilfatfancu	f1 is/has an isomorphism
kazmydu'i	k1 (zilcmi) is isomorphic to k2 (zilcmi)
cmima	given/type annotation: c1 is an element of c2
gripau	g1 is a subset of g2
stepau	s1 is the powerset of s2

And:

cmavo be zo JOI	primitive concept
pi'u	Cartesian product
te'au	Exponential

Composition

Axiom 1 has several formal pieces. First, {zilcmi} and {fancu} are set up. Also, we have the following statements:

{lutfancu} has an l1 for each l2 and l3, provided that the types line up, whose relational rule is a composite of l2 and l3
Given any zilcmi1, there is {dubyfancu} with the appropriate types, whose relational rule is given by {du}
Define {fatfancu}

And lemmas:

{ko'a fatfancu ko'e} <=> {ko'e fatfancu ko'a}

That's the preamble. The axiom is:

{lutfancu} is associative
{lutfancu} has units given by {dubyfancu}

At a high level: sets and functions form a category.

After this, we should be able to prove:

{ko'a fatfancu ko'e} & {ko'a fatfancu ko'i} => {ko'e du ko'i}
Define {zilfatfancu}
{ko'a dubyfancu ko'e} => {ko'a fatfancu ko'a}
{ko'a lutfancu ko'e ko'i} & {ko'e zilfatfancu} & {ko'i zilfatfancu} => {ko'a zilfatfancu}
{ko'a kazmydu'i ko'a}
{ko'a kazmydu'i ko'e} => {ko'e kazmydu'i ko'a}
{ko'a kazmydu'i ko'e} & {ko'e kazmydu'i ko'i} => {ko'a kazmydu'i ko'i}

We can see how we will eventually justify defining {kazmydu'i} as {dunli fi lo ka kazmi}.

Terminal object

There exists a terminal set:

su'o da poi zilcmi zo'u: ro de poi zilcmi zo'u: pa di zo'u:
di fancu de da pa ka cei'i

Afterwards, we should be able to prove:

terminal sets are isomorphic
a stronger version: the terminal set is unique

At this point, we might want to create a new sort of definition for generalized-the and terminality. Then:

For any set, there is exactly one function to the terminal set (expanding axiom 2 with the unique terminal set)
Define {cmima} in terms of {fancu}
Define application?

Well-pointedness

If two functions are equal on all elements, then they are equal.

Then:

A set is terminal <=> that set has exactly one element

Initial object

There is an empty set:

su'o da poi zilcmi zo'u: naku ko'a cmima da

Products

We add syntax: for two sets {da} and {de}, {da pi'u de} is also a set, and there are projection functions:

ro da poi zilcmi zo'u: ro de poi zilcmi zo'u: su'o di zo'u:
di fancu da pi'u de da pa ka ce'u orne ce'u zi'o

ro da poi zilcmi zo'u: ro de poi zilcmi zo'u: su'o di zo'u:
di fancu da pi'u de de pa ka ce'u orne zi'o ce'u

The universal quantifiers here constitute axiom 4. Existence and uniqueness should follow. Afterwards, it should be possible to define pairs and diagonals, and then:

{da pi'u de kazmydu'i de pi'u da}
{da pi'u le pamei kazmydu'i da}
{pi'u} is associative

Function sets

Axiom 6, as given by Leinster, is almost too trivial to formalize: given sets {da} and {de}, {de te'au da} is a set too. However, it must come with, at least, an evaluation arrow:

ro da poi zilcmi zo'u: ro de poi zilcmi zo'u: su'o di zo'u:
di fancu de te'au da pi'u da de
   pa ka su'o da zo'u: su'o de zo'u:
   ge ce'u orne de da
   gi ce'u lutfancu de da

The wiring comes out fairly nicely. Note that we will need parentheses for JOI at some point. From here we should be able to prove that:

evaluation is unique
precomposition is unique
postcomposition is unique
{le pamei te'au da} <=> {le pamei}
{da te'au le pamei} <=> {da}

Fibers

At this point, we run out of notation to discuss families and fibers; we can write out everything longhand, but I'm not in the mood. Axiom 7:

All fibers exist.

We can then define injectivity, surjectivity, and bijectivity.

Subobject classifier

We have subsets, but that's not enough to state axiom 8:

A subset classifier exists.