Sender: lojban@googlegroups.com
Date: Tue, 11 Aug 2020 07:26:54 -0700 (PDT)
From: mostawesomedude@gmail.com
To: lojban <lojban@googlegroups.com>
Message-Id: <676db32f-fdd7-479f-825e-4571293b08a1o@googlegroups.com>
Subject: [lojban] Difficult logical questions
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_1326_592088045.1597156014904"
Reply-To: lojban@googlegroups.com
Precedence: list
Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com
X-Spam_score: -2.5
X-Spam_score_int: -24
X-Spam_bar: --

------=_Part_1326_592088045.1597156014904
Content-Type: multipart/alternative; 
	boundary="----=_Part_1327_698091101.1597156014904"

------=_Part_1327_698091101.1597156014904
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

coi

I apologize somewhat in advance. The following questions have driven folks=
=20
mad (mostly on IRC, but also sometimes IRL), so don't worry if you're not=
=20
interested in them. However, they all seem extremely pertinent to continued=
=20
formalization efforts, and I'd like to think that they've come up before. I=
=20
also have rigged the game somewhat by having an answer for each question,=
=20
which I'll provide; however, I'm very interested in what answers other=20
folks have, and I am only committed to my answers inasmuch as I have=20
researched them in order to have a well-read opinion.

Relations are, generally, sets. In particular they are subsets of products.=
=20
Even more particularly, nullary relations are truth values and unary=20
relations are sets. However, ckaji2 ranges over all unary relations and=20
ckini3 ranges over all binary relations; kampu2, cmima2, and steci3 range=
=20
over (almost) all sets. This leads to immediate size issues; how do we=20
avoid Russell's paradox?

My answer is to declare an inaccessible cardinal, which is like a=20
cornerstone that can be used to build a "small" set theory. This cardinal=
=20
can be big enough to give us enough room for not just ZF set theory, but=20
any small category or similar structure. The downside is that we are=20
immediately cut off from some large objects; however, we weren't using them=
=20
anyway. However, we are given a very flexible universe of things; we are=20
free to accept the Axiom of Choice, or not; we can also choose whether to=
=20
accept the Law of Excluded Middle.

