5: Set Theory
At this point, we are ready to give the axioms for set theory. We will be using ZF.
Functions I: {fancu}, {pagyfancu}, {ficyfancu}, {gairfancu},
We won't get far without functions, so we'll ignore the lack of community
standard and start with {fancu}
. We'll preserve the original place
structure and sharpen the definition to, "f1 is a function with domain f2
(set) and range/codomain f3 (set) and underlying relation f4 (binary ka)."
Under this definition, functions have types, and all functions are merely
relations satisfying a functional property.
So, what's this functional property? There's actually a family of them, but
we'll start with the most general ones. We're going to take a selbri {broda}
and bend it around a little, to something like {de se broda da .ije broda di}
, composing it with itself, which gives a self-relation on a set. Now,
let's compare that self-relation to {da du di}
; this gives us our family of
functional properties.
The first property we'll build is univalence, sometimes
called the functional property: A relation R is univalent if R's dagger
composed with R lattice-implies the identity relation on R's codomain.
Consider, for example, {mlatu}
. If we take each cat species to its
collection of cats, and then take each resulting collection to all of the
species in each collection, then we arrive back at each individual species.
More generally, for binary relations:
zo'u:
pa ka ce'u .e ce'u broda de kei kairni'i pa ka ce'u du ce'u
============================================================= (pagyfancu-intel)
zi'o pagyfancu le'i broda le'i se broda pa ka ce'u broda ce'u
I'm not going to further use or define {le'i}
. What's going on here? For
lack of a better convention, f1 is the "name", or "handle", of the function;
this is not just a label, but the actual reference by which functions are
internally identified in the logic. The good news is that you should already
know roughly what this means if I say {lo pagyfancu}
; the bad news is that
we're still going to be irritatingly formal about the whole affair. A similar
deal applies to the sets in the function type; they are technically supposed
to be references to types, but we don't have quantification over types (yet?)
And why {pagyfancu}
? First, univalence only guarantees that we have partial
functions, not total
functions. So we have the definition, "f1 is a partial function with domain
f2, codomain f3=p2, underlying relation f4, but only covering subset p1 of the
codomain." There are two ways to get to total functions. First, we can
trivially transform between partial functions on some set S, and total
functions on S + 1. Accordingly:
ro da poi ke'a fancu zo'u:
da pagyfancu ko'a ko'e pa ka ce'uxino ce'uxipa bu'a
===================================================================================== (fancu-partial)
da fancu ko'a ko'e .onai le pamei pa ka ce'uxipa se bu'a ce'uxino gi'onai du tarci.bu
This rule was made larger by subscripts on the {ce'u}
so that I could ensure
that the arguments are in the right order. It's very bulky, and it adds an
extra coproduct. Instead, we can show that there's another functional
property, totality, which is sort of like a dual to univalence: A relation R
is total if R composed with its dagger is lattice-implied by the identity
relation. This is like doing a basic covering check to ensure that every value
in the domain is mapped to at least one thing in the codomain.
ro da poi ke'a pagyfancu le'i broda le'i se broda zo'u:
pa ka ce'u du ce'u kei kairni'i pa ka ce'u .e ce'u broda de
=========================================================== (fancu-intel)
da fancu le'i broda le'i se broda pa ka ce'u broda ce'u
So, for example, it is the case that {fancu le'i mlatu le'i se mlatu pa ka ce'u mlatu ce'u}
; this function has the same data as the relation (it is a
subset of the Cartesian product of cats and cat species) but we are now
carrying additional information which proves that it is functional.
We can examine equality of relations, carefully. We can't simply ask whether relations are equal, but we can both witness it syntactically and also logically. First, if two relations lattice-imply each other, then they're equivalent.
ro da poi bridi ke'a ku'o ro de poi bridi ke'a zo'u:
da kairni'i de .ije de kairni'i da
================================== (kairni'i-sym)
da du de
Now, if we don't just have lattice-implication in the univalence property, but
full inversion, so that R composed with its dagger is equivalent to the
identity relation, then R is an injection. The nonce lujvo {ficyfancu}
has
place structure, "f1, f2, f3, f4 as normal, and also for all x3 in f2, {x1
frica x2} => {f1(x1) frica f1(x2)}." As you can see, this definition got a
little rich, but injections are complicated.
ro da poi fancu ko'a ko'e zo'u:
da fancu ko'a ko'e de .ije de kairni'i pa ka ce'u du ce'u
========================================================= (ficyfancu-intel)
da ficyfancu ko'a ko'e de
Dually, surjections technically have more data but are specified in roughly
the same way, with R's dagger composed with R yielding the identity relation.
The nonce lujvo {gairfancu}
has place structure "function f1 has domain
f2=g1 covering codomain f3=g2 with the fact that for all x1 in f2, exists x2
in f3 with f1(x1) = x2."
Note that if f2 and f3 were proper sets, then {gacri}
could be defined as,
among other things, a covering set! This means that when we run
(gairfancu-intel)
in reverse, we are invoking the Axiom of Choice.
ro da poi fancu ko'a ko'e ku'o ro de poi bridi ke'a zo'u:
da fancu ko'a ko'e de .ije pa ka ce'u du ce'u kei kairni'i de
============================================================= (gairfancu-intel)
da gairfancu ko'a ko'e de
Finally, as a definition, a bijection is both an injection and surjection,
with nonce lujvo {mitfancu}
, "isomorphism f1 has domain f2=m1 and codomain
f3=m2, and in that direction, has witnessing relation f4=m3."
ro da poi fancu ko'a ko'e ku'o ro de poi bridi ke'a zo'u:
da ficyfancu je gairfancu ko'a ko'e de
====================================== (mitfancu-intel)
da mitfancu ko'a ko'e de
Injections are, more generally, monomorphisms. We give the universal property for monomorphisms in regular logic: if a monomorphism f sends two objects to the same value, then the objects are the same as well.
ro bu'a poi ficyfancu ko'a ko'e ke'a ku'o ro de ro di zo'u:
de mintu di pa ka ce'u bu'a ce'u
-------------------------------- (ficyfancu-mono)
de du di
Similarly, surjections are epimorphisms. Epimorphisms capture existential quantifiers.
ro bu'a poi gairfancu ko'a ko'e ke'a ku'o ro da zo'u:
su'o de zo'u de bu'a da (gairfancu-epi)
And bijections really are isomorphisms; we can turn them around arbitrarily, and a little work will show that in each every case where there's an isomorphism, we can use our standard dagger. Maybe that's provable with what we've got, but I'll just give it as an axiom:
ro da poi mitfancu ko'a ko'e zo'u da mitfancu ko'a ko'e pa ka ce'u bu'a ce'u
=============================================================================== (mitfancu-iso)
ro da poi mitfancu ko'e ko'a zo'u da mitfancu ko'a ko'e pa ka ce'u se bu'a ce'u
Subsets:
One of the two essential relations of set theory is {cmima}
, which relates
sets to their elements. Like in some flavors of ZF, in Lojban we cannot forget
to which set an element belongs.
Remember, we are using relational logic, and a single set is related to each
of its elements. {da cmima de}
is, for each particular {de}
, going to be
true once for each distinct {da}
.
The other essential relation of set theory is {steci}
, which relates sets to
their subsets using set
comprehension.
Interestingly, unlike most flavors of ZF, not only does Lojban preserve which
superset each subset belongs to, but also the unary {ka}
property which
built it. When we run with steci2 and steci3 but not steci1, then this
effectively selects a choice property out of thin air! Thus, just to implement
{steci}
will require us to adopt ZFC in full, including the Axiom of Choice.
Fortunately, we are in a position to do just that. We'll relate {steci}
to
surjections by choosing inverse functions.
ro da poi bridi ke'a ku'o ro de poi cmima ke'a ro di poi cmima ke'a zo'u:
pa ka ce'u bu'a kei steci de di
================================================= (steci-intel)
zi'o gairfancu di de pa ka ce'u bu'a gi'e du ce'u
Read carefully. On the top, we have a unary selbri, and on the bottom, we invoke it as part of a binary selbri. You could read the bottom function as both calling the top relation as a subroutine on the input, and also copying the input to the output.
Also, I'm using live sets here, despite using labels earlier. Sorry not sorry. I'll keep figuring it out.
Functions II
We'll need to be able to compose functions. The easy way is probably through the front door.
ro da poi ke'a fancu ko'a ko'e ku'o ro de poi ke'a fancu ko'e ko'i zo'u:
da fancu ko'a ko'e pa ka ce'u bu'a ce'u kei .ije de fancu ko'e ko'i pa ka ce'u bu'e ce'u
======================================================================================== (fancu-comp)
zi'o fancu ko'a ko'i pa ka de zo'u ce'u bu'a de .ije de bu'e ce'u
Maybe that's not so easy! We have to explicitly spell out all of the guts of our functions being composed, and don't have a high-level relation representing composition.
Elements:
Almost all sets have elements. In categories of sets, elements are functions from the singleton set. We need to carefully note an equivalence while allowing for distinction; this is part of the "name" concept of functions. A cat, for example, is not the same as the function which chooses it from the set of cats; it is, however, equivalent to the name of the function, and that's a sort of sameness.
As a compromise, the function corresponding to the element can be called, and
calling the function will yield the element. Function calls, like relation
traversals, are done with {ckini}
.
ro da poi cmima ke'a ku'o ro de poi bridi ke'a zo'u:
zi'o fancu le pamei da de
-------------------------------------------------- (cmima-elt)
su'o di zo'u di cmima da .ije tarci.bu di ckini de
The quantification is not great here. {di}
ranges over the set of {da}
,
which is effectively a dependent type. This doesn't surprise me greatly, since
I expected to find 2-categorical structure, but it will complicate the
quantification story. From this point forward, quantification is sketchy.
Subset structure
We'll give the axioms in ornate form. First, the Axiom of Extensionality: If two sets have all of the same supersets, then they're the same set.
ro da poi cmima ke'a ku'o ro de poi cmima ke'a zo'u:
pa ka zi'o steci da ce'u kei du pa ka zi'o steci de ce'u
-------------------------------------------------------- (steci-ext)
da du de
Next, the Axiom of the Empty Set: The empty set has no subsets; the set of subsets of the empty set is itself the empty set. This phrasing uses the idea that unary relations are equivalent to sets, which I haven't formalized further. It is lazy and probably we can do better.
le nomei du pa ka zi'o steci ce'u le nomei (steci-empty)
The Axiom of Pairing: Every pair of sets belongs to a set which contains both of them as elements. My version includes the steci1 which builds that set.
ro da poi cmima ke'a ku'o ro de poi cmima ke'a zo'u:
su'o di zo'u da cmima di .ije de cmima di (cmima-pair)
Finally, the Axiom of Union: We may take the union of a set's elements, and
it will again be a set. I'm not sure if I like the awkward phrasing I've used
here; it might be better put with more {cmima}
and no {steci}
.
ro da poi cmima ke'a zo'u:
su'o de zo'u pa ka ce'u cmima da kei steci de zi'o (steci-union)
Inline sets:
We can now give {ce}
, which is like {ce'o}
but forgets order. Since order
is forgotten, when I write {ce ...}
I mean that the set's elements can be
permuted arbitrarily.
ro da poi ke'a cmima zo'u:
da cmima da ce ... (ce-intel)
Incidentally, this gives the Axiom of Pairing in a lighter fashion.
Axiom of Anti-Foundation
Controversially, although nobody's really said anything yet, relational set logic tends to use the Axiom of Anti-Foundation, AFA, instead of the Axiom of Foundation.
AFA corresponds sets with rooted connected directed cyclic graphs; the root maps to the top of the set, and each path in the graph corresponds to a membership chain, with each edge being a single instance of membership. We will ask that our relations respect this structure when it occurs.
Articles I: {lo},
We are not quite yet to defining 1+1=2, but we have something just as great,
{lo}
. In xorlo, {lo}
is a generic selection. For BPFK, {lo}
is in the
formal gadri
definition
list. Here we are relatively precise about what {lo}
means, but we also use
nearly the same definition as BPFK, only swapping {poi}
for {noi}
and not
claiming any particular difference between the two.
Without further ado, the moment is here.
zo'u:
su'o da poi ke'a broda zo'u da brode
==================================== (lo-intel)
lo broda ku brode
Note that {lo}
folds a hidden bound value within itself, like with {zi'o}
.
In addition, the prenex was consumed. When we use {lo}
, we no longer have a
variable {da}
bound in scope.
We can also do a {be}
expansion. {be}
creates a side condition which must
be moved into the main formula.
su'o da poi ke'a broda ku'o su'o de poi broda ke'a ku'o zo'u da brode .ije da broda de
====================================================================================== (be-intel)
su'o de poi broda ke'a zo'u lo broda be de ku brode
We can use the two-dimensional existential quantifier rule here, though, and obtain a prenexed form which is more ergonomic:
ro de poi broda ke'a zo'u:
su'o da poi ke'a broda zo'u da brode .ije da broda de
===================================================== (be-intel)
lo broda be de ku brode
Natural Numbers Object: {kacna'u}, {kacli'e}, {sumji}, {pilji}, {li}, {no}, {pa}, ...
The set of natural numbers is equivalent to the unary relation {kacna'u}
.
First, let's populate the set. {li}
is grammar for a numeric constant
literal, the metavariable PA
matches any such literal, and the relation
{kacli'e}
sends Lojban natural numbers to their successor/increment.
Nothing magical, just mundane and tedious. Then, zero is a natural number:
li no kacna'u (kacna'u-zero)
And any successor of a natural number is also a natural number:
ro da zo'u:
da kacna'u
======================================= (kacna'u-succ)
su'o de zo'u de kacna'u gi'e kacli'e da
But zero is not a successor:
ro da zo'u:
da kacli'e li no
---------------- (kacli'e-zero)
gai'o
And the natural numbers have structural equality:
ro da ro de zo'u:
su'o di zo'u da .e de kacli'e di
-------------------------------- (kacli'e-succ)
da du de
This NNO is as strong as BA, the system of "baby arithmetic" obtained by weakening Robinson's arithmetic Q. To raise it up to Q, we need to remove all "pseudo-zero" non-successors:
ro da zo'u:
da kacna'u gi'e na du li no
--------------------------- (kacli'e-standard)
su'o de zo'u de kacli'e da
We also need to add arithmetic. For addition, we define {sumji}
. First,
anything plus zero is itself:
ro da zo'u:
da kacna'u
----------------- (sumji-zero)
da sumji da li no
Anything plus a successor is the successor of that thing and its -- look, it's simpler in formal Lojban!
ro da ro de ro di zo'u:
su'o daxivo zo'u di sumji da daxivo .ije de kacli'e daxivo
---------------------------------------------------------- (sumji-succ)
su'o daxivo zo'u daxivo sumji da de .ije daxivo kacli'e di
Maybe not too much simpler. Multiplication is similar, with {pilji}
:
ro da zo'u:
da kacna'u
-------------------- (pilji-zero)
li no pilji da li no
Again, the recursive case is simpler formally than informally. Note the similarity between the top parts of both recursive cases.
ro da ro de ro di zo'u:
su'o daxivo zo'u di pilji da daxivo .ije de kacli'e daxivo
----------------------------------------------------------- (pilji-succ)
su'o daxivo zo'u di sumji daxivo da .ije daxivo pilji da de
So, to be explicit, how do we use these? Well, let's define {li pa}
as an
example.
li no kacli'e li pa (kacli'e-pa)
li pa kacli'e li re (kacli'e-re)
Imagine the axiom schema which builds the NNO; CLL gives the algorithm for counting, and it's largely the same as standard decimal integer counting.
NFOL II: NNO Categoricity
We can give the induction principle for natural numbers with SO quantifiers.
ro bu'a zo'u:
ge li no bu'a gi ro da su'o de zo'u da na.a de bu'a .ije da kacli'e de
---------------------------------------------------------------------- (kacna'u-ind)
ro da zo'u da kacna'u nagi'a bu'a
Quantification I: {no}, {pa}, ...
An essential quantifier in maths is the uniqueness existential quantifier
{pa}
. We can build it from a careful modification of the standard phrasing.
ro bu'a ro de zo'u:
su'o da zo'u da bu'a .ije de bu'a nagi'a du da
============================================== (pa-unique)
pa da zo'u da bu'a
This lines up with both our intuitions on {ka}
from earlier, and also our
understanding of what uniqueness means: Any proclaimed witness to non-uniquess
is, by contraposition, actually equivalent to our original thing.
Articles II:
Next, we have {lo'i}
, which selects sets. Specifically, from the BPFK rule,
we have our rule:
lo se cmima be lo broda cu brode
================================ (lo'i-intel)
lo'i broda ku brode
Remember, we can't forget our relationships. But we also can't remember our
forgotten properties. {lo'i}
quantifiers are satisfied for each subset of
the original set. If we had three things which {broda}
, then we would bind
eight different sets to {lo'i broda}
.
Quantifiers II
We can also quantify {lo'i}
to force them to have a specific cardinality.
This is done merely by plumbing through the PA.
lo se cmima be lo PA broda cu brode da
====================================== (lo'i-pa-intel)
lo'i PA broda ku brode da
Since there is only one subset with the same cardinality as the superset,
there's only one way to bind this value. So, in effect, {lo'i}
with a
quantifier allows us to truncate and collect all at once.
Sets as Extensions:
{kampu}
relates {ka}
properties to their corresponding sets. We can give
an axiom for {kampu}
in terms of {cmima}
, via {lo'i}
.
pa ka ce'u broda kei kampu lo'i broda (kampu-def)
Quantifiers III
We can place a natural number directly onto a {da}
in order to quantify it.
The resulting bridi is, as before, all-or-nothing, based on the cardinality of
results, but otherwise doesn't change the binding. However, since the typical
{poi}
clause ranges over an entire relation, the cardinality of results
usually can be quite high, and as a result, quantifying {da}
usually just
leads to getting results in batches.
What's typical isn't guaranteed, though, so there's no rule that will add a
quantifier to {da}
. We can forget quantifiers, though, and that's a valid
one-way weakening.
PA da broda de
---------------- (pa-weak)
su'o da broda de
Placing a natural number as an outer quantifier onto {lo}
selects subsets of
the given cardinality from the entire set of results. This interpretation is
congruent with what we can derive from applying existing rule (lo-intel)
to
an outer quantifier.
PA lo broda ku brode
================================== (lo-intel)
PA da poi ke'a broda ku'o brode de
And similarly, putting an outer quantifier onto {lo'i}
selects subsets of
the already-selected subset. If there are four {mlatu}
total under
consideration, then {re lo'i ci mlatu}
will first select three cats, then
select two of those, binding a total of twelve times.
CLL allows for {PA broda} to be shorthand for {PA lo broda}.
PA lo broda ku brode
==================== (pa-lo-sugar) [CLL 6.8]
PA broda ku brode
BPFK defines {PA broda} as {PA da poi broda}. That sounds familiar, and indeed, we can recover this definition from a proof.
PA broda ku brode
==================== (pa-lo-sugar)
PA lo broda ku brode
================================== (lo-intel)
PA da poi ke'a broda ku'o brode de
Negation:
We now open the door to the ability to say no. First, note that the outer
quantifier {no}
can effectively act like a negation: If there are zero
results, then we succeed, and if there are any results at all, then we fail.
This is a gentle extension of negation as
failure; this is failure
as negation.
So, for unary selbri, we can start out by saying:
ro da poi ke'a broda zo'u:
no da broda
=========== (na-no-unary)
da na broda
But this is thorny for binary selbri. We will have a pair of one-way rules which have a round-trip in one direction but not the other.
ro da poi ke'a broda ro de pok broda ke'a zo'u:
no da broda no de
================= (na-no-binary-both)
da na broda de
If we made this two-way, then {na}
wouldn't always be dual to {no}
.
ro da poi ke'a broda ro de pok broda ke'a zo'u:
no da broda de
-------------- (na-no-binary)
da na broda de
Logical Set Operators: {ja}, {jo'e},
By flipping around the universal properties, we can build some operators and
also define more logical connections. First, let's define {ku'a}
, the
intersection of two sets.
lo'i broda je brode ku brodi
====================================== (ku'a-intel) [CLL 14.15]
lo'i broda ku ku'a lo'i brode ku brodi
We know what {jo'e}
is, too; it's the union of sets. We have the disjoint
union already, and the non-disjoint union simply forgets that its components
come from one option or another. What is {ja}
, though? Traditionally, in
classical logic, it's an inclusive Boolean OR. We need to preserve all of the
related data, though, and for the OR operation, it's whether only one of the
branches is taken, or both are taken. Those cases are themselves disjoint, and
so we have an equivalence:
ro da ro de zo'u:
da broda jonai brode jonai ke broda je brode de
=============================================== (ja-intel)
da broda ja brode de
This is an awkward amount of data. But now we can define {jo'e}
:
lo'i broda ja brode ku brodi
====================================== (jo'e-intel) [CLL 14.15]
lo'i broda ku jo'e lo'i brode ku brodi
Tracing back through the data, on the bottom of the equivalence, we have elements belonging to one set or the other or possibly both.