lojban Formulae
Lojban Formulae
This represents an attempt to reconstruct a certain phase in the development of Lojban, somewhere between CLL and xorlan, incorporating the practical changes that had been worked out since CLL, without getting into the open-ended process of change incorporated in xorlan.
(This has been revised several times, so parts may be in error for failure to update them. There are also the usual – for me – typos and cases where I just have it wrong. There are also many things left out because I did not think of them – or don’t yet know what to think of them. Comments and corrections are encouraged. Note: failure to agree with CLL or xorlan is not necessarily an error.)
(I have changed “group” to “bunch” to get away from the Lojban uses of “group,” which have often been only for collective predication, and from the complaints of mathematically-minded readers.)
Bunches.
If we build Lojban on standard formal logic, all of its terms have to be singular. That is, each variable is evaluated to a single object and thus all terms – which have to substitute for variables in generalization and instantiation – must refer to single objects (or else valid rules would lead from truth to falsehood). But there are cases where, in order to make normal sense out of the expression, a term has to refer to several objects, as we would normally say. To deal with these cases (and then to others where plurality is handy though not essential), Lojban needs a single thing that can stand in for many things. Lojban has sets explicitly, but sets come with a history that makes it difficult to use them in this new role: for the most part, one would have to go down to the members, organize them again somehow, and then use this new organization. So Lojban (implicitly but usually unnoted – largely because undeveloped) uses bunches, which are simpler and closer to members. In fact they have roughly the logic of mereological sums (which they might in fact be for all the difference it makes). That is, they are an organization of fundamental things (individuals relative to the bunches to be developed – it is a metaphysical question whether there are absolute individuals and we don’t care at this point) by a relation (here expressed as “encompasses,” \x\yxCy) which works down to the individuals (relative to the bunch at the top) ever more encompassing bunches (the individual things and their ordering). We shall write (this is all nonce) “<a>” for the bunch whose only member is a, <ab> for the one with only a and b, and so on. The annotation is symmetric: <ab> = <ba>; associative: <<ab>c> = <a<bc>>; idempotent <aa> =<a>; and reductive <<a> b> = <ab>. The relation C is reflexive (aCa), transitive (if aCb and bCd then aCd), antisymmetric (If a =/= b and aC b then ~bCa), connected above (aCb or bCa or there is d: dCa and dCb), and founded: (for every bunch a there is an individual relative to a, b, such that a C b).
The logic here is first order predicate calculus with restricted quantification (and Aristotelian quantifiers, A and I – universal and particular affirmative, both importing*) with functions forming bunches from individuals (including sets – and bunches for that matter, though these collapse) and the constant C. “xF” is defined originally only for x a bunch and the predication being collective “x c-F”(that is, the bunch as a whole has the property but some of its components may not – and some of the bunches of which it is a component may not, even if the additional bunch has it). “xF” for x an individual and for distributive (non-collective) predication are defined from this base: if a is an individual, a i-F iff <a> c-F; if a is a bunch, a d-F iff, for every individual b such that aCb, b i-F. Although collective predication is basic, when the predication of a place is not fixed and is unmarked, it is taken to be distributive (on the – untested -- assumption that this is the more common case). Unrestricted quantifiers are defined in terms of another constant predicate, “exists,” !: Qx xF iff Qx: x! xF. For every predicate, F, there is a d-predicate, F*, defined as a F* iff Ix: x bunch & xCa x F (Clearly, for d-F, F* is just F)…
- The corresponding E and O, negative universal and particular, non-importing, are just ~I and ~A respectively. The quantifiers of opposite polarity are obtained from the horizontally opposite by negating the predicate or the vertically opposite by negating both the whole and the predicate: A- = E~ = ~I~ and similarly for E+, I- and O+.
Lojban has to deal with a number of quantifiers in addition to the Aristotelian ones (and their mirrors). Many of these can be defined directly in terms of the Aristotelian ones with the help of identity and patience. For now we will treat them as reflecting predicates on bunches (collectively). Even with this they fall into three patterns: numeric, proportional, and relative. The numeric predicates have the form “a is Q in number,” where Q is a number, or an expression like “at least #” or “more than #” or “approximately #.” Proportional quantifiers have the form “a is Q of b” where b is some bunch and Q is a fraction, decimal, or percentage; the whole says that the cardinality of a – the number of individuals in it – is Q of the cardinality of b. b is usually specified in the formulae that follow but that can be overridden (and occasionally supplemented) by a phrase introduced by a new item of NE followed by the name of a bunch.
Relative quantifiers have the form “a is Q for (/to/that/…) b,” where b is an event description. Each of these quantifiers carries in its translation a specification of the appropriate connector: so “enough (for/to),” “so many (that),” and “as many as (for).” Generally, b will be “obvious” from context – roughly making the sentence in which it is embedded true -- but it can be specified by a new NE followed by an event description*.
With this background, we can now given the following analyses:
For first occurrences (i.e., nothing already assigned or bound here –except contextually in e and a series)
{ko’a broda}
aF
(a is assumed to be a bunch, though perhaps encompassing only a single individual. If the collectivity of F/broda is not defined it is here assumed to be distributive. For cases where both are possible and collective is wanted:)
{lu’o ko’a broda}
a c-F
{Q da broda}…
Ix: x bunch x F* & Ay: y F* x C y & xQn / xQf of the existents / xQr
(This bunch is called “the F*s” in what follows) …
(Q cannot evaluate to 0, {no} and its equivalents are handled separately – as E, that is ~I:)
{no da broda}
Ex xF or, more clearly, ~Ix xF
{Q da poi broda cu brode…}
[[Ix: x bunch & xF* & [Az: zF*]] xCz] Iy:xCy yG & yQn/ xQf of the F*s/xQr
{no da poi broda cu brode}
(This says that no brodas brode but is noncommittal about whether there are brodas that don’t brode. That there are requires importing E, E+, =A~:)
{ma’u no da poi broda cu brode}
(Note: {no da broda} would be true if nothing existed. To make sure that we are not talking about the empty world – when nothing else in the context decides the issue – {ma’u no da broda} would be needed.)
{lo broda cu brode}
Ix: x bunch & xF x d-G & x is enough of the F*s
{loi broda cu brode}
Ix: x bunch & xF x c-G & x is enough of the F*s
{lo’i broda cu brode}
Ix: x bunch & Fx {y: ~y bunch & xCy}G
{le broda cu brode}
for some x1 … xn contextually identified
<x1 … xn> “F” & <x1…xn> d-G
{lei broda cu brode}
for some x1…xn contextually identified
<x1 … xn> “F” & <x1…xn> c-G
{le’i broda cu brode}
for some x1…xn contextually identified
{x1 …xn} G & <x1…xn> “F”
({la/lai/la’i} are the same with the different interpretation of “F”
{lo broda goi ko’a cu brode}
Ix: x bunch & xF x is enough of the F*s & x = a & a d-G
(and similarly for all the above)
{lo Q broda cu brode}
Ix: x bunch & xF x d-G & x Qn/Qp of the Fs/ Qr of the F*s
(the last phrase is abbreviated “Q of the F*s”)
(Q cannot be 0 in this pattern.)
(And similarly for all the others, that is the phrase “is enough of the F*s” is replaced by the appropriate Q version of “Q of the F*s.”
{Q lo broda cu brode}
Ix: x bunch & xF Iz: z bunch & xCz z d-G & z is Q of x
{no lo broda cu brode}
Ix: x bunch & xF Az: z bunch & xCz ~z d-G
(And similarly for the others: a second, sub, bunch is introduced and the Q relates its size to that of the original bunch. With {lo/ei} the bunch is predicated of collectively.)
{Q1 lo Q2 broda cu brode}
Ix: x bunch & xF Iz: z bunch & xCz z d-G & z is Q1 of x & x is Q2 of the F*s
{Q1 loi Q2 broda cu brode}
Ix: x bunch & xF Iz: z bunch & xCz z c-G & z is Q1 of x & x is Q2 of the F*s
(And so on, combining the information from forms with Q1 only and those with Q2 only.)
In particular, for le/o’i:
Q1 lo’i Q2 broda cu brode
Ix: x bunch & xF [[Iy: y c {z: xCz}]] yG & yQ1 of x & xQ2 of the F*s
Q1 le’i Q2 broda cu brode
For some x1…xn contextually identified
[[Iy: y c {x1…xn}]] yG & <x1…xn> “F” & <x1…xn> Q2 of the F*s & y Q1 of <x1…xn>
{lo broda poi brode cu brodi}
Ix: x bunch & x F & x G x d-H & x is enough of the (F* & G*)s
(And similarly throughout, expanding the predicate in the quantifier phrase)
{Q lo broda poi brode cu brodi}
Ix: x bunch & x F & x G Iz: z bunch & xCz z d-H & z is Q of x
{Q lo broda ku poi brode cu brodi}
Ix: x bunch & x F Iz: z bunch & xCz zG & z d-H & z is Q of x
{lo broda noi brode cu brodi}
Ix: x bunch & x F x d-H & x is enough of the F*s. x G
(The significance of the period is just that it puts what is after it outside the scope of modifications on the original sentence: negation in particular, but also other operators.)
{Q lo broda ku noi brode cu brodi}
Ix: x bunch & x F Iz: z bunch & xCz z d-H & z is Q of x. zG
If the core term is already introduced then anaphoric cases of the <<>>d term are treated as follows, with a standing for the continuing term in the formula, Qs not {no}, but Q1 can be {ma’u no}, Qdescription and description have different anaphora from the same first occurrence.
{<<da (poi broda)>> brodi}
xH
assuming h/brodi is open (can be either collective or distributive).
<<ko’a>> brodi
<<(Q1)lo/e/a (‘i) (Q2) broda>> brodi
lu’a <<(Q1) lo/e/ai (Q2) broda>> brodi
a d-H
lu’o <<ko’a>> brodi
<<(Q1)lo/e/ai (Q2) broda>> brodi
lu’o<<(Q1) lo/e/a (‘i) (Q2) broda>> brodi
a c-H
if H/brodi is fixed
<<ko’a>> brodi
<<(Q1)lo/e/a (‘i) (Q2) broda>> brodi
<<(Q1)lo/e/ai (Q2) broda>> brodi
a H (whichever type predication H is)
Controversial:
Q <<da (poi broda)>> brodi
Q <<ko’a>> brodi
Q <<(Q1) le/o/a -/i/’i (Q2) broda>> brodi
Iz: z bunch & aCz zH & zQ of a (‘x’ for ‘a’ in the case of {da})
no <<>> brodi
~Iz: aCz zH
<<>> (ku) poi brode cu brodi
Iz: z bunch & aCz & zG zH (‘x’ for ‘a’ with {da})
Plural Quantification
In this system, reference is simply a relation, not a function. That is, each term is related to some number of things (0 or more), each of which is (part of) the meaning of the term, a referent of the term. In general, a term refers to all of its referents, though other versions are possible (but more complex). Thus, a variable may introduce a number of things to be compared, separately or together, depending on the nature of the predication, with what satisfies a given predicate. And an unbound term may also introduce several things one way or the other. In this system, these several things play the same role as was played by the bunch that encompassed them in the bunch-based system. Indeed, to get from the bunch based system to this one, it seems almost enough to simply drop the “x bunch &” portion of many predications and replace “aCb” with the corresponding relation among several things, “bAa,” “b is among a” – each of the several things that together are covered by “b” is also one of the things covered by “a.” With these changes, it seems that the analyses given above for bunches apply for plural quantification as well:
For first occurrences:
{ko’a broda}
aF
(a may refer to several individuals. If the collectivity of F/broda is not defined it is here assumed to be distributive. For cases where both are possible and collective is wanted:)
{lu’o ko’a broda}
a c-F
{Q da broda}…
[[Ix x F* & [Ay: y F*]] yAx] Q of the existents
{no da broda}
~Ix xF
{Q da poi broda cu brode…}
[[Ix: xF* & [Az: zF*]] zAx] Iy: yAx yG & yQ of the F*s
{no da poi broda cu brode}
~Ix: xF xG
{ma’u no da poi broda cu brode}
Ax:Fx ~xG
{lo broda cu brode}
Ix: xF x d-G & x is enough of the F*s
{loi broda cu brode}
Ix: xF x c-G & x is enough of the F*s
{lo’i broda cu brode}
Ix: xF {y: yAx}G
{le broda cu brode}
for some x contextually identified
x “F” & x d-G
(for several particular individual, we just list them)
{lei broda cu brode}
for some x contextually identified
x “F” & x c-G
{le’i broda cu brode}
for some x contextually identified
{y: yAx} G
({la/lai/la’i} are the same with the different interpretation of “F”
{lo broda goi ko’a cu brode}
Ix: xF x is enough of the F*s & x = a & a d-G
(and similarly for all the above)
{lo Q broda cu brode}
Ix: xF x d-G & xQ of the F*s
{Q lo broda cu brode}
Ix: xF Iz: zAx z d-G & z is Q of x & x is enough of the F*s
{no lo broda cu brode}
{Q1 lo Q2 broda cu brode}
Ix: xF Iz: zAx z d-G & z is Q1 of x & x is Q2 of the F*s
{lo broda poi brode cu brodi}
Ix: x F & x G x d-H & x is enough of the (F* & G*)s
{Q lo broda poi brode cu brodi}
Ix: xF & xG Iz: zAx z d-H & z is Q of x
{Q lo broda ku poi brode cu brodi}
Ix: x F Iz: zAx zG & z d-H & z is Q of x
{lo broda noi brode cu brodi}
Ix: x F x d-H & x is enough of the F*s. x G
{Q lo broda ku noi brode cu brodi}
Ix: xF Iz: zAx z d-H & z is Q of x. zG
{<<da (poi broda)>> brodi}
xH
assuming h/brodi is open
<<ko’a>> brodi
<<(Q1)lo/e/a (‘i) (Q2) broda>> brodi
lu’a <<(Q1) lo/e/ai (Q2) broda>> brodi
a d-H
lu’o <<ko’a>> brodi
<<(Q1)lo/e/ai (Q2) broda>> brodi
lu’o<<(Q1) lo/e/a (‘i) (Q2) broda>> brodi
a c-H
if H/brodi is fixed
<<ko’a>> brodi
<<(Q1)lo/e/a (‘i) (Q2) broda>> brodi
<<(Q1)lo/e/ai (Q2) broda>> brodi
a H (whichever type predication H is)
Controversial:
Q <<da (poi broda)>> brodi
Q <<ko’a>> brodi
Q <<(Q1) le/o/a -/i/’i (Q2) broda>> brodi
Iz: zAa zH & zQ of a (‘x’ for ‘a’ in the case of {da})
no <<>> brodi
~Iz: zAa zH
<<>> (ku) poi brode cu brodi
Iz: zAa & zG zH (‘x’ for ‘a’ with {da})
“The most likely Fs”
Standard logic contains a theorem that can be read (however questionably) as introducing the most likely F, a thing such that, if anything at all is an F, it is: Ix(Iy yF => xF). In fact, this thing (as it were) having F is equivalent to something having F. But this mysterious x is a term rather than a quantifier (and we can still make this distinction syntactically at least). We can then devise an expression that represents this object, for each property F, and use it instead of particular quantifiers, when it is convenient to do so. The details of various ways to do this need not concern us here; we take the commonality of these approaches and indicate the most likely F as “Yx: x F.”* Since this is a term, it goes directly into a predicate place, that is “the most likely F is G” comes out as “Yx:FxG,” which is another way of saying Ix: Fx xG, and thus as “an F is G.” It is important to note, that in a given context, ‘Yx: xF” refers to the same thing in all its occurrences, is a constant in that sense at least.
- “Y” is picked to fit in with the pattern of Aristotelian quantifiers, even though this is not strictly a quantifier. It would be the sixth such, leaving “U” for the singular predication “a certain (this, that, or the one named or described) F is G.”
The theorem and the rest of the apparatus carry over to plural quantification as well, where
“Yx: xF G” is now “The most likely Fs are G” or “There are Fs that are G.” Using this notion, we can simplify our analysis somewhat, coming to something closer to the Lojban in most places. The move is summarily to replace “Ix: xF xG” with “Yx: xFG” and all subsequent xs bound by the original quantifier by “Yx:Fx.” This clearly does not shorten the notation, but it does get rid of many extended bound variable scope and, as noted, is closer in form to Lojban. We here use a mixed version that repeats only its variable after the first occurrence of the “most likely” term, standing always for that term, but not technically bound.
(More on this in Descriptions.)
For first occurrences:
{ko’a broda}
aF
{lu’o ko’a broda}
a c-F
{Q da broda}
[[Ix xF* & [Ay: y F*]] yAx] xQ of the existents
{no da broda}
~Ix xF
{Q da poi broda cu brode}
[[Ix: xF* & [Az: zF*]] zAx] Iy: yAx yG & yQ of the F*s
{no da poi broda cu brode}
~Ix: xF xG
{ma’u no da poi broda cu brode}
Ax:Fx ~xG
{lo broda cu brode}
Yx: xF d-G & x is enough of the F*s
{loi broda cu brode}
Yx: xF c-G & x is enough of the F*s
{lo’i broda cu brode}
{y: yAYx: xF} G
{le broda cu brode}
for some x contextually identified
x “F” & x d-G
{lei broda cu brode}
for some x contextually identified
x“F” & xc-G
{le’i broda cu brode}
for some x contextually identified
{y: yAx}G & x“F”
({la/lai/la’i} are the same with the different interpretation of “F”
{lo broda goi ko’a cu brode}
Yx: xF is enough of the F*s & x = a & a d-G
{lo Q broda cu brode}
Yx: xF d-G & x Q of the F*s
{Q lo broda cu brode}
[[Yz: zA[Yx: xF]] d-G & z is Q of x
{no lo broda cu brode}
[[Az: zA[Yx: xF]] ~z d-G
{Q1 lo Q2 broda cu brode}
[[Yz: zA[Yx: xF]] d-G & z is Q1 of x & x is Q2 of the F*s
{lo broda poi brode cu brodi}
Yx: x F & x G d-H & x is enough of the (F* & G*)s
{Q lo broda poi brode cu brodi}
[[Yz: zA[Ix: x F & x G]] d-H & z is Q of x
{Q lo broda ku poi brode cu brodi}
[[Yz: zA[Yx: x F]] G & z d-H & z is Q of x
{lo broda noi brode cu brodi}
Yx: x F d-H & x is enough of the F*s. x G
{Q lo broda ku noi brode cu brodi}
[[Yz: zA[Yx: x F]] d-H & z is Q of x. zG
{<<da (poi broda)>> brodi}
xH
assuming h/brodi is open
<<ko’a>> brodi
<<(Q1)lo/e/a (‘i) (Q2) broda>> brodi
lu’a <<(Q1) lo/e/ai (Q2) broda>> brodi
a d-H
lu’o <<ko’a>> brodi
<<(Q1)lo/e/ai (Q2) broda>> brodi
lu’o<<(Q1) lo/e/a (‘i) (Q2) broda>> brodi
a c-H
if H/brodi is fixed
<<ko’a>> brodi
<<(Q1)lo/e/a (‘i) (Q2) broda>> brodi
<<(Q1)lo/e/ai (Q2) broda>> brodi
a H (whichever type predication H is)
Controversial:
Q <<da (poi broda)>> brodi
Q <<ko’a>> brodi
Q <<(Q1) le/o/a -/i/’i (Q2) broda>> brodi
Yz: zAa H & zQ of a (‘x’ for ‘a’ in the case of {da})
no <<>> brodi
~Iz: zAa zH
<<>> (ku) poi brode cu brodi
Iz: zAa & zG H (‘x’ for ‘a’ with {da})