Envelope-to: lojban-list-archive@lojban.org
Delivery-date: Thu, 14 Jan 2021 08:43:48 -0800
Sender: lojban@googlegroups.com
Date: Thu, 14 Jan 2021 08:43:44 -0800 (PST)
From: Corbin Simpson <mostawesomedude@gmail.com>
To: lojban <lojban@googlegroups.com>
Message-Id: <324d35b2-cbfc-42d2-81a5-18c222d7163bn@googlegroups.com>
In-Reply-To: <81481203-08ac-cd57-4ca1-75838eb623eb@mail.jerrington.me>
References: <fe44283d-dd08-432e-8875-0abd7dab48a2n@googlegroups.com>
 <81481203-08ac-cd57-4ca1-75838eb623eb@mail.jerrington.me>
Subject: Re: [lojban] Second-order quantification has uses
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_2284_1470975525.1610642624163"
Reply-To: lojban@googlegroups.com
Precedence: list
Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com
X-Spam_score: -2.6
X-Spam_score_int: -25
X-Spam_bar: --

------=_Part_2284_1470975525.1610642624163
Content-Type: multipart/alternative; 
	boundary="----=_Part_2285_85558307.1610642624163"

------=_Part_2285_85558307.1610642624163
Content-Type: text/plain; charset="UTF-8"

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.

------=_Part_2285_85558307.1610642624163
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div class=3D"gmail_quote"><div dir=3D"auto" class=3D"gmail_attr">On Tuesda=
y, January 12, 2021 at 7:24:30 AM UTC-8 la tsani wrote:<br></div><blockquot=
e class=3D"gmail_quote" style=3D"margin: 0 0 0 0.8ex; border-left: 1px soli=
d rgb(204, 204, 204); padding-left: 1ex;">I think a consequence of this is =
bu'a et al are made obsolete by=20
<br>'first-order' quantification with da et al.
<br>
<br>Surely, there must be a reason why things aren't done this way in math=
=20
<br>as opposed to in Lojban. I'd bet it introduces some kind of paradox(es)=
.
<br></blockquote><div><br></div><div>mi'u You nailed it. In second-order lo=
gic, 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:</div><div><br></div><div><span><span><span><span></span></=
span><span></span></span></span><span><span><span><span>.i mi'o jersi lo sl=
abu tadji</span>
      </span>
      <span>
        </span></span></span><span><span><span><span><br>    .i sruma lo du=
'u da selcmi lo'i ro selcmi</span>
      </span>
      <span>
        </span></span></span><span><span><span><span><br>    .i pensi lo du=
'u lo ka ce'u na cmima ce'u ku steci de da</span>
      </span>
      <span>
        </span></span></span><span><span><span><span><br>    .i ganai de cm=
ima de gi de na cmima de .i natfe</span>
      </span>
      <span>
        </span></span></span><span><span><span><span><br>    .i ganai de na=
 cmima de gi de cmima de .i natfe</span>
      </span>
      <span>
        </span></span></span>    .i jitfa nibli tadji .i na'e natfe jicmu .=
i lo'i ro selcmi ku na cmima</div><div><br></div><div>This demonstrates tha=
t the relation {cmima} is not quite complete; there's at least one collecti=
on 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-o=
rder world; {bu'a} is a syntactic tool, not just of a different stratificat=
ion.<br></div><div><br></div><div>But, at the same time, when we consider w=
hat {bu'a} quantifies over, we find that it gives us predicates which eithe=
r do or do not hold for each element, and we can extend these predicates in=
to what Frege called "extensions". We call them *sets* today. In second-ord=
er logic, there is a unification between sets, extensions, predicates, and =
relations, s.t. we can make categorical statements which are firmly embedde=
d in the ambient set theory. If our ambient set theory has e.g. natural num=
bers, then second-order logic knows about them too, and also knows that the=
y're the unique such collection.</div><div><br></div><div>The only reason t=
o do first-order set theory is if we are studying sets themselves, and we d=
oubt our ambient set theory. For Lojban, we shouldn't be so squeamish, espe=
cially when the {bu'a} series already exists. But, that said, the main reas=
on 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 a=
ll 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.)<br></div></div>

<p></p>

-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;lojban&quot; group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:lojban+unsubscribe@googlegroups.com">lojban+unsub=
scribe@googlegroups.com</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/d/msgid/lojban/324d35b2-cbfc-42d2-81a5-18c222d7163bn%40googlegroups.com?=
utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.com/d/msgid/l=
ojban/324d35b2-cbfc-42d2-81a5-18c222d7163bn%40googlegroups.com</a>.<br />

------=_Part_2285_85558307.1610642624163--

------=_Part_2284_1470975525.1610642624163--