Second-order quantification has uses

[Corbin Simpson]

coi

I wanted to follow up on a point of la tsani's from the thread "Reasoning by analogy". The point is raised that perhaps {bu'a} is not very useful. At least formally, though, it has enormous potential for giving categorical definitions of objects. (Here, "categorical" is used in the sense of Dedekind and Hilbert: A categorical structure is one which second-order logic can uniquely identify. The typical example is that the natural numbers, if they exist, are categorical.)

The example that I've been playing with recently is how to define {du}. Considering only the binary version of {du}, there are two definitions in jbovlaste currently. One is from la xorxes:

    lu'e x1 mintu lu'e x2 le ka ce'u sinxa makau

That is, {x1 du x2} means that x1 and x2 are references which are equivalent under the operation of looking up their referents; x1 and x2 refer to the same thing. This definition relies upon {mintu} and {sinxa}; I would hope that at least {mintu} could instead be defined in terms of {du}! (la xorxes also goes on to define {mintu} in terms of {dunli}.) Meanwhile, there's also this definition from la ilmen:

    x1 jo'u x2 simxu lo ka ro da poi selkai ce'u cu selkai ce'u .i va'i ro da se ckaji x1 .o x2

That is, {x1 du x2} means that the collection/set of {x1, x2} is self-similar/automorphic when we try to tell x1 and x2 apart by looking at the properties which characterize them; in other words, all properties apply to x1 iff they apply to x2. This is what la tsani refers to by discussing reified {ka} abstractions.

Now, consider this definition, transcribed from nonfirstorderizeable lore:

    ro bu'a zo'u x1 .o x2 bu'a

That is, {x1 du x2} means that, for any property P, P holds for x1 iff it holds for x2. No property can tell apart x1 and x2.

