gadri: an unofficial commentary from a logical point of view

BPFK's gadri page contains expressions misleading people who have at least a little knowledge of logic (discussion).
I will make here a commentary on BPFK's gadri so that it is undersood by them correctly.

Glossary

We will use the following terms in this commentary.

argument (sumti)

Symbol that refers to a referent, or that another argument can be substituted for.

universe of discourse

Set of all referents of arguments. It is naturally a universe that is discussed. A universe of discourse depends on the context.

constant

Argument that refers to a referent.

variable

Argument as a place holder. It does not refer to anything. It is to be substituted for. Variable other than bound variable that will be defined below is called free variable. The truth value of a sentence that includes a free variable is indefinite. Such a sentence is called open sentence.

quantify

In substituting possible arguments one by one for a variable in a sentence, count the number of referents that make the sentence true, and prefix the number to the variable.

quantifier

Number used for quantification. Besides {pa}, {re}, {vei ny su'i pa (ve'o)} and so on, {ro} "all" and {su'o} "there is one or more" are also quantifiers.

bound variable

Variable prefixed by a quantifier. As a result of quantification, there is no room for substituting an arbitrary argument for the variable.

domain

Range of referents to be substituted for a variable, or range to be considered in counting referents in quantification.

tautology

Sentence that is always true independently of context. {ko'a du ko'a} etc.

logical axioms

Sentences selected from tautologies so that all tautologies are proved from them with rules of inference that are defined.

1.2. Plural quantification

In order to understand arguments of Lojban from a logical point of view, it is essential to have a knowledge of plural quantification (see, for example, Thomas McKay: Plural Predication, Oxford University Press, 2006).

Plural quantification was invented in order to facilitate expression of proposition that is meaningful only when the referent of an argument is plural.

Logically, this sentence is a proposition that consists of a constant "people" and three predicates "gathered" "cooked" and "ate". The predicates are different from each other in property of treating the argument. We will discuss precisely how the argument in the sentence is treated.

1.2.1. Collectivity and distributivity

Consider the expression "people gathered": based on the meaning of the predicate "gathered", the constant "people" should refer to plural people.
When referents of an argument satisfy a predicate as collective plural things like this, we express it as "an argument satisfies an predicate collectively", or "the argument has collectivity".

As for each of the plural people referred to by the constant, each sentence such that "Alice gathered", "Bob gathered" and so on is nonsense.
When each referent referred to by a constant cannot satisfy a predicate alone, we express it as "an argument satisfies an predicate non-distributively".

On the other hand, in the expression "people ate", although the constant "people" refers to plural people, the predicate "ate" is satisfied by each person. That is to say, each sentence such that "Alice ate", "Bob ate" and so on is meaningful.
When each referent referred to by a constant satisfies a predicate alone, we express it as "an argument satisfies an predicate distributively", or "the argument has distributivity".

Moreover, if the predicate "eat" means an act "put food in a mouth, bite it, let it pass through an esophagus and send it to a stomach", it is hardly considered that "people" satisfies "eat" collectively. Even if a person helps another to eat, the helper is not eater, and the eater is not collective people but an individual.
When each referent referred to by a constant cannot satisfy a predicate as collective plural things, we express it as "an argument satisfies an predicate non-collectively".
(However, it is possible to interpret the predicate "eat" as involving collectivity. For example, if it is interpreted as "put food away from outside to inside of body", we may say "collectively eat" to express an event that people eat and consume a mass of food together.)

There are also predicates that allow both properties "collectivity" and "distributivity".
"People cooked" may mean that plural people knead paste of pizza together, and that each of them is in charge of cakes or pot-au-feu. In this case, the constant "people" refers to plural people, and they cooked pizza collectively, cakes and pot-au-feu distributively. The constant "people" thus satisfies the predicate "cooked" collectively and distributively.

Note that the constant "people" refers to what is common to three predicates "gathered", "cooked" and "ate". No matter if a constant satisfies predicates collectively or distributively, the referent is the same.

If we use an argument "a set of people" in the case of satisfying a predicate collectively, it might be possible to interpret the predicate "gathered" so that the argument satisfies it, but the same argument cannot satisfy the predicate "ate", because we can hardly say that a set of people, which is an abstract entity, performs "ate".

Using plural constants and plural variables that will be discussed in the following sections, we can express plural things in the form of predicate logic without using sets.

1.2.2. Plural constant and plural variable

An argument that refers to referent without introducing a notion of sets, without distinguishing collectivity and distributivity, without distinguishing plurality and singularity, is called plural constant.
A variable for which a plural constant can be substituted is called plural variable.
Quantifying a plural variable is called plural quantification. A quantifier used for plural quantification is called plural quantifier. A plural variable prefixed with a plural quantifier is called a bound plural variable.

1.2.2.1. me and jo'u

We introduce relations between plural constants and plural variables: {me} and {jo'u}.

X and Y represent here plural constants or plural variables. A cluster {me Y (me'u)} is a selbri in Lojban grammar. {me'u} is an elidable terminator of structure beginning with {me}.

{me} has the following properties with arbitrary arguments X, Y and Z:

1. X me X (reflexivity)
2. X me Y ijebo Y me Z inaja X me Z (transitivity)
3. X me Y ijebo Y me X ijo X du Y (identity)

The property 3 means that the identity between referents of X and Y is represented with {me}, as a relation that {X me Y ijebo Y me X}.

{jo'u} combines two arguments X and Y into one plural constant or one plural variable.

{jo'u} has the following properties with arbitrary arguments X and Y:

1. X me X jo'u Y
2. X jo'u Y du Y jo'u X
3. X jo'u X du X

The property 2 means that the referent of the whole argument does not vary when two arguments combined by {jo'u} are interchanged with each other. The property 3 means that {jo'u} does not add any referent when it combines an argument with itself.

Using {jo'u}, the following expression is possible:

Each of {by} and {cy} is a plural constant.

The predicate {jukpa} (cook) can be interpreted collectively and/or distributively, but the plural constant {by jo'u cy} says nothing about whether it satisfies {jukpa} collectively and/or distributively. If we want to make explicit that they cooked "collectively", we say {by joi cy} using {joi} that will be discussed in ((|#Relation_between_jo_u_joi_ce_and_gadri|Section 3.4)), or {lu'o by jo'u cy} using {lu'o} that will be discussed in ((|#Relation_between_lu_a_lu_o_lu_i_and_gadri|Section 3.3)). Contrastively, if we want to make explicit that they cooked "distributively", we say {lu'a by jo'u cy} using {lu'a} that will be discussed in ((|#Relation_between_lu_a_lu_o_lu_i_and_gadri|Section 3.3)). However, these arguments that says explicitly collectivity and/or distributivity are not always commonly used for other predicates like {jmaji} or {citka}.

The diagram below shows relations constructed with {me} and {jo'u} represented with a directed graph, in which the vertices represent plural constants.

1.2.2.2. Individual

Referent of a plural constant is not necessarily plural: a plural constant can refer to one individual.
An individual is defined as follows:

where ro'oi is an experimental cmavo proposed by la xorxes, which is a plural quantifier meaning "all". {ro'oi da} is a bound plural variable meaning "for all that can be substituted for {da}". This definition means that X is called an individual when the condition "for all {da} that are among X, X is among {da}" is satisfied. In other words, "in the universe of discourse, nothing other than {X} can be substituted for {da} such that {X me da}" is expressed by "X is an individual".

When each of X and Y is an individual and X is not equal to Y, {X jo'u Y} is called individuals. When each of X and Y is an individual or individuals, {X jo'u Y} is called individuals as well.

1.2.2.3. Difference between plural and singular

A plural constant that refers to a single individual is called a singular constant.

Unless X=Y and X is an individual, no matter whether each of X and Y is plural or singular, {X jo'u Y} is not a singular constant. It is because

holds true, and then {X jo'u Y} does not satisfy the condition of an individual {ro'oi da poi ke'a me X jo'u Y zo'u X jo'u Y me da}.

1.2.2.4. Bound singular variable

When the domain of a bound plural variable is restricted to what is an individual, the variable is called bound singular variable. A bound singular variable cannot take more than one individual value at a time.
{ro da} (for all {da}) and {su'o da} (there is at least one {da}), which are officially defined in Lojban, are bound singular variables. They can be defined with bound plural variables as follows:

su'oi is an experimental cmavo proposed by la xorxes, and is a plural quantifier meaning "there is/are". Note that {su'oi} is not "at least one". {su'oi da} is a bound plural variable meaning "there is/are {da}".

1.2.2.5. What is neither an individual nor individuals

Referent of a plural constant is not necessarily an individual or individuals.
It is possible to discuss a universe of discourse such that referent of a plural constant is neither an individual nor individuals.

For example, consider such a universe of discourse in which the following proposition holds true.

In other words, in this universe of discourse, for all X such that {X me ko'a}, there is always Y such that {Y me X} and not {X me Y}.

Theorem

In a universe of discourse where Condition_1 is true, {ko'a} is neither an individual nor individuals.

Proof

Suppose {ko'a} is an individual. From the definition of "an individual":

Replace {ro'oi da} with {naku su'oi da naku}:

Move the inner-most {naku} into the proposition:

Replace {su'oi da poi} with {ije} and move into the proposition:

Replace {ije naku} with {ijenai}:

By the way, from a property of {me},

is always true. {ko'a} is therefore in the domain of {da} of Condition_1. Replace {ro'oi da} of Condition_1 with {ko'a}, and it thus holds true:

Condition_1-1 and Supposition_2-4 contradict each other.
Supposition_2 is thus rejected by reductio ad absurdum.
It means that {ko'a} is not an individual.

Moreover, when {ko'a} is expanded to {A jo'u B}, from a property of {jo'u}, the following propositions hold true:

Each of A and B is in the domain of {da} of Condition_1. Considering similarly to Condition_1-1, neither A nor B is an individual. {ko'a} is thus not individuals.
Q.E.D.

When {ko'a} is neither an individual nor individuals, what actually does it refer to?
We may interpret that it refers to what is referred to by a material noun, for example.
By a speaker who thinks that a cut-off piece of bread is also bread, bread is regarded as neither an individual nor individuals.

(I wrote the same proof only in Lojban.)

1.2.2.6. A logical axiom on plural constant

The following logical axiom is given to an arbitrary plural constant C:

It means "in a universe of discourse, if a proposition in which a plural constant is x1 of {broda} holds true, there is referent that is x1 of {broda}".

That is to say, an argument that has no referent in a universe of discourse cannot be represented by a plural constant. An argument that has no referent is expressed in the form {naku su'oi da}, which is a negation of a bound plural variable {su'oi da} meaning "there is/are".

1.3. Definition of gadri

lo (LE)

It is prefixed to selbri, and forms a plural constant that refers to what satisfies x1, the first place of the selbri. If a quantifier follows {lo}, the quantifier represents the count of all the referents of the plural constant. In the case that a quantifier follows {lo}, a sumti may follow it. In this case, it forms a plural constant that refers to what is/are among sumti.

{ku}, {ku'o}, {me'u} are elidable terminators.

Putting a quantifier after gadri like {lo PA} is called inner quantification, and the quantifier is called inner quantifier. Although the term "quantify" is involved, it is different from quantification of logic. Inner quantification does not involve counting referents of constants that can be substituted for a variable, but counting all the referents of one plural constant. Inner quantification will be discussed more precisely in ((|#Inner_quantification|Section 3.1)).

On the other hand, putting a quantifier before gadri, or before a sumti more generally, is called outer quantification, and the quantifier is called outer quantifier. Outer quantification will be discussed more precisely in ((|#Outer_quantification|Section 3.2)).

All sumti formed with gadri are defined so that they are expanded into expressions with {zo'e}. That is to say, the most general plural constant is represented by a single {zo'e}. A sumti formed with gadri is {zo'e} accompanied by an explanation.

While the predicate {jukpa} (cook) can be interpreted collectively as well as distributively, the plural constant {lo prenu} (people) does not say explicitly if it satisfies {jukpa} collectively or distributively. If we want to say explicitly that they "collectively" cooked, we use {loi}, which will be discussed later, and say {loi prenu}. Contrastively, if we want to say explicitly that they "distributively" cooked, we say {ro lo prenu} with an outer quantification, or {lu'a lo prenu}. However, a sumti that says explicitly collectivity or distributivity is not necessarily able to be shared with other predicate like {jmaji} or {citka}.

le (LE)

{le broda} refers specifically to a referent of {lo broda}, and explicitly express that the speaker has the referent in mind. Its logical property is the same as that of {lo}.

la (LA)

It is prefixed to selbri or cmevla, and forms a plural constant that refers to what is named the selbri or cmevla string. Its logical property is the same as that of {lo}.

loi (LE), lei (LE), lai (LA)

{loi/lei/lai broda} refers to a referent of {lo/le/la broda}, and explicitly express that the referent satisfies a predicate collectively.

Because {loi/lei/lai} is thus defined by another plural constant {lo gunma be lo/le/la}, it does not refer directly to referent of {lo broda} or {lo PA sumti}, but referent of {lo gunma}. Therefore, even if {lo broda} or {lo PA sumti} is not an individual, {loi broda} or {loi PA sumti} can be an individual {lo gunma} under the following condition:

lo'i (LE), le'i (LE), la'i (LA)

{lo'i/le'i/la'i broda} refers to a set or sets of individual(s) that constitute(s) a plural constant {lo/le/la broda}. Because {lo'i/le'i/la'i} forms a set or sets, it is defined only when its/their member(s) {lo/le/la broda} is/are an individual or individuals. A set itself is always an individual, and sets are always individuals: there is no set that is not an individual.

Because {lo'i/le'i/la'i} is defined by another plural constant {lo selcmi be lo/le/la}, it does not refer directly to referent of {lo broda} or {lo PA sumti}, but referent of {lo selcmi}.

In set theory, an empty set is defined as {lo selcmi be no da}, and an expression {lo no broda} is officially meaningless (see ((|#Inner_quantification|Section 3.1)). This implies that an empty set cannot be expressed with {lo'i/le'i/la'i}.

If we accept this definition, a set referred to by {lo'i/le'i/la'i}-sumti consists of only the referent of {lo/le/la [PA] broda} or {lo/le/la PA sumti}. Contrastively, if we define it as {selcmi}={se cmima}, the set may include what is/are other than the referent of {lo/le/la [PA] broda} or {lo/le/la PA sumti}. It is not yet officially determined which interpretation is to be accepted.

1.3.1. Inner quantification

BPFK defines inner quantification as follows:

That is to say, inner quantifier means number of referent counted by unit {lo broda} or {lo me sumti} that is x3 of {zilkancu}.
However, instead of {zilkancu}, the meaning of which is too vague for definition, an idea of redefinition using {mei} was suggested as follows:

Axiom 1

ro'oi da su'o pa mei

Definition

(D1) ko'a su'o N mei	=ca'e	su'oi da poi me ko'a ku'o su'oi de poi me ko'a zo'u ge da su'o N-1 mei ginai de me da
(D2) ko'a N mei	=ca'e	ko'a su'o N mei gi'e nai su'o N+1 mei
(D3) lo PA broda	=ca'e	zo'e noi ke'a PA mei gi'e broda

Using these definitions and Axiom 1, the following theorem will be proved.

Proof

(D2) is

Applying (D1) to (S2),

(D2) is therefore

When N=1,

Because of Axiom 1, it implies

The right side implies {ro'oi da poi ke'a me ko'a zo'u ko'a me da}, which is the condition for "{ko'a} is an individual". Its converse is also true.
Q.E.D.

The diagram below shows a procedure of counting something up to four represented with a directed graph. In this diagram, loops such as {X me X} are omitted for simplicity, though they exist. Counting up corresponds to selecting a subgraph of a directed graph formed with {me}: the subgraph that has a form of tree that includes all leaves (constants each of which is an individual) to be counted, for example the part of magenta color in the diagram.

1.3.1.1. Repeating inner quantification

Because {lo PA sumti} is defined, we can repeat inner quantification to form an argument.

1.3.1.2. Problems on inner quantification

1.3.1.2.1. Cannot say zero

Because an argument formed by gadri is a plural constant, {lo broda} implies {su'oi da zo'u da broda} according to the logical axiom on plural constant shown in ((|#A_logical_axiom_on_plural_constant|Section 2.2.6)). That is to say, the expression {lo no broda} implies "there are what are broda, which are counted 0", which seems meaningless.

This means that official Lojban cannot express negation of existence of plural variable {naku su'oi da}, which is nevertheless necessary, for example in the following situation:

This response is an abbreviated form of {lo no prenu cu jmaji gi'e jukpa gi'e citka}.

This proposition means that {lo no prenu} satisfies selbri {jmaji} collectively and (je) non-distributively, {jukpa} collectively or (ja) distributively, {citka} non-collectively and (je) distributively. Because it includes selbri {jmaji} to be satisfied non-distributively, the sumti cannot be replaced by negation of existence of bound singular variable {naku su'o da}={no da}. Moreover, because it includes selbri {citka} to be satisfied non-collectively, {lo} of the sumti cannot be replaced by {loi}={lo gunma be lo}.

For making such a proposition meaningful, it is essential to give an expression {lo no broda} a meaning of negation of existence of plural variable.
For this purpose, I suggest the following definition valid in the case that PA=0 for {lo PA broda}.

Unofficial definition of {lo no broda}

lo no broda	=ca'e	naku su'oi da poi ke'a broda

（If it were defined as {naku lo broda}, the negation would have spanned the whole proposition, and it would not have implied quantification. I abandoned therefore such a definition.)

1.3.1.2.2. Cannot quantify material noun or something

Axiom 1 of ((|#Inner_quantification|Section 3.1)) excludes sumti that is neither an individual nor individuals from expressions {(su'o) N mei} and {lo N broda}.

Can we use {piPA} for sumti that is neither an individual nor individuals, then? No.
Actually, piPA is defined only for outer quantification.

As we can see in the definition, the body of outer quantification by {piPA} is plural constant {lo piPA si'e}, which is not a bound singular variable. However, x2 of {piPA si'e} is {pa me sumti}, to which the definition of PA broda is applied:

As a result, {piPA sumti} is defined only when there is an individual that satisfies x1 of {me sumti}. That is to say, what is neither an individual nor individuals is excluded also from an expression of outer quantification with {piPA}.

What would be if {piPA} were defined also for inner quantification?
In that case, the following definition would be desirable to conform the definition of {piPA} of outer quantification:

Unofficial definition of {piPA} of inner quantification

lo piPA broda	=ca'e	zo'e noi ke'a piPA si'e be lo pa broda

This definition of {piPA} of inner quantification still excludes what is neither an individual nor individuals unless {lo pa broda} is defined in another way so that it can be what is neither an individual nor individuals.

Why don't we use {PA si'e} to express quantification of what is neither an individual nor individuals?
It is possible, but BPFK's current definition of {si'e} depends on {pagbu}:

If we interpret {pagbu} so that x1 is not larger than x2 (and this is ordinary interpretation), {si'e} is very inconvenient because the unit should be changed every time counting up. If {si'e} were defined so that PA of {PA si'e} could be larger than 1, {si'e} would have been pragmatic for quantification of what is neither an individual nor individuals.

Besides those considerations, if we abandon Axiom 1 of ((|#Inner_quantification|Section 3.1)), Definitions (D1) (D2) (D3) can be applied to what is neither an individual nor individuals.
In this case, a speaker should select some plural constants {ko'a, ko'e, ...}, and decide that {[ko'a/ko'e/...] su'o pa mei}; the selection must be done attentively so that referents of plural constants that are {pa mei} do not overlap with each other.
Those preparations of {ko'a, ko'e, ...} and (D2) imply only

Under these conditions, there is no need that what is x1 of {pa mei} is an individual.

When we use Definitions (D1) (D2) (D3) without using Axiom 1 of ((|#Inner_quantification|Section 3.1)), a condition {gi'e su'o pa mei} must be added to {de} of (D1)（When Axiom 1 is used, referents in the domain of variable {de} satisfies this condition automatically).

Unofficial definitions under the condition that Axiom 1 is abandoned

(D1') ko'a su'o N mei	=ca'e	su'oi da poi me ko'a ku'o su'oi de poi me ko'a gi'e su'o pa mei zo'u ge da su'o N-1 mei ginai de me da
(D2) ko'a N mei	=ca'e	ko'a su'o N mei gi'e nai su'o N+1 mei
(D3) lo PA broda	=ca'e	zo'e noi ke'a PA mei gi'e broda

Using these definitions, inner quantification of what is neither an individual nor individuals becomes possible. Moreover, "Unofficial definition of {piPA} of inner quantification" discussed above becomes able to be applied to what is neither an individual nor individuals.

The diagram below shows a procedure of counting up what is neither an individual nor individuals represented with a directed graph. In this diagram, loops such as {X me X} are omitted for simplicity, though they exist. Among infinite number of vertices (plural constants), the vertices that a speaker selected as {su'o pa mei} are colored pink. Counting up corresponds to selecting a tree that is a subgraph of a directed graph formed with {me}, for example the part of blue color in the diagram.

1.3.2. Outer quantification

BPFK defines outer quantification as follows:

Outer quantification except {piPA} forms {PA da}, which is officially a bound singular variable. It implies that these arguments satisfy a predicate distributively. For example, it is meaningless to use {ci lo prenu} as x1 of {jmaji} (gather), because it is not the case that each of three people satisfies the predicate "gather".

However, if we use unofficial plural quantifiers {ro'oi} or {su'oi} for PA, outer quantification can form bound plural variable. For example,

This proposition is implied by a proposition including plural constant

with the logical axiom in ((|#A_logical_axiom_on_plural_constant|Section 2.2.6)).

{PA lo broda} differs from {PA broda} in domain of referents of bound singular variable to be counted. The definitions of outer quantification are applied to them as follows:

Example 1 mentions all {jmive} in the universe of discourse. In the universe of discourse of Example 2, it is possible to interpret that there are {prenu} other than the referent of the plural constant {lo prenu}.

The outer quantification by {piPA} forms plural constant {lo piPA si'e}. However, x2 of {piPA si'e} is bound singular variable {pa me sumti}. {pi} in this definition means "not larger than 1"; practically, {fi'u} or something can be used instead of {pi}

1.3.2.1. Combination of outer and inner quantifications

The definitions of inner and outer quantification imply the following interpretations:

Among them, {M lo [N] broda} and {pi M loi [N] broda} can express some of plural number of things.

{re lo [ci] mlatu} of Example 1 refers to two cats among [three] cats that are referent of {lo [ci] mlatu}.
If the inner quantifier {ci} is not said, it is unclear how many cats are referred to by {lo mlatu}; in any case {re lo mlatu} refers to two of them.

In Example 2, the argument is formed by {loi}, and the referent is actually {lo gunma}. Expanding Example 2 according to the definitions of {loi} and {piPA sumti},

That is to say, {re fi'u ci loi...} refers to two third of an individual {pa me lo gunma...}. This {lo gunma} consists of {vei ci pi'i ny (ve'o)} cats.
If the inner quantifier is not said, it is unclear how many cats constitute {lo gunma} that is {loi mlatu}; in any case {re fi'u ci loi mlatu} refers to two third of {lo gunma}. However,

is meaningful only when {loi mlatu} consists of 3n cats, because it is not ordinary to interpret that a fragment of a cat satisfies the predicate {viska}.
According to BPFK's definition, {loi} cannot form a plural constant that satisfies a predicate non-collectively. If you want to mean "cats see me non-collectively", avoid {loi}, or use {lu'a}, which will be discussed in ((|#Relation_between_lu_a_lu_o_lu_i_and_gadri|Section 3.3)):

1.3.2.2. Bound variables and constants in a statement

When both bound variables and constants appear in a statement, the constants do not necessarily span over all bound variables. Although they are called "constants", it is not generally determined whether they refer to common referents for all referents in domains of variables, or they refer to different referents dependent on referents in domains of variables. The reason follows below (Discussion).

When some sumti of terbri in a statement are omitted, it is considered that there are implicit {zo'e} in those places (CLL 7.7).
For example,

seems to be true from a standard point of view. According to definition of terbri of {jbena}, it is considered that three sumti are omitted, and this statement has the same meaning as

in which {zo'e} are explicit.
Unless all cats in this universe of discourse are/will be born to common parents at the same time at the same place, these {zo'e} cannot be considered as common constants for all referents in a domain of {ro mlatu}. In order to make such an expression like {ro mlatu cu jbena} have intended meaning, "constants" of Lojban can be dependent on referents in domains of bound variables.

"Constants" in this meaning correspond to Skolem functions in Skolem normal forms of predicate logic. The table below shows comparison of interpretations between predicate logic, xorlo on which this commentary depends and implicit quantifier (CLL Chapter 6) which was abolished. The expressions that have the same truth value are aligned in the same column. Upper case Y represents a plural variable. The row of zo'u+xorlo shows unofficial suggestion of interpretation. In the gray part in the row of Prenex normal, unofficial expressions with an experimental cmavo {su'oi} are shown. (Click on the table to enlarge.)