CLL Lojban allows quantification ranging over two orders of variables; {da}=
=20
range over things, while {bu'a} range over relations between things. This=
=20
is syntax for second-order logic (SOL). However, many speakers, including=
=20
myself, infer an informal type system which constrains each {da} to range=
=20
only over some set of things which isn't the set of all things in the=20
universe. (To clarify this sentence, solve our size issues.) When all=20
things are constrained in this way, then it happens that second-order logic=
=20
becomes many-sorted first-order logic; every "set of things" becomes its=20
own type in a sort of types of sets. Is Lojban second-order, or many-sorted=
=20
first-order?

My answer is to embrace full SOL. The main tradeoff to consider is that=20
full second-order semantics often give categoricity, which means that=20
things can be specified up to isomorphism, but are G=C3=B6del-incomplete; w=
hile=20
first-order semantics can be G=C3=B6del-complete, but usually admits=20
non-standard models of any infinite thing. For example, the natural numbers=
=20
are categorical, which means that there is a second-order theory (known as=
=20
Z=E2=82=82) which uniquely identifies them. In modern category-theoretic la=
nguage,=20
we say that a natural numbers object, or NNO, is unique when it exists. In=
=20
both cases, the uniqueness is up to the bounding rules of the universe of=
=20
sets. We can, of course, recover fragments of first-order reasoning at any=
=20
time by simply putting extra {poi} onto our {da}, and we can mechanically=
=20
send SOL to FOL with some choice of type-inference algorithm.

Also, like, "the cat is red," is it a cat or a red? SOL lets us just say=20
that it's a thing which is both among the set of cats and also among the=20
set of reds, while FOL requires us to informally infer types and say that=
=20
it's a cat.

CLL gives full-throated support for the Law of Excluded Middle (LEM), with=
=20
a rule which sends {na na broda} =3D> {broda}. This happens to be equivalen=
t=20
to a complete buy-in to the world of Boolean reasoning, and there are=20
examples of this embrace throughout Lojban. {nagi'a} is mistaken for=20
implication, for example, despite merely having the same truth table in the=
=20
Booleans; {steci} manifests the Axiom of Choice in one direction with=20
steci1 empty, or LEM with steci2 empty. To be fair, it's reasonable to=20
imagine that, since a unary relation is a set, surely a thing either is or=
=20
is not an element of a unary relation. But, over the past century, we've=20
found that LEM is not realizeable/computable. {le du'u nei jitfa} (or=20
whatever equivalent one (in)formally desires to work with) doesn't have a=
=20
consistent truth value. So do we keep LEM?

My answer is kind of biased, isn't it? I'm a constructivist of sorts, so=20
I'm going to prefer it if LEM is optional. It can always be added in on a=
=20
per-proof basis in order to tighten up some reasoning. But this also=20
requires trading in De Morgan's laws and negation-raising through the=20
prenex for weaker constructive versions.

Oh, also, the inaccessible-cardinal construction I used earlier gives us a=
=20
topos, but not necessarily a Boolean topos; if we have a set of things, we=
=20
can't form the set of all things in the universe which are't in our=20
original set, because we can't see from inside the topos that the=20
universe's things might all fit into a set.

To be a bit more clear, we could still have {na na na broda} <=3D> {na=20
broda}. There would still only be two truth values. We simply would be a=20
bit more honest about when we can't tell which of the two truth values=20
we're supposed to assign.

I hope that this was useful food for thought for the multiple folks working=
=20
on different formalizations, since I think that everybody will need to=20
answer these questions one way or another.

And finally, I should include preliminary feedback from IRC. Folks were=20
generally supportive of the first two points, but preferred not giving up=
=20
LEM. There were strong and serious concerns about contextuality vs. modal=
=20
possibility and the domain of discourse vs. the universe of things; folks=
=20
don't want Lojban to be artificially limited. In general, I'm finding that=
=20
that one quote from a decade ago is true, about how formalization is a=20
political process even when the maths is well-settled.

.i mi'e la korvo .i di'ai

--=20
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 e=
mail to lojban+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/=
lojban/676db32f-fdd7-479f-825e-4571293b08a1o%40googlegroups.com.

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

<div dir=3D"ltr">coi<br><br>I apologize somewhat in advance. The following =
questions have driven folks mad (mostly on IRC, but also sometimes IRL), so=
 don&#39;t worry if you&#39;re not interested in them. However, they all se=
em extremely pertinent to continued formalization efforts, and I&#39;d like=
 to think that they&#39;ve come up before. I also have rigged the game some=
what by having an answer for each question, which I&#39;ll provide; however=
, I&#39;m very interested in what answers other folks have, and I am only c=
ommitted to my answers inasmuch as I have researched them in order to have =
a well-read opinion.<br><br>Relations are, generally, sets. In particular t=
hey are subsets of products. Even more particularly, nullary relations are =
truth values and unary relations are sets. However, ckaji2 ranges over all =
unary relations and ckini3 ranges over all binary relations; kampu2, cmima2=
, and steci3 range over (almost) all sets. This leads to immediate size iss=
ues; how do we avoid Russell&#39;s paradox?<br><br>My answer is to declare =
an inaccessible cardinal, which is like a cornerstone that can be used to b=
uild a &quot;small&quot; set theory. This cardinal can be big enough to giv=
e us enough room for not just ZF set theory, but any small category or simi=
lar structure. The downside is that we are immediately cut off from some la=
rge objects; however, we weren&#39;t using them anyway. However, we are giv=
en a very flexible universe of things; we are free to accept the Axiom of C=
hoice, or not; we can also choose whether to accept the Law of Excluded Mid=
dle.<br><br>CLL Lojban allows quantification ranging over two orders of var=
iables; {da} range over things, while {bu&#39;a} range over relations betwe=
en things. This is syntax for second-order logic (SOL). However, many speak=
ers, including myself, infer an informal type system which constrains each =
{da} to range only over some set of things which isn&#39;t the set of all t=
hings in the universe. (To clarify this sentence, solve our size issues.) W=
hen all things are constrained in this way, then it happens that second-ord=
er logic becomes many-sorted first-order logic; every &quot;set of things&q=
uot; becomes its own type in a sort of types of sets. Is Lojban second-orde=
r, or many-sorted first-order?<br><br>My answer is to embrace full SOL. The=
 main tradeoff to consider is that full second-order semantics often give c=
ategoricity, which means that things can be specified up to isomorphism, bu=
t are G=C3=B6del-incomplete; while first-order semantics can be G=C3=B6del-=
complete, but usually admits non-standard models of any infinite thing. For=
 example, the natural numbers are categorical, which means that there is a =
second-order theory (known as Z=E2=82=82) which uniquely identifies them. I=
n modern category-theoretic language, we say that a natural numbers object,=
 or NNO, is unique when it exists. In both cases, the uniqueness is up to t=
he bounding rules of the universe of sets. We can, of course, recover fragm=
ents of first-order reasoning at any time by simply putting extra {poi} ont=
o our {da}, and we can mechanically send SOL to FOL with some choice of typ=
e-inference algorithm.<br><br>Also, like, &quot;the cat is red,&quot; is it=
 a cat or a red? SOL lets us just say that it&#39;s a thing which is both a=
mong the set of cats and also among the set of reds, while FOL requires us =
to informally infer types and say that it&#39;s a cat.<br><br>CLL gives ful=
l-throated support for the Law of Excluded Middle (LEM), with a rule which =
sends {na na broda} =3D&gt; {broda}. This happens to be equivalent to a com=
plete buy-in to the world of Boolean reasoning, and there are examples of t=
his embrace throughout Lojban. {nagi&#39;a} is mistaken for implication, fo=
r example, despite merely having the same truth table in the Booleans; {ste=
ci} manifests the Axiom of Choice in one direction with steci1 empty, or LE=
M with steci2 empty. To be fair, it&#39;s reasonable to imagine that, since=
 a unary relation is a set, surely a thing either is or is not an element o=
f a unary relation. But, over the past century, we&#39;ve found that LEM is=
 not realizeable/computable. {le du&#39;u nei jitfa} (or whatever equivalen=
t one (in)formally desires to work with) doesn&#39;t have a consistent trut=
h value. So do we keep LEM?<br><br>My answer is kind of biased, isn&#39;t i=
t? I&#39;m a constructivist of sorts, so I&#39;m going to prefer it if LEM =
is optional. It can always be added in on a per-proof basis in order to tig=
hten up some reasoning. But this also requires trading in De Morgan&#39;s l=
aws and negation-raising through the prenex for weaker constructive version=
s.<br><br>Oh, also, the inaccessible-cardinal construction I used earlier g=
ives us a topos, but not necessarily a Boolean topos; if we have a set of t=
hings, we can&#39;t form the set of all things in the universe which are=
9;t in our original set, because we can&#39;t see from inside the topos tha=
t the universe&#39;s things might all fit into a set.<br><br>To be a bit mo=
re clear, we could still have {na na na broda} &lt;=3D&gt; {na broda}. Ther=
e would still only be two truth values. We simply would be a bit more hones=
t about when we can&#39;t tell which of the two truth values we&#39;re supp=
osed to assign.<br><br><div>I hope that this was useful food for thought fo=
r the multiple folks working on different formalizations, since I think tha=
t everybody will need to answer these questions one way or another.</div><d=
iv><br></div><div>And finally, I should include preliminary feedback from I=
RC. Folks were generally supportive of the first two points, but preferred =
not giving up LEM. There were strong and serious concerns about contextuali=
ty vs. modal possibility and the domain of discourse vs. the universe of th=
ings; folks don&#39;t want Lojban to be artificially limited. In general, I=
&#39;m finding that that one quote from a decade ago is true, about how for=
malization is a political process even when the maths is well-settled.<br><=
/div><br>.i mi&#39;e la korvo .i di&#39;ai<br></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/676db32f-fdd7-479f-825e-4571293b08a1o%40googlegroups.com?=
utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.com/d/msgid/l=
ojban/676db32f-fdd7-479f-825e-4571293b08a1o%40googlegroups.com</a>.<br />

------=_Part_1327_698091101.1597156014904--

------=_Part_1326_592088045.1597156014904--