This is the power of second-order logic and {bu'a}, if we embrace it.

u'i .i mi'e la korvo .i co'o

u'isai ji'a Also notice that {x1 me x2} suddenly has a clean definition if we change {.o} to {na.a}, without using any plural logic whatsoever. Second-order logic knows what sets are, because it knows what properties are, and sets are merely extensions of properties.

[Jacob Thomas Errington]

coi

On 2021-01-08 13:17, Corbin Simpson wrote:
> That is, {x1 du x2} means that x1 and x2 are references which are
> equivalent under the operation of looking up their referents; x1 and
> x2 refer to the same thing. This definition relies upon {mintu} and
> {sinxa}; I would hope that at least {mintu} could instead be defined
> in terms of {du}! (la xorxes also goes on to define {mintu} in terms
> of {dunli}.) Meanwhile, there's also this definition from la ilmen:
>
>     x1 jo'u x2 simxu lo ka ro da poi selkai ce'u cu selkai ce'u .i
> va'i ro da se ckaji x1 .o x2
>
> That is, {x1 du x2} means that the collection/set of {x1, x2} is
> self-similar/automorphic when we try to tell x1 and x2 apart by
> looking at the properties which characterize them; in other words, all
> properties apply to x1 iff they apply to x2. This is what la tsani
> refers to by discussing reified {ka} abstractions.

Let's forget the first sentence from Ilmen's definition and look at the
second sentence, which he says is a rephrasing of the first.

  .i ro da se ckaji x1 .o x2

Now we need to squint a little and pretend that this {ro da} is
referring only to properties, doesn't this work out to the same thing as

  .i ro bu'a zo'u x1 .o x2 bu'a

?

Lojban is funny in that you can smuggle selbri around as sumti (as
witnessed by the very common {lo ka}) and 'unbox' them with {ckaji} --
this unboxing is very flavourless, but there are delicious unboxings
like {carmi}, {pluka}, etc. -- and more generally you can unbox any
reified selbri with the experimental cmavo {me'au}:

  .i x1 x2 x3 ... broda === x1 x2 x3 ... me'au lo ka ce'u ce'u ce'u ...
broda

I think a consequence of this is bu'a et al are made obsolete by
'first-order' quantification with da et al.

Surely, there must be a reason why things aren't done this way in math
as opposed to in Lojban. I'd bet it introduces some kind of paradox(es).

.i mi'e la tsani mu'o

[scope845h...@icebubble.org]

Jacob Thomas Errington <ja...@mail.jerrington.me> writes:

> Lojban is funny in that you can smuggle selbri around as sumti (as witnessed by the very common {lo ka}) and 'unbox' them with {ckaji} --
> this unboxing is very flavourless, but there are delicious unboxings
> like {carmi}, {pluka}, etc. -- and more generally you can unbox any
> reified selbri with the experimental cmavo {me'au}:
>
>   .i x1 x2 x3 ... broda === x1 x2 x3 ... me'au lo ka ce'u ce'u ce'u
> ... broda

I use {nu'a ma'o mo'e} for that. It takes an indirect route - via
Lojban's mex subgrammar - but it gets there.

[Mark E. Shoulson]

On 1/8/21 1:17 PM, Corbin Simpson wrote:

coi

I wanted to follow up on a point of la tsani's from the thread "Reasoning by analogy". The point is raised that perhaps {bu'a} is not very useful.

I think I recall (the?) one time I felt a use for {bu'a}, but I did have to have it explained to me that {ro bu'a zo'u} doesn't mean "for all things that bu'a" but rather "for all predicates bu'a," which is an exception to the usual rules—precisely because otherwise it's hard to use {bu'a}!

Esther 8:1: "For she (Esther) had told him (Ahasuerus) what he (Mordecai) was to her [viz. her cousin]"

.i .ebu pu cusku fi .abu fe lo du'u my bu'akau .ebu

I guess it doesn't need the quantification after all (this originally occurred to me before the invention of {kau}, I think.)  Does there need to be some quantification anyway, though?  To mean some particular implied (ellipsized) relationship, and not some random one like {viska} or {te djuno} or something?

~mark

[Corbin Simpson]

On Tuesday, January 12, 2021 at 7:24:30 AM UTC-8 la tsani wrote:

I think a consequence of this is bu'a et al are made obsolete by
'first-order' quantification with da et al.

Surely, there must be a reason why things aren't done this way in math
as opposed to in Lojban. I'd bet it introduces some kind of paradox(es).

mi'u You nailed it. In second-order logic, we understand that elements are not the same type as sets of elements. The main reason for this is Russell's Paradox. To quote from a translation I'm working on:

.i mi'o jersi lo slabu tadji
.i sruma lo du'u da selcmi lo'i ro selcmi
.i pensi lo du'u lo ka ce'u na cmima ce'u ku steci de da
.i ganai de cmima de gi de na cmima de .i natfe
.i ganai de na cmima de gi de cmima de .i natfe .i jitfa nibli tadji .i na'e natfe jicmu .i lo'i ro selcmi ku na cmima

This demonstrates that the relation {cmima} is not quite complete; there's at least one collection which is implied to exist (because all of its elements exist) and which contains every inhabited set (by definition!) and which behaves like a set, but which is not itself a set (by the above statement of Russell's Paradox). It also shows that we can still use {da} to bind sets even in a second-order world; {bu'a} is a syntactic tool, not just of a different stratification.

But, at the same time, when we consider what {bu'a} quantifies over, we find that it gives us predicates which either do or do not hold for each element, and we can extend these predicates into what Frege called "extensions". We call them *sets* today. In second-order logic, there is a unification between sets, extensions, predicates, and relations, s.t. we can make categorical statements which are firmly embedded in the ambient set theory. If our ambient set theory has e.g. natural numbers, then second-order logic knows about them too, and also knows that they're the unique such collection.

The only reason to do first-order set theory is if we are studying sets themselves, and we doubt our ambient set theory. For Lojban, we shouldn't be so squeamish, especially when the {bu'a} series already exists. But, that said, the main reason to embrace {bu'a} is that it makes some statements simpler and lighter. (There's also the problem that no Lojban gismu even tries to be a type of all propositions, or all events, in the same way that ckaji2 and cmima2 have all (inhabited) sets. Doing proper type theory requires a way to do proper type annotation.)

[Jacob Thomas Errington]

For these kinds of "you're free to be as you are" type of statements, I actually think there's a connection to indirect questions. In a sense, there is a hidden indirect question when we say "as you are", since it appears in a subclause and we're not actually _saying_ what "as you are" is supposed to be. It's kind of like saying "tell me who I am".

So in Lojban:

.i do zifre lo ka mokau

Or to rephrase your example:

.i .ebu pu cusku fi .abu fe lo du'u my .ebu mokau