Sender: lojban@googlegroups.com
Date: Mon, 5 Oct 2020 16:28:01 -0700 (PDT)
From: Corbin Simpson <mostawesomedude@gmail.com>
To: lojban <lojban@googlegroups.com>
Message-Id: <8d4c191f-7015-4fd1-ae70-fa721ff98efbn@googlegroups.com>
Subject: [lojban] Inventory of logical connectives
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_664_955045251.1601940481042"
Reply-To: lojban@googlegroups.com
Precedence: list
Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com
X-Spam_score: -0.9
X-Spam_score_int: -8
X-Spam_bar: /

------=_Part_664_955045251.1601940481042
Content-Type: multipart/alternative; 
	boundary="----=_Part_665_960421199.1601940481042"

------=_Part_665_960421199.1601940481042
Content-Type: text/plain; charset="UTF-8"


coi

la gleki asks, in private communication, about several features of the 
inventory of logical connectives.

First, does Lojban have operators/connectives for material 
condition/implication? I claim no, which is contra CLL. To explain, let's 
take for example the family of jeks, with {ja}, {je}, {jo}, and {ju}. CLL 
suggests that {naja} is then the implication for this family. But is it?

Classical Boolean logic is not the only logic, and as soon as we 
generalize, then we have questions about implication. First, let's consider 
constructive Boolean logic. Imagine that we try to expand `X -> Y` to `~X 
\/ Y` using the above {naja} CLL rule. However, in constructive logic, `~X` 
"not X" is actually shorthand for `X -> _|_` "X implies falsehood", so our 
expansion becomes `(X -> _|_) \/ Y`. In constructive logic, implication is 
a primitive operation which can't be built just by satisfying a truth 
table. (BHK interpretations show us that constructive logic doesn't just 
show statements true or false, but builds structures which witness their 
truth/falsity.)

[omitted paragraph about linear logic; yes, it exists; no, it isn't germane]

Lojban, I think, is built on relations; this means that it has relational 
logic. (Lojban also has classical logic; the two logics interact through 
2-categorical structure called an allegory.) In relational logic, we can 
reverse implications; `X -> Y` can be transformed into `Y -> X`. For 
example, given an implication {pa ka ce'u mlatu ce'u} which sends cats to 
species, we can obtain the reversal {pa ka ce'u se mlatu ce'u} which send 
species to cats. Recall that relational logic is many-to-many, so negation 
doesn't work like one might expect.

Practically, what does this mean? Well, it's bikeshed time. Personally, I 
recommend altering the CLL's De Morgan rules so that {naja} cannot be 
desugared into { ... na ... ja } with NA moving into and out of the 
connective, and instead freeze {naja} as "implies". I'm not 100% convinced 
that this is right, but it's very compatibilist: everybody still reads it 
as "implies" and we just disagree on what expansions are legal.

la gleki also asks about optimality of the current syntactic allocation. In 
particular, the quantifiers are in PA, the modal-logic operators are in 
CAhA, negation is in NA, NAI, and NAhE; what could be done better?

One obvious point is that all formal logics tend to get by with just one 
form of negation. Indeed, negation is usually tightly controlled and only 
mentioned in one or two axioms.

Modal logic being contained to CAhA makes it easy to be optional or to 
specify in terms of other grammar (thinking specifically of PU). CAhA 
cannot tag sumti like UI, which is unfortunate if one actually wanted to 
*do* modal logic.

NAhE could be extremely powerful, depending on how it's formalized.

-- 
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/8d4c191f-7015-4fd1-ae70-fa721ff98efbn%40googlegroups.com.

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

<br><div>coi</div><div><br></div><div>la gleki asks, in private communicati=
on, about several features of the inventory of logical connectives.</div><d=
iv><br></div><div>First, does Lojban have operators/connectives for materia=
l condition/implication? I claim no, which is contra CLL. To explain, let's=
 take for example the family of jeks, with {ja}, {je}, {jo}, and {ju}. CLL =
suggests that {naja} is then the implication for this family. But is it?</d=
iv><div><br></div><div>Classical Boolean logic is not the only logic, and a=
s soon as we generalize, then we have questions about implication. First, l=
et's consider constructive Boolean logic. Imagine that we try to expand `X =
-&gt; Y` to `~X \/ Y` using the above {naja} CLL rule. However, in construc=
tive logic, `~X` "not X" is actually shorthand for `X -&gt; _|_` "X implies=
 falsehood", so our expansion becomes `(X -&gt; _|_) \/ Y`. In constructive=
 logic, implication is a primitive operation which can't be built just by s=
atisfying a truth table. (BHK interpretations show us that constructive log=
ic doesn't just show statements true or false, but builds structures which =
witness their truth/falsity.)</div><div><br></div><div>[omitted paragraph a=
bout linear logic; yes, it exists; no, it isn't germane]</div><div><br></di=
v><div>Lojban, I think, is built on relations; this means that it has relat=
ional logic. (Lojban also has classical logic; the two logics interact thro=
ugh 2-categorical structure called an allegory.) In relational logic, we ca=
n reverse implications; `X -&gt; Y` can be transformed into `Y -&gt; X`. Fo=
r example, given an implication {pa ka ce'u mlatu ce'u} which sends cats to=
 species, we can obtain the reversal {pa ka ce'u se mlatu ce'u} which send =
species to cats. Recall that relational logic is many-to-many, so negation =
doesn't work like one might expect.</div><div><br></div><div>Practically, w=
hat does this mean? Well, it's bikeshed time. Personally, I recommend alter=
ing the CLL's De Morgan rules so that {naja} cannot be desugared into { ...=
 na ... ja } with NA moving into and out of the connective, and instead fre=
eze {naja} as "implies". I'm not 100% convinced that this is right, but it'=
s very compatibilist: everybody still reads it as "implies" and we just dis=
agree on what expansions are legal.</div><div><br></div><div>la gleki also =
asks about optimality of the current syntactic allocation. In particular, t=
he quantifiers are in PA, the modal-logic operators are in CAhA, negation i=
s in NA, NAI, and NAhE; what could be done better?</div><div><br></div><div=
>One obvious point is that all formal logics tend to get by with just one f=
orm of negation. Indeed, negation is usually tightly controlled and only me=
ntioned in one or two axioms.</div><div><br></div><div>Modal logic being co=
ntained to CAhA makes it easy to be optional or to specify in terms of othe=
r grammar (thinking specifically of PU). CAhA cannot tag sumti like UI, whi=
ch is unfortunate if one actually wanted to *do* modal logic.</div><div><br=
></div><div>NAhE could be extremely powerful, depending on how it's formali=
zed.<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/8d4c191f-7015-4fd1-ae70-fa721ff98efbn%40googlegroups.com?=
utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.com/d/msgid/l=
ojban/8d4c191f-7015-4fd1-ae70-fa721ff98efbn%40googlegroups.com</a>.<br />

------=_Part_665_960421199.1601940481042--

------=_Part_664_955045251.1601940481042--