[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [lojban] Second-order quantification has uses



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

--
You received this message because you are subscribed to the Google Groups "lojban" group.
To unsubscribe from this group and stop receiving emails from it, send an email to lojban+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/lojban/324d35b2-cbfc-42d2-81a5-18c222d7163bn%40googlegroups.com.