Envelope-to: lojban-list-archive@lojban.org
Delivery-date: Fri, 08 Jan 2021 10:22:31 -0800
Sender: lojban@googlegroups.com
Date: Fri, 8 Jan 2021 10:17:48 -0800 (PST)
From: Corbin Simpson <mostawesomedude@gmail.com>
To: lojban <lojban@googlegroups.com>
Message-Id: <fe44283d-dd08-432e-8875-0abd7dab48a2n@googlegroups.com>
Subject: [lojban] Second-order quantification has uses
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_1432_1201699867.1610129868489"
Reply-To: lojban@googlegroups.com
Precedence: list
Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com
X-Spam_score: -2.2
X-Spam_score_int: -21
X-Spam_bar: --

------=_Part_1432_1201699867.1610129868489
Content-Type: multipart/alternative; 
	boundary="----=_Part_1433_974454521.1610129868489"

------=_Part_1433_974454521.1610129868489
Content-Type: text/plain; charset="UTF-8"

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.

-- 
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/fe44283d-dd08-432e-8875-0abd7dab48a2n%40googlegroups.com.

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

<div>coi</div><div><br></div><div>I wanted to follow up on a point of la ts=
ani's from the thread "Reasoning by analogy". The point is raised that perh=
aps {bu'a} is not very useful. At least formally, though, it has enormous p=
otential 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.)</div><div><br></=
div><div>The example that I've been playing with recently is how to define =
{du}. Considering only the binary version of {du}, there are two definition=
s in jbovlaste currently. One is from la xorxes:</div><div><br></div><div>&=
nbsp;&nbsp;&nbsp; lu'e x<span>1</span> mintu lu'e x<span>2</span> le ka ce'=
u sinxa makau</div><div><br></div><div>That is, {x1 du x2} means that x1 an=
d 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 t=
erms of {dunli}.) Meanwhile, there's also this definition from la ilmen:</d=
iv><div><br></div><div>&nbsp;&nbsp;&nbsp; x<span>1</span> jo'u x<span>2</sp=
an> simxu lo ka ro da poi selkai ce'u cu selkai ce'u .i va'i ro da se ckaji=
 x<span>1</span> .o x<span>2</span></div><div><span><br></span></div><div><=
span>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 p=
roperties 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 reif=
ied {ka} abstractions.</span></div><div><span><br></span></div><div><span>N=
ow, consider this definition, transcribed from nonfirstorderizeable lore:</=
span></div><div><span><br></span></div><div><span>&nbsp;&nbsp;&nbsp; ro bu'=
a zo'u x1 .o x2 bu'a</span></div><div><span><br></span></div><div><span>Tha=
t is, {x1 du x2} means that, for any property P, P holds for x1 iff it hold=
s for x2. No property can tell apart x1 and x2.</span></div><div><span><br>=
</span></div><div><span>This is the power of second-order logic and {bu'a},=
 if we embrace it.</span></div><div><span><br></span></div><div><span>u'i .=
i mi'e la korvo .i co'o<br></span></div><div><span><br></span></div><div><s=
pan>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. Se=
cond-order logic knows what sets are, because it knows what properties are,=
 and sets are merely extensions of properties.<br></span></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/fe44283d-dd08-432e-8875-0abd7dab48a2n%40googlegroups.com?=
utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.com/d/msgid/l=
ojban/fe44283d-dd08-432e-8875-0abd7dab48a2n%40googlegroups.com</a>.<br />

------=_Part_1433_974454521.1610129868489--

------=_Part_1432_1201699867.1610129868489--